Merge branch 'mathcomp-2.0.0'

.circleci/config.yml

@@ -46,76 +46,49 @@ commands:
           opam install --with-test .
 
 jobs:
-  coq-8-11:
+  coq-8-17-mathcomp-2-0-0:
     <<: *defaults
     steps:
     - startup
     - prepare:
-        mathcomp-version: '1.11.0'
+        mathcomp-version: '2.0.0'
     - build
     docker:
-    - image: coqorg/coq:8.11
-    resource_class: large
-
-  coq-8-12-mathcomp-1-11-0:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare:
-        mathcomp-version: '1.11.0'
-    - build
-    docker:
-    - image: coqorg/coq:8.12
-
-  coq-8-13-mathcomp-1-13-0:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare:
-        mathcomp-version: '1.13.0'
-    - build
-    docker:
-    - image: coqorg/coq:8.13
-
-  coq-8-14-mathcomp-1-13-0:
-    <<: *defaults
-    steps:
-    - startup
-    - prepare:
-        mathcomp-version: '1.13.0'
-    - build
-    docker:
-    - image: coqorg/coq:8.14
+    - image: coqorg/coq:8.17
+    resource_class: 'large'
 
-  coq-8-15-mathcomp-1-15-0:
+  coq-8-17-mathcomp-dev:
     <<: *defaults
     steps:
     - startup
     - prepare:
-        mathcomp-version: '1.15.0'
+        mathcomp-version: 'dev'
     - build
     docker:
-    - image: coqorg/coq:8.15
+    - image: coqorg/coq:8.17
+    resource_class: 'large'
 
-  coq-8-16-mathcomp-1-16-0:
+  coq-8-18-mathcomp-2-0-0:
     <<: *defaults
     steps:
     - startup
     - prepare:
-        mathcomp-version: '1.16.0'
+        mathcomp-version: '2.0.0'
     - build
     docker:
-    - image: coqorg/coq:8.16
+    - image: coqorg/coq:8.18
+    resource_class: 'large'
 
-  coq-8-17-mathcomp-dev:
+  coq-8-18-mathcomp-dev:
     <<: *defaults
     steps:
     - startup
     - prepare:
         mathcomp-version: 'dev'
     - build
     docker:
-    - image: coqorg/coq:8.17
+    - image: coqorg/coq:8.18
+    resource_class: 'large'
 
   coq-dev:
     <<: *defaults
@@ -126,15 +99,13 @@ jobs:
     - build
     docker:
     - image: coqorg/coq:dev
+  resource_class: 'large'
 
 workflows:
   build:
     jobs:
-    - coq-8-11
-    - coq-8-12-mathcomp-1-11-0
-    - coq-8-13-mathcomp-1-13-0
-    - coq-8-14-mathcomp-1-13-0
-    - coq-8-15-mathcomp-1-15-0
-    - coq-8-16-mathcomp-1-16-0
+    - coq-8-17-mathcomp-2-0-0
     - coq-8-17-mathcomp-dev
+    - coq-8-18-mathcomp-2-0-0
+    - coq-8-18-mathcomp-dev
     - coq-dev

.gitignore

@@ -8,3 +8,8 @@ CoqMakefile
 CoqMakefile.conf
 theories/tactics.v
 .dir-locals.el
+.direnv
+.envrc
+make_tactics
+make_tactics.cmo
+make_tactics.cmi

CHANGELOG.md

@@ -6,6 +6,22 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Changed
+- Make Deriving compatible with Hierarchy Builder and MathComp 2.0.0.
+
+- Following the changes of terminology in MathComp, the syntax for deriving the
+  base mixins has now the form `[derive [<flag>] <mixin> for <type>]`, where
+  + `<flag>` is one of `red`, `nored` or `lazy`.
+  + `<mixin>` is one of `hasDecEq`, `hasChoice`, `isCountable`, `isFinite` or
+    `isOrder`.
+
+### Deprecated
+
+- The derivation forms `[derive ...]` that mention the old MathComp mixin names
+  `eqMixin`, `choiceMixin`, `countMixin`, `finMixin` and `orderMixin` are
+  deprecated.  Use the new names for those mixins, as explained in the previous
+  section.
+
 ## [0.1.1] - 2023-03-10
 ### Fixed
 - Add `global` locality annotations to comply with newer versions of Coq

README.md

