Update 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:
@@ -28,8 +28,6 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.16'
-          - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
@@ -40,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))

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/math-comp/mczify/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/mczify/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/math-comp/mczify/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/mczify/actions/workflows/docker-action.yml
 
 
 

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"}

examples/test_ssreflect.v

@@ -106,27 +106,17 @@ Proof. zify_op; reflexivity. Qed.
 Fact test_eq_op_nat n m : (n == m) = Z.eqb (Z.of_nat n) (Z.of_nat m).
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_addn_rec n m : Z.of_nat (n + m)%Nrec = (Z.of_nat n + Z.of_nat m)%Z.
-Proof. zify_op; reflexivity. Qed.
-
 Fact test_addn n m : Z.of_nat (n + m) = (Z.of_nat n + Z.of_nat m)%Z.
 Proof. zify_op; reflexivity. Qed.
 
 Fact test_addn_trec n m :
   Z.of_nat (NatTrec.add n m) = (Z.of_nat n + Z.of_nat m)%Z.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_subn_rec n m :
-  Z.of_nat (n - m)%Nrec = Z.max 0 (Z.of_nat n - Z.of_nat m).
-Proof. zify_op; reflexivity. Qed.
-
 Fact test_subn n m :
   Z.of_nat (n - m) = Z.max 0 (Z.of_nat n - Z.of_nat m).
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_muln_rec n m : Z.of_nat (n * m)%Nrec = (Z.of_nat n * Z.of_nat m)%Z.
-Proof. zify_op; reflexivity. Qed.
-
 Fact test_muln n m : Z.of_nat (n * m) = (Z.of_nat n * Z.of_nat m)%Z.
 Proof. zify_op; reflexivity. Qed.
 

meta.yml

@@ -53,10 +53,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.16'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.17'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.19'
@@ -75,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