diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 000000000..6f6ec7961 --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -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. +name: Docker CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'coqorg/coq:8.11' + - 'coqorg/coq:8.12' + - 'coqorg/coq:8.13' + fail-fast: false + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-hierarchy-builder.opam' + custom_image: ${{ matrix.image }} + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml deleted file mode 100644 index c6c3a7dc6..000000000 --- a/.github/workflows/main.yml +++ /dev/null @@ -1,31 +0,0 @@ -# This is a basic workflow to help you get started with Actions - -name: docker CI - -# Controls when the action will run. Triggers the workflow on push or pull request -# events but only for the master branch -on: - push: - branches: [ master ] - pull_request: - branches: [ master ] - -jobs: - opam: - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - coq_version: - - '8.11' - - '8.12' - - '8.13' - ocaml_version: - - 'minimal' - 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 }} diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml new file mode 100644 index 000000000..21a3d20af --- /dev/null +++ b/.github/workflows/nix-action.yml @@ -0,0 +1,125 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Nix CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + prerequisites: + runs-on: ubuntu-latest + + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + extraPullNames: coq + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Cache Nix Store + uses: actions/cache@v2.1.4 + id: cache-nix + with: + path: nix-store.nar + key: nix-${{ runner.os }}-${{ github.sha }} + restore-keys: | + nix-${{ runner.os }}- + - name: Import Nix Store + if: steps.cache-nix.outputs.cache-hit + run: nix-store --import < nix-store.nar + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Build + run: nix-build --arg ci true --arg ci-step 0 + - name: Compute Closure + run: nix-build --arg ci true --arg ci-step 0 | xargs nix path-info -r | tee closure.txt + - name: Export Nix Store + run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar + + main: + runs-on: ubuntu-latest + needs: prerequisites + + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + extraPullNames: coq + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Cache Nix Store + uses: actions/cache@v2.1.4 + id: cache-nix + with: + path: nix-store.nar + key: nix-${{ runner.os }}-${{ github.sha }} + restore-keys: | + nix-${{ runner.os }}- + - name: Import Nix Store + if: steps.cache-nix.outputs.cache-hit + run: nix-store --import < nix-store.nar + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Build + run: nix-build --arg ci true --arg ci-step 1 + - name: Compute Closure + run: nix-build --arg ci true --arg ci-step 1 | xargs nix path-info -r | tee closure.txt + - name: Export Nix Store + run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar + + CI: + runs-on: ubuntu-latest + needs: main + + steps: + - name: Cachix install + uses: cachix/install-nix-action@v12 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup + uses: cachix/cachix-action@v8 + with: + # Name of a cachix cache to pull/substitute + name: math-comp + extraPullNames: coq + authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' + - name: Cache Nix Store + uses: actions/cache@v2.1.4 + id: cache-nix + with: + path: nix-store.nar + key: nix-${{ runner.os }}-${{ github.sha }} + restore-keys: | + nix-${{ runner.os }}- + - name: Import Nix Store + if: steps.cache-nix.outputs.cache-hit + run: nix-store --import < nix-store.nar + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Build + run: nix-build --arg ci true --arg ci-step 2 + - name: Compute Closure + run: nix-build --arg ci true --arg ci-step 2 | xargs nix path-info -r | tee closure.txt + - name: Export Nix Store + run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar \ No newline at end of file diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml deleted file mode 100644 index 620901d27..000000000 --- a/.github/workflows/nix.yml +++ /dev/null @@ -1,80 +0,0 @@ -# This is a basic workflow to help you get started with Actions - -name: nix CI - -# Controls when the action will run. Triggers the workflow on push or pull request -# events but only for the master branch -on: - push: - branches: [ master ] - pull_request: - branches: [ master ] - -jobs: - hb: - runs-on: ubuntu-latest - - steps: - - name: Cachix install - uses: cachix/install-nix-action@v12 - - name: Cachix setup - uses: cachix/cachix-action@v8 - with: - name: math-comp - extraPullNames: coq - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - - name: Cache Nix Store - uses: actions/cache@v2.1.4 - id: cache-nix - with: - path: nix-store.nar - key: nix-${{ runner.os }}-${{ github.sha }} - restore-keys: | - nix-${{ runner.os }}- - - name: Import Nix Store - if: steps.cache-nix.outputs.cache-hit - run: nix-store --import < nix-store.nar - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - - name: Build - run: nix-build - - name: Compute Closure - run: nix path-info --all | tee closure.txt - - name: Export Nix Store - run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar - - mathcomp: - runs-on: ubuntu-latest - needs: hb - steps: - - name: Cachix install - uses: cachix/install-nix-action@v12 - - name: Cachix setup - uses: cachix/cachix-action@v8 - with: - name: math-comp - extraPullNames: coq - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - - name: Cache Nix Store - uses: actions/cache@v2.1.4 - id: cache-nix - with: - path: nix-store.nar - key: nix-${{ runner.os }}-${{ github.sha }} - restore-keys: | - nix-${{ runner.os }}- - - name: Import Nix Store - if: steps.cache-nix.outputs.cache-hit - run: nix-store --import < nix-store.nar - - name: Git checkout - uses: actions/checkout@v2 - with: - fetch-depth: 0 - - name: Build - run: nix-build --arg ci true - - name: Compute Closure - run: nix path-info --all | tee closure.txt - - name: Export Nix Store - run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix new file mode 100644 index 000000000..9cb6ea968 --- /dev/null +++ b/.nix/fallback-config.nix @@ -0,0 +1,5 @@ +{ + format = "1.0.0"; + coq-attribute = "hiearchy-builder"; + +} diff --git a/README.md b/README.md index ea1cf5612..2ad67e70a 100644 --- a/README.md +++ b/README.md @@ -1,11 +1,77 @@ -[![Actions Status](https://github.com/math-comp/hierarchy-builder/workflows/CI/badge.svg)](https://github.com/math-comp/hierarchy-builder/actions) -[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Buidlder) - + # Hierarchy Builder -High level commands to declare and evolve a hierarchy based on packed classes. +[![Docker CI][docker-action-shield]][docker-action-link] +[![Nix CI][nix-action-shield]][nix-action-link] +[![Chat][chat-shield]][chat-link] + +[docker-action-shield]: https://github.com/math-comp/hierarchy-builder/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/math-comp/hierarchy-builder/actions?query=workflow:"Docker%20CI" + +[nix-action-shield]: https://github.com/math-comp/hierarchy-builder/workflows/Nix%20CI/badge.svg?branch=master +[nix-action-link]: https://github.com/math-comp/hierarchy-builder/actions?query=workflow:"Nix%20CI" +[chat-shield]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg +[chat-link]: https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder + + + + +Hierarchy Builder is a high level language to build hierarchies of +algebraic structures and make these hierarchies evolve without breaking +user code. The key concepts are the ones of factory, builder and +abbreviation that let the hierarchy developer describe an actual +interface for their library. Behind that interface the developer can +provide appropriate code to ensure retro compatibility. + +## Meta + +- Author(s): + - Cyril Cohen (initial) + - Kazuhiko Sakaguchi (initial) + - Enrico Tassi (initial) +- License: [MIT](LICENSE) +- Compatible Coq versions: Coq 8.11 to 8.13 (or dev) +- Additional dependencies: + - [Coq elpi](https://github.com/LPCIC/coq-elpi) +- Coq namespace: `HB` +- Related publication(s): + - [Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi](https://hal.inria.fr/hal-02478907) doi:[10.4230/LIPIcs.FSCD.2020.34](https://doi.org/10.4230/LIPIcs.FSCD.2020.34) + - [Hierarchy Builder: FSCD Talk](https://www.youtube.com/watch?v=F6iRaTlQrlo)) + +## Building and installation instructions + +### Opam installation + +
(click to expand)

