extract_and_run_coq.yml

name: Extract and Run - Coq

on: [pull_request]
jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        with:
          path: hax

      - uses: DeterminateSystems/nix-installer-action@main
      - uses: DeterminateSystems/magic-nix-cache-action@main

      - name: ⤵ Install hax
        run: |
          nix profile install --verbose ./hax

      - name: build coverage example
        working-directory: hax/examples/coverage
        run: |
          nix run . into coq

      - name: run coq - coverage
        working-directory: hax/examples/coverage/proofs/coq/extraction
        run: |
          sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here.
          nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
          nix-shell --packages coq coqPackages.coq-record-update --run "make"

      - name: build and run coq on tests
        env:
          FILES: assert attribute-opaque constructor-as-closure enum-repr enum-struct-variant even
          NOT_SUPPORTED_FILES: attributes cli conditional-match cyclic-modules dyn functions
        run: |
          for f in $FILES; do \
            cd hax/tests/$f && \
            nix run . into coq && \
            cd ../../..
          done
          for f in $FILES; do \
            cd hax/tests/$f/proofs/coq/extraction && \
            nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
            nix-shell --packages coq coqPackages.coq-record-update --run "make" && \
            cd ../../../../../../
          done