Run Rocq tests.

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