Merge pull request #65 from math-comp/release

Prepare for a release

Author: pi8027

.github/workflows/docker-action.yml

@@ -17,33 +17,21 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
           - 'mathcomp/mathcomp:2.3.0-coq-8.18'
           - 'mathcomp/mathcomp:2.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-coq-8.19'
           - 'mathcomp/mathcomp:2.4.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.20'
           - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-mathcomp-zify.opam'
+          opam_file: 'rocq-mathcomp-zify.opam'
           custom_image: ${{ matrix.image }}
           export: 'OPAMWITHTEST'
         env:

Make

@@ -4,4 +4,5 @@ theories/zify_algebra.v
 theories/zify.v
 
 -R theories mathcomp.zify
+-arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden

Makefile.coq.local

@@ -0,0 +1,7 @@
+pre-all::
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	  for f in $(shell grep "From Stdlib" $$(find . -name "*.v") | cut -d: -f1) ; do \
+	    sed -i.bak 's/From Stdlib/From Coq/' $${f} ; \
+	    $(RM) $${f}.bak ; \
+	  done ; \
+	fi

README.md

@@ -21,11 +21,11 @@ by extending the zify tactic.
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Coq versions: 8.16 or later
+- Compatible Rocq/Coq versions: 8.18 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) ssreflect 2.0 or later
+  - [MathComp](https://math-comp.github.io) ssreflect 2.3 or later
   - [MathComp](https://math-comp.github.io) algebra
-- Coq namespace: `mathcomp.zify`
+- Rocq/Coq namespace: `mathcomp.zify`
 - Related publication(s): none
 
 ## Building and installation instructions
@@ -35,7 +35,7 @@ is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq-mathcomp-zify
+opam install rocq-mathcomp-zify
 ```
 
 To instead build and install manually, do:

_CoqProject

@@ -1,2 +1,3 @@
 -R theories mathcomp.zify
+-arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden

coq-mathcomp-zify.opam

@@ -1,33 +1,18 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
-maintainer: "kazuhiko.sakaguchi@inria.fr"
+maintainer: "kazuhiko.sakaguchi@ens-lyon.fr"
 version: "dev"
 
 homepage: "https://github.com/math-comp/mczify"
 dev-repo: "git+https://github.com/math-comp/mczify.git"
 bug-reports: "https://github.com/math-comp/mczify/issues"
 license: "CECILL-B"
 
-synopsis: "Micromega tactics for Mathematical Components"
-description: """
-This small library enables the use of the Micromega arithmetic solvers of Coq
-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"}
-  "coq-mathcomp-ssreflect" {>= "2.0"}
-  "coq-mathcomp-algebra" 
-]
-
+depends: [ "rocq-mathcomp-zify" { = version } ]
 tags: [
   "logpath:mathcomp.zify"
 ]
 authors: [
   "Kazuhiko Sakaguchi"
 ]
+
+synopsis: "Compatibility package for rocq-mathcomp-zify"

meta.yml

@@ -1,7 +1,7 @@
 ---
 fullname: Mczify
 shortname: mczify
-opam_name: coq-mathcomp-zify
+opam_name: rocq-mathcomp-zify
 organization: math-comp
 action: true
 
@@ -17,42 +17,20 @@ authors:
 - name: Kazuhiko Sakaguchi
   initial: true
 
-opam-file-maintainer: kazuhiko.sakaguchi@inria.fr
+opam-file-maintainer: kazuhiko.sakaguchi@ens-lyon.fr
 
 license:
   fullname: CeCILL-B Free Software License Agreement
   identifier: CECILL-B
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.16 or later
-  opam: '{>= "8.16"}'
+  text: 8.18 or later
+  opam: '{>= "8.18"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.19'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.19'
@@ -67,8 +45,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.20'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'rocq-prover-9.0'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'rocq-prover-dev'
@@ -77,9 +53,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "2.0"}'
+    version: '{>= "2.3"}'
   description: |-
-    [MathComp](https://math-comp.github.io) ssreflect 2.0 or later
+    [MathComp](https://math-comp.github.io) ssreflect 2.3 or later
 - opam:
     name: coq-mathcomp-algebra
   description: |-

rocq-mathcomp-zify.opam

@@ -0,0 +1,33 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "[email protected]"
+version: "dev"
+
+homepage: "https://github.com/math-comp/mczify"
+dev-repo: "git+https://github.com/math-comp/mczify.git"
+bug-reports: "https://github.com/math-comp/mczify/issues"
+license: "CECILL-B"
+
+synopsis: "Micromega tactics for Mathematical Components"
+description: """
+This small library enables the use of the Micromega arithmetic solvers of Coq
+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.18"}
+  "coq-mathcomp-ssreflect" {>= "2.3"}
+  "coq-mathcomp-algebra" 
+]
+
+tags: [
+  "logpath:mathcomp.zify"
+]
+authors: [
+  "Kazuhiko Sakaguchi"
+]

theories/ssrZ.v

@@ -1,4 +1,4 @@
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
@@ -37,38 +37,6 @@ Qed.
 
 Module Instances.
 
-(* Instances taken from math-comp/math-comp#1031, authored by Pierre Roux *)
-(* TODO: remove them when we drop support for MathComp 2.0 *)
-#[export]
-HB.instance Definition _ := GRing.isNmodule.Build nat addnA addnC add0n.
-
-#[export]
-HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build nat
-  mulnA mulnC mul1n mulnDl mul0n erefl.
-
-#[export]
-HB.instance Definition _ (V : nmodType) (x : V) :=
-  GRing.isSemiAdditive.Build nat V (GRing.natmul x) (mulr0n x, mulrnDr x).
-
-#[export]
-HB.instance Definition _ (R : semiRingType) :=
-  GRing.isMultiplicative.Build nat R (GRing.natmul 1) (natrM R, mulr1n 1).
-
-Fact Posz_is_semi_additive : semi_additive Posz.
-Proof. by []. Qed.
-
-#[export]
-HB.instance Definition _ := GRing.isSemiAdditive.Build nat int Posz
-  Posz_is_semi_additive.
-
-Fact Posz_is_multiplicative : multiplicative Posz.
-Proof. by []. Qed.
-
-#[export]
-HB.instance Definition _ := GRing.isMultiplicative.Build nat int Posz
-  Posz_is_multiplicative.
-(* end *)
-
 #[export]
 HB.instance Definition _ := Countable.copy N (can_type nat_of_binK).
 

theories/zify.v

@@ -1,4 +1,4 @@
-From Coq Require Export Lia.
+From Stdlib Require Export Lia.
 From mathcomp Require Import zify_ssreflect zify_algebra.
 Export SsreflectZifyInstances.Exports.
 Export AlgebraZifyInstances.Exports.