Merge pull request #98 from math-comp/ci

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 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:
@@ -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-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

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/algebra-tactics/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/algebra-tactics/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/math-comp/algebra-tactics/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/algebra-tactics/actions/workflows/docker-action.yml
 
 
 

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

@@ -68,10 +68,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'
@@ -100,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