+ +The easiest way to install the latest released version of Hierarchy Builder +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-hierarchy-builder +``` + +

+ +### Manual installation + +
(click to expand)

+ +To instead build and install manually, do: + +``` shell +git clone https://github.com/math-comp/hierarchy-builder.git +cd hierarchy-builder +make # or make -j +make install VFILES=structures.v +``` + +

-[Presented at FSCD2020, talk available on youtube.](https://www.youtube.com/watch?v=F6iRaTlQrlo) ## Example @@ -74,21 +140,12 @@ The current version forces the carrier to be a type, ruling hierarchies of morph This [draft paper](https://hal.inria.fr/hal-02478907) describes the language in full detail. -#### Installation & availability +#### Alternative Installation instructions
(click to expand)

-HB works on Coq 8.10 and 8.11. - -- You can install it via OPAM - -```shell -opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-hierarchy-builder -``` +- You can use it in nix with the attribute `coqPackages_8_13.hierarchy-builder` e.g. via `nix-shell -p coq_8_13 -p coqPackages_8_13.hierarchy-builder` -- You can use it in nix with the attribute `coqPackages_8_11.hierarchy-builder` e.g. via `nix-shell -p coq_8_11 -p coqPackages_8_11.hierarchy-builder` -

#### Key concepts diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 3a31049a3..07e8f37ef 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -1,21 +1,37 @@ +# 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" -name: "coq-hierarchy-builder" -version: "dev" maintainer: "Enrico Tassi " -authors: [ "Cyril Cohen" "Kazuhiko Sakaguchi" "Enrico Tassi" ] -license: "MIT" +version: "dev" + homepage: "https://github.com/math-comp/hierarchy-builder" +dev-repo: "git+https://github.com/math-comp/hierarchy-builder.git" bug-reports: "https://github.com/math-comp/hierarchy-builder/issues" -dev-repo: "git+https://github.com/math-comp/hierarchy-builder" +license: "MIT" -build: [ make ] -install: [ make "install" "VFILES=structures.v" ] -depends: [ "coq-elpi" {>= "1.6" & < "1.9~"} ] -synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" +synopsis: "High level commands to declare and evolve a hierarchy based on packed classes." description: """ -Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these -hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder -and abbreviation that let the hierarchy developer describe an actual interface for their library. -Behind that interface the developer can provide appropriate code to ensure retro compatibility. -""" -tags: [ "logpath:HB" ] +Hierarchy Builder is a high level language to build hierarchies of +algebraic structures and make these hierarchies evolve without breaking +user code. The key concepts are the ones of factory, builder and +abbreviation that let the hierarchy developer describe an actual +interface for their library. Behind that interface the developer can +provide appropriate code to ensure retro compatibility.""" + +build: [ make "-j%{jobs}%" ] +install: [ make "install" "VFILES=structures.v" ] +depends: [ + "coq" { (>= "8.11" & < "8.14~") | (= "dev") } + "coq-elpi" {>= "1.6" & < "1.9~"} +] + +tags: [ + "keyword:algebraic hierarchy" + "logpath:HB" +] +authors: [ + "Cyril Cohen" + "Kazuhiko Sakaguchi" + "Enrico Tassi" +] diff --git a/default.nix b/default.nix index c382c517a..309024871 100644 --- a/default.nix +++ b/default.nix @@ -1,3 +1,5 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, update-nixpkgs ? false, ci ? false, ci-step ? null, inNixShell ? null }@args: diff --git a/meta.yml b/meta.yml new file mode 100644 index 000000000..94dbc427c --- /dev/null +++ b/meta.yml @@ -0,0 +1,205 @@ +fullname: Hierarchy Builder +shortname: hierarchy-builder +organization: math-comp +opam_name: coq-hierarchy-builder +nix_name: hiearchy-builder +community: false +action: true +coqdoc: false +nix: true + +synopsis: >- + High level commands to declare and evolve + a hierarchy based on packed classes. +description: |- + Hierarchy Builder is a high level language to build hierarchies of + algebraic structures and make these hierarchies evolve without breaking + user code. The key concepts are the ones of factory, builder and + abbreviation that let the hierarchy developer describe an actual + interface for their library. Behind that interface the developer can + provide appropriate code to ensure retro compatibility. + +chat: +- url: https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder + shield: zulip + +authors: +- name: Cyril Cohen + initial: true +- name: Kazuhiko Sakaguchi + initial: true +- name: Enrico Tassi + initial: true + +keywords: +- name: algebraic hierarchy + +publications: +- pub_url: https://hal.inria.fr/hal-02478907 + pub_title: "Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi" + pub_doi: 10.4230/LIPIcs.FSCD.2020.34 +- pub_url: https://www.youtube.com/watch?v=F6iRaTlQrlo) + pub_title: "Hierarchy Builder: FSCD Talk" + +license: + fullname: MIT + identifier: MIT + file: LICENSE + +namespace: HB + +opam-file-maintainer: Enrico Tassi + +opam-file-version: dev + +supported_coq_versions: + text: Coq 8.11 to 8.13 (or dev) + opam: '{ (>= "8.11" & < "8.14~") | (= "dev") }' + +tested_coq_opam_versions: +- version: '8.11' +- version: '8.12' +- version: '8.13' + +dependencies: +- opam: + name: coq-elpi + version: '{>= "1.6" & < "1.9~"}' + description: |- + [Coq elpi](https://github.com/LPCIC/coq-elpi) + +cachix: + name: math-comp + extraPullNames: coq + token: CACHIX_AUTH_TOKEN + +make_install_flags: "VFILES=structures.v" + +documentation: |- + ## Example + + ```coq + From HB Require Import structures. + From Coq Require Import ssreflect ZArith. + + HB.mixin Record AddComoid_of_Type A := { + zero : A; + add : A -> A -> A; + addrA : forall x y z, add x (add y z) = add (add x y) z; + addrC : forall x y, add x y = add y x; + add0r : forall x, add zero x = x; + }. + HB.structure Definition AddComoid := { A of AddComoid_of_Type A }. + + Notation "0" := zero. + Infix "+" := add. + + Check forall (M : AddComoid.type) (x : M), x + x = 0. + ``` + + This is all we need to do in order to declare the `AddComoid` structure + and write statements in its signature. + + We proceed by declaring how to obtain an Abelian group out of the + additive, commutative, monoid. + + ```coq + HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := { + opp : A -> A; + addNr : forall x, opp x + x = 0; + }. + HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }. + + Notation "- x" := (opp x). + ``` + + Abelian groups feature the operations and properties given by the + `AbelianGrp_of_AddComoid` mixin (and its dependency `AddComoid`). + + ```coq + Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0. + Proof. by rewrite addrC addNr -[LHS](addNr zero) addrC add0r. Qed. + ``` + + We proceed by showing that `Z` is an example of both structures, and use + the lemma just proved on a statement about `Z`. + + ```coq + HB.instance Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l. + HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l. + + Lemma example2 (x : Z) : x + (- x) = - 0. + Proof. by rewrite example. Qed. + ``` + + ## Documentation + + #### Status + + The software is beta-quality, it works but error messages should be improved. + + The current version forces the carrier to be a type, ruling hierarchies of morphisms out. + + This [draft paper](https://hal.inria.fr/hal-02478907) describes the language + in full detail. + + #### Alternative Installation instructions + +
(click to expand)

+ + - You can use it in nix with the attribute `coqPackages_8_13.hierarchy-builder` e.g. via `nix-shell -p coq_8_13 -p coqPackages_8_13.hierarchy-builder` + +

+ + #### Key concepts + +
(click to expand)

+ + - a *mixin* is a bare bone building block of the hierarchy, it packs operations + and axioms. + + - a *factory* is a package of operations and properties that is elaborated by + HB to one or more mixin. A mixin is hence a trivial factory. + + - a *structure* is declared by attaching zero or more factories to a type. + + - a *builder* is a user provided piece of code capable of + building one or more mixins from a factory. + + - an *instance* is an example of a structure: it provides all operation and + fulfills all axioms. + +

+ + #### The commands of HB + +
(click to expand)

+ + - `HB.mixin` declares a mixin + - `HB.structure` declares a structure + - `HB.factory` declares a factory + - `HB.builders` and `HB.end` declares a set of builders + - `HB.instance` declares a structure instance + - `HB.status` dumps the contents of the hierarchy (debug purposes) + + Their documentation can be found in the comments of [structures.v](structures.v), + search for `Elpi Command` and you will find them. All commands can be + prefixed with the attribute `#[verbose]` to get an idea of what they are doing. + +

+ + #### Demos + +
(click to expand)

+ + - [demo1](demo1/) and [demo3](demo3/) declare and evolve a hierarchy up to + rings with various clients that are tested not to break when the hierarchy + evolves + - [demo2](demo2/) describes the subtle triangular interaction between groups, + topological space and uniform spaces. Indeed, 1. all uniform spaces induce a + topology, which makes them topological spaces, but 2. all topological groups + (groups that are topological spaces such that the addition and opposite are + continuous) induce a uniformity, which makes them uniform spaces. We solve + this seamingly mutual dependency using HB. + +