From 610d3d05669ad209c60da0f0515de4a5dc07fba4 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 28 May 2024 15:00:55 +0200 Subject: [PATCH 1/3] Update CI --- .github/workflows/docker-action.yml | 2 -- README.md | 4 ++-- meta.yml | 4 ---- 3 files changed, 2 insertions(+), 8 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index db1a18d..abdfe98 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -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' diff --git a/README.md b/README.md index ca1f6ab..aa95f5f 100644 --- a/README.md +++ b/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 diff --git a/meta.yml b/meta.yml index d66ce68..343825f 100644 --- a/meta.yml +++ b/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' From 0132827d185d646f734062d72f1bce8900615e60 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 28 May 2024 15:20:20 +0200 Subject: [PATCH 2/3] Remove the broken test cases --- examples/test_ssreflect.v | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/examples/test_ssreflect.v b/examples/test_ssreflect.v index 07e6ce4..872fcbb 100644 --- a/examples/test_ssreflect.v +++ b/examples/test_ssreflect.v @@ -106,9 +106,6 @@ 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. @@ -116,17 +113,10 @@ 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. From 6b429f0822076bde272b883f3940154c74771908 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 28 May 2024 15:47:52 +0200 Subject: [PATCH 3/3] Simplify the test-suite infrastructure in CI --- .github/workflows/docker-action.yml | 16 +++++----------- Make.test-suite | 1 + Makefile | 10 +--------- coq-mathcomp-zify.opam | 1 + meta.yml | 6 ++++++ 5 files changed, 14 insertions(+), 20 deletions(-) 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