@@ -6,6 +6,7 @@ The Deriving library builds instances of basic MathComp classes for inductive
 data types with little boilerplate, akin to Haskell's `deriving` functionality.
 To define an `eqType` instance for a type `foo`, just write:
 
+    From HB Require Import structures.
     From mathcomp Require Import ssreflect ssrnat eqtype.
     From deriving Require Import deriving.
 
@@ -15,8 +16,8 @@ To define an `eqType` instance for a type `foo`, just write:
     Definition foo_indDef := [indDef for foo_rect].
     Canonical foo_indType := IndType foo foo_indDef.
 
-    Definition foo_eqMixin := [derive eqMixin for foo].
-    Canonical foo_eqType := EqType foo foo_eqMixin.
+    Definition foo_hasDecEq := [derive hasDecEq for foo].
+    HB.instance Definition _ := foo_hasDecEq.
 
 ## Supported types and limitations
 
@@ -72,17 +73,17 @@ instances as much as possible, to make them more similar to hand-written code.
 However, this process can be too slow for large definitions, so it can be
 disabled with the `nored` flag:
 
-    Definition large_type_eqMixin : Equality.mixin_of large_type.
-    Proof. exact [derive nored eqMixin for large_type]. Qed.
+    Definition large_type_hasDecEq : Equality.mixin_of large_type.
+    Proof. exact [derive nored hasDecEq for large_type]. Qed.
 
 In such cases, it is a good idea to keep the instance opaque (e.g. defined with
 `Qed`) to avoid slowdown.
 
 ## Requirements
 
-- Coq 8.11 -- 8.17
+- Coq 8.17
 
-- `coq-mathcomp-ssreflect` 1.11 -- 1.16
+- `coq-mathcomp-ssreflect` 2.0.0
 
 ## Installation
 

TODO.org

@@ -1,3 +1,8 @@
-* Support mutually inductive types
 * Documentation
 * Clean up code
+* Ensure equality and order operations are simplified properly
+* Check why it is not possible to derive the mixin directly in the instance
+E.g. this does not work:
+HB.instance Definition _ := [derive eqMixin for foo].
+* Find a better way of writing packing functions (cf. infer.v and the derive notation in eqtype.v)
+* By default, [derive nored eqMixin for ...] does not simplify the type of the mixin

_CoqProject

@@ -3,6 +3,8 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -non-reversible-notation
 -arg -w -arg -ssr-search-moved
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
 
 theories/base.v
 theories/ind.v

deriving.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "coq-deriving"
-version: "0.1.1"
+version: "dev"
 maintainer: "Arthur Azevedo de Amorim <[email protected]>"
 
 homepage: "https://github.com/arthuraa/deriving"
@@ -11,8 +11,8 @@ license: "MIT"
 build: [ make "-j" "%{jobs}%" "test" {with-test} ]
 install: [ make "install" ]
 depends: [
-  "coq" { (>= "8.11" & < "8.18~") | (= "dev") }
-  "coq-mathcomp-ssreflect" {>= "1.11" | (= "dev")}
+  "coq" { (>= "8.17" & < "8.19~") | (= "dev") }
+  "coq-mathcomp-ssreflect" {>= "2.0" | (= "dev")}
 ]
 
 tags: [

flake.nix

@@ -0,0 +1,33 @@
+{
+  description = ''
+    Deriving provides generic instances of MathComp classes for
+    inductive data types.  It includes native support for eqType,
+    choiceType, countType and finType instances, and it allows users to
+    define their own instances for other classes.
+  '';
+
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+
+  outputs = { self, nixpkgs, flake-utils }:
+    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:
+                { mathcomp = super.mathcomp.override {
+                    version = "2.0.0";
+                  };
+                  deriving = super.deriving.overrideAttrs {
+                    version = "0.2.0";
+                    src = ./.;
+                  };
+                });
+              ocaml = pkgs.ocaml;
+            };
+
+            devShell = pkgs.mkShell {
+              packages = with packages; [ coq coqPackages.mathcomp.ssreflect ocaml ];
+            };
+      }
+    );
+}

tests/mutual.v

@@ -1,3 +1,5 @@
+From HB Require Import structures.
+
 From mathcomp Require Import
   ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype finset order.
 
@@ -31,36 +33,29 @@ Canonical foo_indType := IndType foo foo_bar_baz_indDef.
 Canonical bar_indType := IndType bar foo_bar_baz_indDef.
 Canonical baz_indType := IndType baz foo_bar_baz_indDef.
 
-Definition foo_eqMixin := [derive lazy eqMixin for foo].
-Canonical foo_eqType := EqType foo foo_eqMixin.
-Definition bar_eqMixin := [derive lazy eqMixin for bar].
-Canonical bar_eqType := EqType bar bar_eqMixin.
-Definition baz_eqMixin := [derive lazy eqMixin for baz].
-Canonical baz_eqType := EqType baz baz_eqMixin.
-Definition foo_choiceMixin := [derive choiceMixin for foo].
-Canonical foo_choiceType := Eval hnf in ChoiceType foo foo_choiceMixin.
-Definition bar_choiceMixin := [derive choiceMixin for bar].
-Canonical bar_choiceType := Eval hnf in ChoiceType bar bar_choiceMixin.
-Definition baz_choiceMixin := [derive choiceMixin for baz].
-Canonical baz_choiceType := Eval hnf in ChoiceType baz baz_choiceMixin.
-Definition foo_countMixin := [derive countMixin for foo].
-Canonical foo_countType := Eval hnf in CountType foo foo_countMixin.
-Definition bar_countMixin := [derive countMixin for bar].
-Canonical bar_countType := Eval hnf in CountType bar bar_countMixin.
-Definition baz_countMixin := [derive countMixin for baz].
-Canonical baz_countType := Eval hnf in CountType baz baz_countMixin.
-Definition foo_orderMixin := [derive lazy orderMixin for foo].
-Canonical foo_porderType := Eval hnf in POrderType tt foo foo_orderMixin.
-Canonical foo_latticeType := Eval hnf in LatticeType foo foo_orderMixin.
-Canonical foo_distrLatticeType := Eval hnf in DistrLatticeType foo foo_orderMixin.
-Canonical foo_orderType := Eval hnf in OrderType foo foo_orderMixin.
-Definition bar_orderMixin := [derive lazy orderMixin for bar].
-Canonical bar_porderType := Eval hnf in POrderType tt bar bar_orderMixin.
-Canonical bar_latticeType := Eval hnf in LatticeType bar bar_orderMixin.
-Canonical bar_distrLatticeType := Eval hnf in DistrLatticeType bar bar_orderMixin.
-Canonical bar_orderType := Eval hnf in OrderType bar bar_orderMixin.
-Definition baz_orderMixin := [derive lazy orderMixin for baz].
-Canonical baz_porderType := Eval hnf in POrderType tt baz baz_orderMixin.
-Canonical baz_latticeType := Eval hnf in LatticeType baz baz_orderMixin.
-Canonical baz_distrLatticeType := Eval hnf in DistrLatticeType baz baz_orderMixin.
-Canonical baz_orderType := Eval hnf in OrderType baz baz_orderMixin.
+(* FIXME: Why aren't the recursors being simplified away here? *)
+Definition foo_hasDecEq := [derive hasDecEq for foo].
+HB.instance Definition _ := foo_hasDecEq.
+Definition bar_hasDecEq := [derive hasDecEq for bar].
+HB.instance Definition _ := bar_hasDecEq.
+Definition baz_hasDecEq := [derive hasDecEq for baz].
+HB.instance Definition _ := baz_hasDecEq.
+Definition foo_hasChoice := [derive hasChoice for foo].
+HB.instance Definition _ := foo_hasChoice.
+Definition bar_hasChoice := [derive hasChoice for bar].
+HB.instance Definition _ := bar_hasChoice.
+Definition baz_hasChoice := [derive hasChoice for baz].
+HB.instance Definition _ := baz_hasChoice.
+Definition foo_isCountable := [derive isCountable for foo].
+HB.instance Definition _ := foo_isCountable.
+Definition bar_isCountable := [derive isCountable for bar].
+HB.instance Definition _ := bar_isCountable.
+Definition baz_isCountable := [derive isCountable for baz].
+HB.instance Definition _ := baz_isCountable.
+(* FIXME: Why aren't the recursors being simplified away here? *)
+Definition foo_isOrder := [derive isOrder for foo].
+HB.instance Definition _ := foo_isOrder.
+Definition bar_isOrder := [derive isOrder for bar].
+HB.instance Definition _ := bar_isOrder.
+Definition baz_isOrder := [derive isOrder for baz].
+HB.instance Definition _ := baz_isOrder.