From 845813d4bb6ee9f5453a430dcbc2947224a0c204 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 14 Feb 2026 18:41:37 -0300
Subject: [PATCH] Run Rocq tests.

---
 .forgejo/workflows/test.yml |  1 +
 rocq-demo/.gitignore        |  8 ++++++++
 rocq-demo/Makefile          | 31 +++++++++++++++++++++++++++++++
 rocq-demo/_CoqProject       |  5 +++++
 scripts/check-copyright.sh  |  2 +-
 5 files changed, 46 insertions(+), 1 deletion(-)
 create mode 100644 rocq-demo/.gitignore
 create mode 100644 rocq-demo/Makefile
 create mode 100644 rocq-demo/_CoqProject

diff --git a/.forgejo/workflows/test.yml b/.forgejo/workflows/test.yml
index 001168f4..77d378d1 100644
--- a/.forgejo/workflows/test.yml
+++ b/.forgejo/workflows/test.yml
@@ -16,6 +16,7 @@ jobs:
       - uses: https://git.libre-chip.org/mirrors/rust-cache@v2
         with:
           save-if: ${{ github.ref == 'refs/heads/master' }}
+      - run: make -C rocq-demo
       - run: cargo test
       - run: cargo build --tests --features=unstable-doc
       - run: cargo test --doc --features=unstable-doc
diff --git a/rocq-demo/.gitignore b/rocq-demo/.gitignore
new file mode 100644
index 00000000..01821130
--- /dev/null
+++ b/rocq-demo/.gitignore
@@ -0,0 +1,8 @@
+# SPDX-License-Identifier: LGPL-3.0-or-later
+# See Notices.txt for copyright information
+.CoqMakefile.d
+*.aux
+CoqMakefile
+CoqMakefile.conf
+*.glob
+*.vo*
diff --git a/rocq-demo/Makefile b/rocq-demo/Makefile
new file mode 100644
index 00000000..d0d5c9e3
--- /dev/null
+++ b/rocq-demo/Makefile
@@ -0,0 +1,31 @@
+# SPDX-License-Identifier: LGPL-3.0-or-later
+# See Notices.txt for copyright information
+#
+# Example Makefile wrapper as given on the Rocq documentation
+# https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/utilities.html#building-a-rocq-project-with-rocq-makefile-details
+
+# KNOWNTARGETS will not be passed along to CoqMakefile
+KNOWNTARGETS := CoqMakefile
+# KNOWNFILES will not get implicit targets from the final rule, and so
+# depending on them won't invoke the submake
+# Warning: These files get declared as PHONY, so any targets depending
+# on them always get rebuilt
+KNOWNFILES   := Makefile _CoqProject
+
+.DEFAULT_GOAL := invoke-coq-makefile
+
+CoqMakefile: Makefile _CoqProject
+	$(COQBIN)rocq makefile -f _CoqProject -o CoqMakefile
+
+invoke-coq-makefile: CoqMakefile
+	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
+
+.PHONY: invoke-coq-makefile $(KNOWNFILES)
+
+####################################################################
+##                      Your targets here                         ##
+####################################################################
+
+# This should be the last rule, to handle any targets not declared above
+%: invoke-coq-makefile
+	@true
diff --git a/rocq-demo/_CoqProject b/rocq-demo/_CoqProject
new file mode 100644
index 00000000..be104207
--- /dev/null
+++ b/rocq-demo/_CoqProject
@@ -0,0 +1,5 @@
+# SPDX-License-Identifier: LGPL-3.0-or-later
+# See Notices.txt for copyright information
+
+-Q . RocqDemo
+.
diff --git a/scripts/check-copyright.sh b/scripts/check-copyright.sh
index 023cd21f..99205bb3 100755
--- a/scripts/check-copyright.sh
+++ b/scripts/check-copyright.sh
@@ -50,7 +50,7 @@ function main()
         /crates/fayalite/tests/ui/*.stderr|/crates/fayalite/tests/sim/expected/*.vcd|/crates/fayalite/tests/sim/expected/*.txt)
             # file that can't contain copyright header
             ;;
-        /.forgejo/workflows/*.yml|*/.gitignore|*.toml)
+        /.forgejo/workflows/*.yml|*/.gitignore|*.toml|*/Makefile|*/_CoqProject)
             check_file "$file" "${POUND_HEADER[@]}"
             ;;
         *.md)