Skip to content

Trying out meta.yml with nix action #154

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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