Move tests requiring Stdlib to separate directories

Co-authored-by: Enrico Tassi <[email protected]>

Author: proux01

.gitignore

@@ -55,4 +55,6 @@ _build
 tmp.out
 coq-elpi-tests.opam
 coq-elpi-tests.install
-coq-elpi.install
+coq-elpi.install
+
+theories-stdlib/dune

Makefile

@@ -10,44 +10,66 @@ elpi/dune: elpi/dune.in
 	fi
 	@chmod a-w $@
 
-all: elpi/dune
+all: elpi/dune theories-stdlib/dune
 	$(call dune,build)
 	$(call dune,build) builtin-doc
 .PHONY: all
 
-build-core: elpi/dune
+build-core: elpi/dune theories-stdlib/dune
 	$(call dune,build) theories
 	$(call dune,build) builtin-doc
 .PHONY: build-core
 
-build-apps: elpi/dune
+build-apps: elpi/dune theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name theories)
 .PHONY: build-apps
 
-build: elpi/dune
+build: elpi/dune theories-stdlib/dune
 	$(call dune,build) -p coq-elpi @install
 	$(call dune,build) builtin-doc
 .PHONY: build
 
-test-core: elpi/dune
+all-tests: test-core test-stdlib test-apps test-apps-stdlib
+.PHONY: all-tests
+
+test-core: elpi/dune theories-stdlib/dune
 	$(call dune,runtest) tests
 	$(call dune,build) tests
 .PHONY: test-core
 
-test-apps: elpi/dune
+test-apps: elpi/dune theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test-apps
 
-test: elpi/dune
-	$(call dune,runtest)
-	$(call dune,build) tests
-	$(call dune,build) $$(find apps -type d -name tests)
-.PHONY: test
+test-apps-stdlib: elpi/dune theories-stdlib/dune
+	$(call dune,build) $$(find apps -type d -name tests-stdlib)
+.PHONY: test-apps-stdlib
+
+test-stdlib: elpi/dune theories-stdlib/dune
+	$(call dune,build) tests-stdlib
+.PHONY: test-stdlib
 
-examples: elpi/dune
+all-examples: examples examples-stdlib
+.PHONY: all-examples
+
+examples: elpi/dune theories-stdlib/dune
 	$(call dune,build) examples
 .PHONY: examples
 
+examples-stdlib: elpi/dune theories-stdlib/dune
+	$(call dune,build) examples-stdlib
+.PHONY: examples-stdlib
+
+theories-stdlib/dune: theories-stdlib/dune.in
+	@rm -f $@
+	@echo "; generated by make, do not edit" > $@
+	@if $$(coqc --version | grep -q "8.19\|8.20") ; then \
+		sed -e 's/@@STDLIB@@//' $< >> $@ ; \
+	else \
+		sed -e 's/@@STDLIB@@/Stdlib/' $< >> $@ ; \
+	fi
+	@chmod a-w $@
+
 doc: build
 	@echo "########################## generating doc ##########################"
 	@mkdir -p doc

apps/derive/tests-stdlib/dune

@@ -0,0 +1,7 @@
+(coq.theory
+ (package coq-elpi-tests-stdlib)
+ (name elpi_apps_derive_tests_stdlib)
+ (flags :standard -w -default-output-directory)
+ (theories elpi elpi.apps.derive elpi.apps.derive.tests elpi_stdlib))
+
+(include_subdirs qualified)

apps/derive/tests/test_derive.v renamed to apps/derive/tests-stdlib/test_derive.v

@@ -170,7 +170,3 @@ End derive_container.
 About wimpls.wimpls.
 About wimpls.Kwi.
 Redirect "tmp" Check Kwi _ (refl_equal 3).
-
-From Coq Require Ascii.
-
-#[only(param2)] derive Ascii.ascii.

apps/eltac/tests-stdlib/dune

@@ -0,0 +1,6 @@
+(coq.theory
+ (package coq-elpi-tests-stdlib)
+ (name elpi_apps_eltac_tests_stdlib)
+ (theories elpi elpi.apps.eltac elpi_stdlib))
+
+(include_subdirs qualified)

apps/eltac/tests/test_injection.v renamed to apps/eltac/tests-stdlib/test_injection.v

@@ -1,5 +1,5 @@
 (coq.theory
  (name elpi.apps.tc.examples)
- (theories elpi elpi.apps.tc))
+ (theories elpi elpi.apps.tc elpi_stdlib))
 
 (include_subdirs qualified)

apps/tc/examples/dune

@@ -1,4 +1,4 @@
-Require Import Bool.
+From elpi_stdlib Require Import Bool.
 From elpi.apps Require Import tc.
 
 Class Eqb (T: Type) := {
@@ -93,4 +93,5 @@ Module Backtrack.
 End Backtrack.
 
 TC.Print_instances.
-TC.Get_class_info DecidableClass.Decidable.
+(* Require Stdlib *)
+(* TC.Get_class_info DecidableClass.Decidable. *)

apps/tc/examples/tutorial.v

@@ -89,7 +89,7 @@ def buildTree(len):
 
 def writeFile(fileName: str, composeLen: int, isCoq: bool):
     PREAMBLE = f"""\
-From elpi.apps.tc.tests Require Import {"stdppInjClassic" if isCoq else "stdppInj"}.
+From elpi_apps_tc_tests_stdlib Require Import {"stdppInjClassic" if isCoq else "stdppInj"}.
 {"" if isCoq else 'Elpi TC.Solver. Set TC Time Refine. Set TC Time Instance Search. Set TC Time Build Query. Set Debug "elpitime".'}
 """
     GOAL = buildTree(composeLen)
@@ -130,4 +130,4 @@ def loopTreeDepth(file_name: str, maxHeight: int, makeCoq=True, onlyOne=False):
     height = int(sys.argv[1])
     loopTreeDepth(file_name, height, makeCoq=not (
         "-nocoq" in sys.argv), onlyOne=("-onlyOne" in sys.argv))
-    #writeFile(file_name, 1, False)
+    #writeFile(file_name, 1, False)

apps/tc/tests/bench/bench_inj.py renamed to apps/tc/tests-stdlib/bench/bench_inj.py

@@ -1,3 +1,3 @@
-From elpi.apps.tc.tests Require Import stdppInj.
+From elpi_apps_tc_tests_stdlib Require Import stdppInj.
 Elpi TC.Solver. Set TC Time Refine. Set TC Time Instance Search. Set Debug "elpitime".
 Goal Inj eq eq((compose f f )). Time apply _. Qed.