Skip to content

Commit

Permalink
Trying out meta.yml with nix action
Browse files Browse the repository at this point in the history
  • Loading branch information
CohenCyril committed Feb 19, 2021
1 parent 5982d90 commit 6ae8bad
Show file tree
Hide file tree
Showing 9 changed files with 474 additions and 142 deletions.
33 changes: 33 additions & 0 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
@@ -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
31 changes: 0 additions & 31 deletions .github/workflows/main.yml

This file was deleted.

125 changes: 125 additions & 0 deletions .github/workflows/nix-action.yml
Original file line number Diff line number Diff line change
@@ -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
80 changes: 0 additions & 80 deletions .github/workflows/nix.yml

This file was deleted.

5 changes: 5 additions & 0 deletions .nix/fallback-config.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
{
format = "1.0.0";
coq-attribute = "hiearchy-builder";

}
89 changes: 73 additions & 16 deletions README.md
Original file line number Diff line number Diff line change
@@ -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

Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 6ae8bad

Please sign in to comment.