diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index abdfe98..0acf050 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/Make.test-suite b/Make.test-suite index ec012dc..c7bc107 100644 --- a/Make.test-suite +++ b/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 diff --git a/Makefile b/Makefile index 1c48795..3964aef 100644 --- a/Makefile +++ b/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)) diff --git a/coq-mathcomp-zify.opam b/coq-mathcomp-zify.opam index e46251a..2fb6518 100644 --- a/coq-mathcomp-zify.opam +++ b/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"} diff --git a/meta.yml b/meta.yml index 343825f..e551d81 100644 --- a/meta.yml +++ b/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