Skip to content

Commit ca723a7

Browse files
CohenCyrilCohenCyril
committed
Trying out meta.yml with nix action
1 parent d9a6b28 commit ca723a7

File tree

9 files changed

+448
-142
lines changed

9 files changed

+448
-142
lines changed

‎.github/workflows/docker-action.yml

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
# This file was generated from `meta.yml`, please do not edit manually.
2+
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
3+
name: Docker CI
4+
5+
on:
6+
push:
7+
branches:
8+
- master
9+
pull_request:
10+
branches:
11+
- '**'
12+
13+
jobs:
14+
build:
15+
# the OS must be GNU/Linux to be able to use the docker-coq-action
16+
runs-on: ubuntu-latest
17+
strategy:
18+
matrix:
19+
image:
20+
- 'coqorg/coq:8.11'
21+
- 'coqorg/coq:8.12'
22+
- 'coqorg/coq:8.13'
23+
fail-fast: false
24+
steps:
25+
- uses: actions/checkout@v2
26+
- uses: coq-community/docker-coq-action@v1
27+
with:
28+
opam_file: 'coq-hierarchy-builder.opam'
29+
custom_image: ${{ matrix.image }}
30+
31+
# See also:
32+
# https://github.com/coq-community/docker-coq-action#readme
33+
# https://github.com/erikmd/docker-coq-github-action-demo

‎.github/workflows/main.yml

Lines changed: 0 additions & 31 deletions
This file was deleted.

‎.github/workflows/nix-action.yml

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
# This file was generated from `meta.yml`, please do not edit manually.
2+
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
3+
name: Nix CI
4+
5+
on:
6+
push:
7+
branches:
8+
- master
9+
pull_request:
10+
branches:
11+
- '**'
12+
13+
jobs:
14+
prerequisites:
15+
runs-on: ubuntu-latest
16+
17+
steps:
18+
- name: Cachix install
19+
uses: cachix/install-nix-action@v12
20+
with:
21+
nix_path: nixpkgs=channel:nixpkgs-unstable
22+
- name: Cache Nix Store
23+
uses: actions/[email protected]
24+
id: cache-nix
25+
with:
26+
path: nix-store.nar
27+
key: nix-${{ runner.os }}-${{ github.sha }}
28+
restore-keys: |
29+
nix-${{ runner.os }}-
30+
- name: Import Nix Store
31+
if: steps.cache-nix.outputs.cache-hit
32+
run: nix-store --import < nix-store.nar
33+
- name: Git checkout
34+
uses: actions/checkout@v2
35+
with:
36+
fetch-depth: 0
37+
- name: Build
38+
run: nix-build --arg ci true --arg ci-step 0
39+
- name: Compute Closure
40+
run: nix path-info -r | tee closure.txt
41+
- name: Export Nix Store
42+
run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar
43+
44+
main:
45+
runs-on: ubuntu-latest
46+
needs: prerequisites
47+
48+
steps:
49+
- name: Cachix install
50+
uses: cachix/install-nix-action@v12
51+
with:
52+
nix_path: nixpkgs=channel:nixpkgs-unstable
53+
- name: Cache Nix Store
54+
uses: actions/[email protected]
55+
id: cache-nix
56+
with:
57+
path: nix-store.nar
58+
key: nix-${{ runner.os }}-${{ github.sha }}
59+
restore-keys: |
60+
nix-${{ runner.os }}-
61+
- name: Import Nix Store
62+
if: steps.cache-nix.outputs.cache-hit
63+
run: nix-store --import < nix-store.nar
64+
- name: Git checkout
65+
uses: actions/checkout@v2
66+
with:
67+
fetch-depth: 0
68+
- name: Build
69+
run: nix-build --arg ci true --arg ci-step 1
70+
- name: Compute Closure
71+
run: nix path-info -r | tee closure.txt
72+
- name: Export Nix Store
73+
run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar
74+
75+
CI:
76+
runs-on: ubuntu-latest
77+
needs: main
78+
79+
steps:
80+
- name: Cachix install
81+
uses: cachix/install-nix-action@v12
82+
with:
83+
nix_path: nixpkgs=channel:nixpkgs-unstable
84+
- name: Cache Nix Store
85+
uses: actions/[email protected]
86+
id: cache-nix
87+
with:
88+
path: nix-store.nar
89+
key: nix-${{ runner.os }}-${{ github.sha }}
90+
restore-keys: |
91+
nix-${{ runner.os }}-
92+
- name: Import Nix Store
93+
if: steps.cache-nix.outputs.cache-hit
94+
run: nix-store --import < nix-store.nar
95+
- name: Git checkout
96+
uses: actions/checkout@v2
97+
with:
98+
fetch-depth: 0
99+
- name: Build
100+
run: nix-build --arg ci true --arg ci-step 1
101+
- name: Compute Closure
102+
run: nix path-info -r | tee closure.txt
103+
- name: Export Nix Store
104+
run: xargs --arg-file=closure.txt nix-store --export > nix-store.nar

