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 regenerate 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-zify.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

@@ -4,5 +4,6 @@ examples/zagier.v
 examples/test_ssreflect.v
 examples/test_algebra.v
 
+-R theories mathcomp.zify
 -I .
 -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.zify
-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,7 +17,7 @@ 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))

coq-mathcomp-zify.opam

@@ -17,6 +17,7 @@ for goals stated with the definitions of the Mathematical Components library
 by extending the zify tactic."""
 
 build: [make "-j%{jobs}%"]
+run-test: [make "-j%{jobs}%" "test-suite"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.16"}

meta.yml

@@ -71,8 +71,14 @@ dependencies:
   description: |-
     [MathComp](https://math-comp.github.io) algebra
 
+test_target: test-suite
 namespace: mathcomp.zify
 
+action_appendix: |2-
+            export: 'OPAMWITHTEST'
+          env:
+            OPAMWITHTEST: true
+
 documentation: |-
   ## File contents