Trying out meta.yml with nix action

.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

.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/[email protected]
+      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/[email protected]
+      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/[email protected]
+      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

.nix/fallback-config.nix

@@ -0,0 +1,5 @@
+{
+  format = "1.0.0";
+  coq-attribute = "hiearchy-builder";
+
+}

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)
-
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # 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
+
+<details><summary>(click to expand)</summary><p>
+
+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
+```
+
+</p></details>
+
+### Manual installation
+
+<details><summary>(click to expand)</summary><p>
+
+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 <number-of-cores-on-your-machine> 
+make install VFILES=structures.v
+```
+
+</p></details>
 
-[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
 
 <details><summary>(click to expand)</summary><p>
 
-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`
-
 </p></details>
 
 #### Key concepts