coq-hacspec-lib.yml

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