Merge pull request #31 from arthuraa/mathcomp-2.3.0-ci

Mathcomp 2.3.0 ci

.circleci/config.yml

@@ -101,6 +101,17 @@ jobs:
     - image: coqorg/coq:8.19
     resource_class: 'large'
 
+  coq-8-19-mathcomp-2-3-0:
+    <<: *defaults
+    steps:
+    - startup
+    - prepare:
+        mathcomp-version: '2.3.0'
+    - build
+    docker:
+    - image: coqorg/coq:8.19
+    resource_class: 'large'
+
   coq-8-19-mathcomp-dev:
     <<: *defaults
     steps:
@@ -131,5 +142,6 @@ workflows:
     - coq-8-18-mathcomp-2-0-0
     - coq-8-18-mathcomp-dev
     - coq-8-19-mathcomp-2-2-0
+    - coq-8-19-mathcomp-2-3-0
     - coq-8-19-mathcomp-dev
     - coq-dev

CHANGELOG.md

@@ -10,15 +10,21 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Changed
 
-- Use new display type for `orderType`, as in MathComp 2.3.0.  The generated
-  instances now use the default display.
-
 ### Deprecated
 
 ### Removed
 
 ### Fixed
 
+## [0.2.1] - 2024-12-02
+
+### Changed
+
+- Use new display type for `orderType`, as in MathComp 2.3.0.  The generated
+  instances now use the default display.
+
+### Fixed
+
 - Simplify the type of derived isFinite instances to avoid a non-forgetful
   inheritance warning.
 
@@ -48,7 +54,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 - First version supporting inductive types.
 
-[Unreleased]: https://github.com/arthuraa/deriving/compare/v0.2.0...HEAD
+[Unreleased]: https://github.com/arthuraa/deriving/compare/v0.2.1...HEAD
+[0.2.1]: https://github.com/arthuraa/deriving/releases/tag/v0.2.1
 [0.2.0]: https://github.com/arthuraa/deriving/releases/tag/v0.2.0
 [0.1.1]: https://github.com/arthuraa/deriving/releases/tag/v0.1.1
 [0.1.0]: https://github.com/arthuraa/deriving/releases/tag/v0.1.0

CoqMakefile.local

@@ -3,7 +3,7 @@ TESTVOFILES=$(TESTVFILES:.v=.vo)
 UNFOLDFILES = theories/ind.v theories/base.v
 
 theories/tactics.v: make_tactics.ml $(UNFOLDFILES)
-	ocaml str.cma make_tactics.ml $(UNFOLDFILES) > theories/tactics.v
+	ocaml -I +str str.cma make_tactics.ml $(UNFOLDFILES) > theories/tactics.v
 
 test: $(TESTVOFILES)
 .PHONY: test

README.md

@@ -81,9 +81,9 @@ In such cases, it is a good idea to keep the instance opaque (e.g. defined with
 
 ## Requirements
 
-- Coq 8.17 -- 8.18
+- Coq 8.17 -- 8.19
 
-- `coq-mathcomp-ssreflect` 2.0.0
+- `coq-mathcomp-ssreflect` 2.0.0 -- 2.3.0
 
 ## Installation
 

_CoqProject

@@ -11,6 +11,7 @@ theories/ind.v
 theories/tactics.v
 theories/infer.v
 theories/instances.v
+theories/compat.v
 theories/deriving.v
 
 theories/instances/eqtype.v

flake.nix

@@ -12,13 +12,13 @@
     flake-utils.lib.eachDefaultSystem (system:
       let pkgs = nixpkgs.legacyPackages.${system}; in rec {
             packages = rec {
-              coq = pkgs.coq_8_17;
-              coqPackages = pkgs.coqPackages_8_17.overrideScope' (self: super:
+              coq = pkgs.coq_8_19;
+              coqPackages = pkgs.coqPackages_8_19.overrideScope (self: super:
                 { mathcomp = super.mathcomp.override {
-                    version = "2.0.0";
+                    version = "2.2.0";
                   };
                   deriving = super.deriving.overrideAttrs {
-                    version = "0.2.0";
+                    version = "0.2.1";
                     src = ./.;
                   };
                 });

tests/syntax.v

@@ -154,9 +154,9 @@ HB.instance Definition _ := expr_isCountable.
 Definition val_isCountable :=
   [derive isCountable for val].
 HB.instance Definition _ := val_isCountable.
-Definition expr_isOrder : Order.isOrder tt expr.
+Definition expr_isOrder : Order.isOrder Order.default_display expr.
 Proof. exact: [derive nored isOrder for expr]. Qed.
 HB.instance Definition _ := expr_isOrder.
-Definition val_isOrder : Order.isOrder tt val.
+Definition val_isOrder : Order.isOrder Order.default_display val.
 Proof. exact: [derive nored isOrder for val]. Qed.
 HB.instance Definition _ := val_isOrder.

theories/base.v

@@ -1308,13 +1308,3 @@ Definition hnth1 m :=
 Coercion hnth1 : hlist1 >-> Funclass.
 #[global]
 Hint Unfold hnth1 : deriving.
-
-(* Compatibility layer for Order.disp_t introduced in MathComp 2.3            *)
-(* TODO: remove when we drop the support for MathComp 2.2                     *)
-Module Order.
-Import Order.
-Definition disp_t : Set.
-Proof. exact: disp_t || exact: unit. Defined.
-Definition default_display : disp_t.
-Proof. exact: tt || exact: Disp tt tt. Defined.
-End Order.

theories/compat.v

@@ -0,0 +1,18 @@
+From HB Require Import structures.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype order.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Set Primitive Projections.
+
+(* Compatibility layer for Order.disp_t introduced in MathComp 2.3            *)
+(* TODO: remove when we drop the support for MathComp 2.2                     *)
+Module Order.
+Import Order.
+Definition disp_t : Set.
+Proof. exact: disp_t || exact: unit. Defined.
+Definition default_display : disp_t.
+Proof. exact: tt || exact: Disp tt tt. Defined.
+End Order.

theories/deriving.v

@@ -1 +1 @@
-From deriving Require Export ind tactics infer instances.
+From deriving Require Export ind tactics infer instances compat.

theories/instances.v

@@ -2,7 +2,7 @@ From HB Require Import structures.
 From mathcomp Require Import
   ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype order.
 
-From deriving Require Import base ind tactics infer.
+From deriving Require Import base ind tactics infer compat.
 From deriving.instances Require Export eqtype tree_of_ind fintype order.
 
 From Coq Require Import ZArith NArith String Ascii.

theories/instances/order.v

@@ -1,7 +1,7 @@
 From mathcomp Require Import
   ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype order.
 
-From deriving Require Import base ind tactics infer.
+From deriving Require Import base ind tactics infer compat.
 
 From Coq Require Import ZArith NArith String Ascii.