Simplify the test-suite infrastructure in CI

.github/workflows/docker-action.yml

@@ -1,5 +1,5 @@
-# This file was generated from `meta.yml` using the coq-community templates and
-# then patched to support the test-suite. Be careful when regenerating it.
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
 name: Docker CI
 
 on:
@@ -38,15 +38,9 @@ jobs:
         with:
           opam_file: 'coq-mathcomp-algebra-tactics.opam'
           custom_image: ${{ matrix.image }}
-          after_script: |
-            startGroup "Run tests"
-              sudo chown -R coq:coq .
-              make test-suite TEST_SKIP_BUILD=1
-            endGroup
-      - name: Revert permissions
-        if: ${{ always() }}
-        run: sudo chown -R 1001:116 .
-
+          export: 'OPAMWITHTEST'
+        env:
+          OPAMWITHTEST: true
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

Make.test-suite

@@ -5,5 +5,6 @@ examples/ring_examples_no_check.v
 examples/from_sander.v
 examples/lra_examples.v
 
+-R theories mathcomp.algebra_tactics
 -R examples mathcomp.algebra_tactics.examples
 -arg -w -arg -notation-overridden

Makefile

@@ -9,14 +9,6 @@ KNOWNFILES   := Makefile Make Make.test-suite
 
 .DEFAULT_GOAL := invoke-coqmakefile
 
-ifneq "$(TEST_SKIP_BUILD)" ""
-TEST_DEP :=
-LIBRARY_PATH :=
-else
-TEST_DEP := invoke-coqmakefile
-LIBRARY_PATH := -R theories mathcomp.algebra_tactics
-endif
-
 COQMAKEFILE       = $(COQBIN)coq_makefile
 COQMAKE           = $(MAKE) --no-print-directory -f Makefile.coq
 COQMAKE_TESTSUITE = $(MAKE) --no-print-directory -f Makefile.test-suite.coq
@@ -25,12 +17,12 @@ Makefile.coq: Makefile Make
 	$(COQMAKEFILE) -f Make -o Makefile.coq
 
 Makefile.test-suite.coq: Makefile Make.test-suite
-	$(COQMAKEFILE) -f Make.test-suite $(LIBRARY_PATH) -o Makefile.test-suite.coq
+	$(COQMAKEFILE) -f Make.test-suite -o Makefile.test-suite.coq
 
 invoke-coqmakefile: Makefile.coq
 	$(COQMAKE) $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
 
-test-suite: Makefile.test-suite.coq $(TEST_DEP)
+test-suite: Makefile.test-suite.coq invoke-coqmakefile
 	$(COQMAKE_TESTSUITE)
 
 theories/%.vo: Makefile.coq

coq-mathcomp-algebra-tactics.opam

@@ -25,6 +25,7 @@ automatically push down ring morphisms and additive functions to leaves of
 ring/field expressions before applying the proof procedures."""
 
 build: [make "-j%{jobs}%"]
+run-test: [make "-j%{jobs}%" "test-suite"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.16"}

meta.yml

@@ -96,8 +96,14 @@ dependencies:
   description: |-
     [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later (known not to work with 1.17.0)
 
+test_target: test-suite
 namespace: mathcomp.algebra_tactics
 
+action_appendix: |2-
+            export: 'OPAMWITHTEST'
+          env:
+            OPAMWITHTEST: true
+
 documentation: |-
 
   ## Documentation