‎.github/workflows/nix.yml

Lines changed: 0 additions & 80 deletions
This file was deleted.

‎.nix/fallback-config.nix

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{
2+
format = "1.0.0";
3+
coq-attribute = "hiearchy-builder";
4+
5+
}

‎README.md

Lines changed: 73 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,77 @@
1-
[![Actions Status](https://github.com/math-comp/hierarchy-builder/workflows/CI/badge.svg)](https://github.com/math-comp/hierarchy-builder/actions)
2-
[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Buidlder)
3-
1+
<!---
2+
This file was generated from `meta.yml`, please do not edit manually.
3+
Follow the instructions on https://github.com/coq-community/templates to regenerate.
4+
--->
45
# Hierarchy Builder
56

6-
High level commands to declare and evolve a hierarchy based on packed classes.
7+
[![Docker CI][docker-action-shield]][docker-action-link]
8+
[![Nix CI][nix-action-shield]][nix-action-link]
9+
[![Chat][chat-shield]][chat-link]
10+
11+
[docker-action-shield]: https://github.com/math-comp/hierarchy-builder/workflows/Docker%20CI/badge.svg?branch=master
12+
[docker-action-link]: https://github.com/math-comp/hierarchy-builder/actions?query=workflow:"Docker%20CI"
13+
14+
[nix-action-shield]: https://github.com/math-comp/hierarchy-builder/workflows/Nix%20CI/badge.svg?branch=master
15+
[nix-action-link]: https://github.com/math-comp/hierarchy-builder/actions?query=workflow:"Nix%20CI"
16+
[chat-shield]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg
17+
[chat-link]: https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder
18+
19+
20+
21+
22+
Hierarchy Builder is a high level language to build hierarchies of
23+
algebraic structures and make these hierarchies evolve without breaking
24+
user code. The key concepts are the ones of factory, builder and
25+
abbreviation that let the hierarchy developer describe an actual
26+
interface for their library. Behind that interface the developer can
27+
provide appropriate code to ensure retro compatibility.
28+
29+
## Meta
30+
31+
- Author(s):
32+
- Cyril Cohen (initial)
33+
- Kazuhiko Sakaguchi (initial)
34+
- Enrico Tassi (initial)
35+
- License: [MIT](LICENSE)
36+
- Compatible Coq versions: Coq 8.11 to 8.13 (or dev)
37+
- Additional dependencies:
38+
- [Coq elpi](https://github.com/LPCIC/coq-elpi)
39+
- Coq namespace: `HB`
40+
- Related publication(s):
41+
- [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)
42+
- [Hierarchy Builder: FSCD Talk](https://www.youtube.com/watch?v=F6iRaTlQrlo))
43+
44+
## Building and installation instructions
45+
46+
### Opam installation
47+
48+
<details><summary>(click to expand)</summary><p>
49+
50+
The easiest way to install the latest released version of Hierarchy Builder
51+
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
52+
53+
```shell
54+
opam repo add coq-released https://coq.inria.fr/opam/released
55+
opam install coq-hierarchy-builder
56+
```
57+
58+
</p></details>
59+
60+
### Manual installation
61+
62+
<details><summary>(click to expand)</summary><p>
63+
64+
To instead build and install manually, do:
65+
66+
``` shell
67+
git clone https://github.com/math-comp/hierarchy-builder.git
68+
cd hierarchy-builder
69+
make # or make -j <number-of-cores-on-your-machine>
70+
make install VFILES=structures.v
71+
```
72+
73+
</p></details>
774

8-
[Presented at FSCD2020, talk available on youtube.](https://www.youtube.com/watch?v=F6iRaTlQrlo)
975

1076
## Example
1177

@@ -74,21 +140,12 @@ The current version forces the carrier to be a type, ruling hierarchies of morph
74140
This [draft paper](https://hal.inria.fr/hal-02478907) describes the language
75141
in full detail.
76142

77-
#### Installation & availability
143+
#### Alternative Installation instructions
78144

79145
<details><summary>(click to expand)</summary><p>
80146

81-
HB works on Coq 8.10 and 8.11.
82-
83-
- You can install it via OPAM
84-
85-
```shell
86-
opam repo add coq-released https://coq.inria.fr/opam/released
87-
opam install coq-hierarchy-builder
88-
```
147+
- 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`
89148

90-
- 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`
91-
92149
</p></details>
93150

94151
#### Key concepts

0 commit comments

Comments
 (0)