Skip to content

Coq proof lib

Coq proof lib #1

name: Hacspec - Coq Lib
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.18'
fail-fast: false
steps:
- uses: actions/checkout@v3
- uses: DeterminateSystems/nix-installer-action@main
- uses: DeterminateSystems/magic-nix-cache-action@main
- name: Build
run: nix build -L
- name: Install the toolchain
run: |
nix profile install nixpkgs#yq
nix profile install .#rustc
nix profile install .
- name: Install tomlq
run: cargo install --git https://github.com/Techcable/tomlq
- name: Set up environment
run: |
echo "::group::Setting up problem matcher"
echo "::add-matcher::./.github/coq-errors.json"
echo "::endgroup::"
- name: Build Coq-Hacspec lib
uses: coq-community/docker-coq-action@v1
with:
opam_file: 'opam/coq-hacspec.opam'
custom_image: ${{ matrix.image }}
- name: Run Coq on Tests
working-directory: tests
run: |
paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml)
for cratePath in $paths; do
crate=$(tomlq -r '.package.name' "$cratePath/Cargo.toml")
for skip in $SKIPLIST; do
if [[ "$skip" == "$crate" || "$skip" == "$crate-$backend" ]]; then
echo "⛔ $crate [$backend] (skipping)"
continue 2
fi
done
for backend in coq; do
echo "::group::$crate [$backend]"
cargo hax -C -p "$crate" \; into "$backend"
coqc $cratePath/proofs/coq/extraction/*.v
echo "::endgroup::"
done
done
env:
SKIPLIST: |
enum-struct-variant
literals
slices
naming
if-let
enum-repr
pattern-or
side-effects
v1-lib
mut_arg
fnmut
mut-ref-functionalization
generics
loops
even
odd
never-type
attributes
attribute-opaque
raw-attributes
traits
reordering
nested-derefs
minimal
basic-structs
ping-pong
noise-kkpsk0
fn-to-letfun
include-flag
recursion
# See also:
# https://github.com/coq-community/docker-coq-action#readme
# https://github.com/erikmd/docker-coq-github-action-demo