diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 37253cbbe..cc299f70e 100644 --- a/.github/workflows/main.yml +++ b/.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' diff --git a/coq-hierarchy-builder-shim.opam b/coq-hierarchy-builder-shim.opam index 9a190e591..935914113 100644 --- a/coq-hierarchy-builder-shim.opam +++ b/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 diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 70a22128b..d4ea65af1 100644 --- a/coq-hierarchy-builder.opam +++ b/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: """ diff --git a/tests/about.v.out.15 b/tests/about.v.out.15 new file mode 100644 index 000000000..a93916a7a --- /dev/null +++ b/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: