Merge pull request #299 from proux01/master_815

Master branch compiles on Coq 8.15

.github/workflows/main.yml

@@ -17,16 +17,14 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
+          - '8.15'
           - '8.16'
-        ocaml_version:
-          - '4.09-flambda'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1
       with:
         opam_file: './coq-hierarchy-builder.opam'
         coq_version: ${{ matrix.coq_version }}
-        ocaml_version: ${{ matrix.ocaml_version }}
         export: 'OPAMWITHTEST'  # space-separated list of variables
       env:
         OPAMWITHTEST: 'true'

coq-hierarchy-builder-shim.opam

@@ -11,7 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
 build: [ make "-C" "shim" "build" ]
 install: [ make "-C" "shim" "install" ]
 conflicts: [ "coq-hierarchy-builder" ]
-depends: [ "coq" {>= "8.10"} ]
+depends: [ "coq-elpi" { (>= "1.14" & < "1.16~") | = "dev" } ]
 synopsis: "Shim package for HB"
 description: """
 This package provide the support constants one can use to compile files

coq-hierarchy-builder.opam

@@ -12,7 +12,7 @@ build: [ [ make "build"]
          [ make "test-suite" ] {with-test}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" { (>= "1.15.1" & < "1.16~") | = "dev" } ]
+depends: [ "coq-elpi" { (>= "1.14" & < "1.16~") | = "dev" } ]
 conflicts: [ "coq-hierarchy-builder-shim" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """

tests/about.v.out.15

@@ -0,0 +1,142 @@
+HB: AddMonoid_of_TYPE is a factory
+    (from "./examples/demo1/hierarchy_5.v", line 10)
+HB: AddMonoid_of_TYPE operations and axioms are:
+    - zero
+    - add
+    - addrA
+    - add0r
+    - addr0
+HB: AddMonoid_of_TYPE requires the following mixins:
+HB: AddMonoid_of_TYPE provides the following mixins:
+    - hierarchy_5.AddMonoid_of_TYPE
+
+HB: AddMonoid_of_TYPE.Build is a factory constructor
+    (from "./examples/demo1/hierarchy_5.v", line 10)
+HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with:
+HB: AddMonoid_of_TYPE.Build provides the following mixins:
+    - hierarchy_5.AddMonoid_of_TYPE
+HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0
+    - S : Type
+    - zero : AddMonoid.sort S
+    - add : S -> S -> S
+    - addrA : associative add
+    - add0r : left_id 0%G add
+    - addr0 : right_id 0%G add
+
+HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
+HB: AddAG.type characterizing operations and axioms are:
+    - addNr
+    - opp
+HB: hierarchy_5.AddAG is a factory for the following mixins:
+    - hierarchy_5.AddMonoid_of_TYPE
+    - hierarchy_5.AddComoid_of_AddMonoid
+    - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *)
+HB: hierarchy_5.AddAG inherits from:
+    - hierarchy_5.AddMonoid
+    - hierarchy_5.AddComoid
+HB: hierarchy_5.AddAG is inherited by:
+    - hierarchy_5.Ring
+
+HB: hierarchy_5.AddMonoid.type is a structure
+    (from "./examples/demo1/hierarchy_5.v", line 17)
+HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are:
+    - addr0
+    - add0r
+    - addrA
+    - add
+    - zero
+HB: hierarchy_5.AddMonoid is a factory for the following mixins:
+    - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *)
+HB: hierarchy_5.AddMonoid inherits from:
+HB: hierarchy_5.AddMonoid is inherited by:
+    - hierarchy_5.AddComoid
+    - hierarchy_5.AddAG
+    - hierarchy_5.BiNearRing
+    - hierarchy_5.SemiRing
+    - hierarchy_5.Ring
+
+HB: Ring_of_AddAG is a factory
+    (from "./examples/demo1/hierarchy_5.v", line 108)
+HB: Ring_of_AddAG operations and axioms are:
+    - one
+    - mul
+    - mulrA
+    - mulr1
+    - mul1r
+    - mulrDl
+    - mulrDr
+HB: Ring_of_AddAG requires the following mixins:
+    - hierarchy_5.AddMonoid_of_TYPE
+    - hierarchy_5.AddComoid_of_AddMonoid
+    - hierarchy_5.AddAG_of_AddComoid
+HB: Ring_of_AddAG provides the following mixins:
+    - hierarchy_5.BiNearRing_of_AddMonoid
+Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
+     mul0r are derived from addrC and the other ring axioms, following a proof
+     of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
+     theory. In Near-rings and near-fields. Proceedings of the conference held
+     in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
+     and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
+     1995).
+
+HB: Ring_of_AddAG.Build is a factory constructor
+    (from "./examples/demo1/hierarchy_5.v", line 108)
+HB: Ring_of_AddAG.Build requires its subject to be already equipped with:
+    - hierarchy_5.AddMonoid_of_TYPE
+    - hierarchy_5.AddComoid_of_AddMonoid
+    - hierarchy_5.AddAG_of_AddComoid
+HB: Ring_of_AddAG.Build provides the following mixins:
+    - hierarchy_5.BiNearRing_of_AddMonoid
+HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr
+    - A : Type
+    - one : A
+    - mul : A -> A -> A
+    - mulrA : associative mul
+    - mulr1 : left_id one mul
+    - mul1r : right_id one mul
+    - mulrDl : left_distributive mul add
+    - mulrDr : right_distributive mul add
+Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
+     mul0r are derived from addrC and the other ring axioms, following a proof
+     of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
+     theory. In Near-rings and near-fields. Proceedings of the conference held
+     in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
+     and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
+     1995).
+
+HB: add is an operation of structure hierarchy_5.AddMonoid
+    (from "./examples/demo1/hierarchy_5.v", line 17)
+HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE
+    (from "./examples/demo1/hierarchy_5.v", line 10)
+
+HB: AddAG.sort is a canonical projection
+    (from "./examples/demo1/hierarchy_5.v", line 73)
+HB: AddAG.sort has the following canonical values:
+    - @eta 
+    - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
+    - Z 
+
+HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass
+    (from "./examples/demo1/hierarchy_5.v", line 73)
+
+HB: Z is canonically equipped with mixins:
+    - hierarchy_5.AddMonoid
+      hierarchy_5.AddComoid
+      hierarchy_5.AddAG
+      (from "(stdin)", line 5)
+    - hierarchy_5.BiNearRing
+      hierarchy_5.SemiRing
+      hierarchy_5.Ring
+      (from "(stdin)", line 10)
+
+HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
+    hierarchy_5.Ring to hierarchy_5.SemiRing
+    (from "./examples/demo1/hierarchy_5.v", line 196)
+
+HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
+    hierarchy_5.Ring to hierarchy_5.SemiRing
+    (from "./examples/demo1/hierarchy_5.v", line 196)
+
+HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to 
+hierarchy_5.BiNearRing_of_AddMonoid
+HB: synthesized in file File "(stdin)", line 5, column 122, character 127: