SAWScript #3672
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Overall configuration notes: | |
| # - Artifact uploads for binaries are from GHC 9.6.6 | |
| # - Builds for Ubuntu happen on 22.04. We also include a single configuration | |
| # for 20.04 to increase our Linux coverage. | |
| # - Docker builds happen nightly, on manual invocation, and on release branch commits | |
| # Please update this comment as those details change. | |
| name: SAWScript | |
| on: | |
| push: | |
| tags: ["v?[0-9]+.[0-9]+(.[0-9]+)?"] | |
| branches: [master, "release-**"] | |
| pull_request: | |
| schedule: | |
| - cron: "0 10 * * *" # 10am UTC -> 2/3am PST | |
| workflow_dispatch: | |
| env: | |
| # The CABAL_CACHE_VERSION and SOLVER_CACHE_VERSION environment variables | |
| # can be updated to force the use of a new cabal or solver cache if the | |
| # respective current cache contents become corrupted/invalid. This can | |
| # sometimes happen when (for example) the OS version is changed but | |
| # older .so files are cached, which can have various effects | |
| # (e.g. cabal complains it can't find a valid version of the "happy" | |
| # tool). | |
| CABAL_CACHE_VERSION: 1 | |
| SOLVER_CACHE_VERSION: 1 | |
| DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc" | |
| # Solver package snapshot date - also update in the following locations: | |
| # ./saw/Dockerfile | |
| # ./saw-remote-api/Dockerfile | |
| # ./s2nTests/scripts/blst-entrypoint.sh | |
| # ./s2nTests/docker/saw.dockerfile | |
| SOLVER_PKG_VERSION: "snapshot-20240212" | |
| OCAML_VERSION: 4.09.x | |
| jobs: | |
| config: | |
| runs-on: ubuntu-22.04 | |
| outputs: | |
| name: ${{ steps.config.outputs.name }} | |
| version: ${{ steps.config.outputs.version }} | |
| event-tag: ${{ steps.config.outputs.tag }} | |
| event-schedule: ${{ steps.config.outputs.schedule }} | |
| publish: ${{ steps.config.outputs.publish }} | |
| release: ${{ steps.config.outputs.release }} | |
| retention-days: ${{ steps.config.outputs.retention-days }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: config | |
| id: config | |
| env: | |
| EVENT_TAG: ${{ startsWith(github.event.ref, 'refs/tags/') }} | |
| EVENT_SCHEDULE: ${{ github.event_name == 'schedule' }} | |
| EVENT_DISPATCH: ${{ github.event_name == 'workflow_dispatch' }} | |
| RELEASE: ${{ startsWith(github.event.ref, 'refs/heads/release-') }} | |
| run: | | |
| set -x | |
| .github/ci.sh output name saw-$(.github/ci.sh ver) | |
| .github/ci.sh output version $(.github/ci.sh ver) | |
| .github/ci.sh output tag $EVENT_TAG | |
| .github/ci.sh output schedule $EVENT_SCHEDULE | |
| .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false) | |
| .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh ver)" == "${{ github.event.ref }}" ]] && echo true || echo false) | |
| .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5) | |
| build: | |
| runs-on: ${{ matrix.os }} | |
| needs: [config] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [macos-14] | |
| cabal: ["3.10.3.0"] | |
| ghc: ["9.6.6"] | |
| run-tests: [true] | |
| hpc: [false] | |
| outputs: | |
| cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: | | |
| git submodule update --init | |
| - id: config | |
| shell: bash | |
| run: | | |
| NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-${{ runner.arch }}" | |
| .github/ci.sh output name $NAME | |
| echo "NAME=${{ needs.config.outputs.name }}-${{ matrix.os }}-${{ runner.arch }}" >> $GITHUB_ENV | |
| - uses: haskell-actions/setup@v2 | |
| id: setup-haskell | |
| with: | |
| ghc-version: ${{ matrix.ghc }} | |
| cabal-version: ${{ matrix.cabal }} | |
| - name: Post-GHC installation fixups on Windows | |
| shell: bash | |
| if: runner.os == 'Windows' | |
| run: | | |
| # A workaround for https://github.com/Mistuke/CabalChoco/issues/5 | |
| cabal user-config update -a "extra-include-dirs: \"\"" | |
| cabal user-config update -a "extra-lib-dirs: \"\"" | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| BUILD_TARGET_ARCH: ${{ runner.arch }} | |
| - uses: actions/cache/restore@v4 | |
| name: Restore cabal store cache | |
| with: | |
| path: | | |
| ${{ steps.setup-haskell.outputs.cabal-store }} | |
| dist-newstyle | |
| key: ${{ env.CABAL_CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} | |
| restore-keys: | | |
| ${{ env.CABAL_CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- | |
| - if: needs.config.outputs.release == 'true' | |
| shell: bash | |
| run: | | |
| sed -i.bak \ | |
| -e 's/^hashText = .*$/hashText = ""/' \ | |
| -e '/import GitRev.*$/d' \ | |
| saw/SAWScript/Version.hs | |
| rm -f saw/SAWScript/Version.hs.bak | |
| - shell: bash | |
| run: .github/ci.sh build | |
| env: | |
| ENABLE_HPC: ${{ matrix.hpc }} | |
| - shell: bash | |
| env: | |
| RELEASE: ${{ needs.config.outputs.release }} | |
| run: .github/ci.sh build_cryptol | |
| - uses: GaloisInc/.github/actions/cabal-collect-bins@v1.1.1 | |
| id: cabal-test-suites | |
| with: | |
| targets: | | |
| integration_tests | |
| test-sawcore | |
| cryptol-saw-core-tc-test | |
| prover_tests | |
| dest: dist-tests | |
| - uses: actions/upload-artifact@v2 | |
| if: "matrix.ghc == '9.6.6'" | |
| with: | |
| path: dist-tests | |
| name: dist-tests-${{ matrix.os }} | |
| - shell: bash | |
| run: .github/ci.sh setup_dist_bins | |
| - shell: bash | |
| run: .github/ci.sh bundle_files | |
| - shell: bash | |
| run: .github/ci.sh zip_dist $NAME | |
| - shell: bash | |
| run: .github/ci.sh zip_dist_with_solvers $NAME-with-solvers | |
| - if: matrix.ghc == '9.6.6' && github.event.pull_request.head.repo.fork == false | |
| shell: bash | |
| env: | |
| SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} | |
| SIGNING_KEY: ${{ secrets.SIGNING_KEY }} | |
| run: .github/ci.sh sign $NAME.tar.gz | |
| - if: matrix.ghc == '9.6.6' && github.event.pull_request.head.repo.fork == false | |
| shell: bash | |
| env: | |
| SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} | |
| SIGNING_KEY: ${{ secrets.SIGNING_KEY }} | |
| run: .github/ci.sh sign $NAME-with-solvers.tar.gz | |
| ########################################################################## | |
| # We upload an archive containing SAW, and also and archive containing SAW | |
| # and the set of possible SMT solvers, but only for our "primary" | |
| # distribution (currently: GHC 9.6.6). These archives are utilized in | |
| # subsequent CI jobs, but are also published for external users, and are | |
| # therefore signed. | |
| # | |
| # In addition, if we built with HPC, we upload a tarball containing the | |
| # HPC-enabled binaries and HPC-specific files generated during the build | |
| # process. These are mostly used for subsequent CI jobs that will | |
| # generate a coverage report, and the binaries are essentially the same as | |
| # those collected for the previous operation, but they are captured in | |
| # their original cabal-generated locations where they are expected to live | |
| # for subsequent coverage collection. | |
| # In the next 3 steps we check that `matrix.hpc == false` so that if the | |
| # distribution version matches the HPC version, the HPC build artifacts do | |
| # not clobber the non-HPC distribution artifacts. | |
| - if: matrix.ghc == '9.6.6' && matrix.hpc == false | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }}) | |
| path: "${{ steps.config.outputs.name }}.tar.gz*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - if: matrix.ghc == '9.6.6' && matrix.hpc == false | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: ${{ steps.config.outputs.name }}-with-solvers (GHC ${{ matrix.ghc }}) | |
| path: "${{ steps.config.outputs.name }}-with-solvers.tar.gz*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - if: matrix.ghc == '9.6.6' && matrix.run-tests && matrix.hpc == false | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| path: dist/bin | |
| name: ${{ matrix.os }}-bins | |
| - if: matrix.hpc == true | |
| shell: bash | |
| run: .github/ci.sh collect_hpc_files | |
| - if: matrix.hpc == true | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| path: hpc.tar.gz | |
| name: ${{ matrix.os }}-hpc.tar.gz | |
| - uses: actions/cache/save@v4 | |
| name: Save cabal store cache | |
| if: always() | |
| with: | |
| path: | | |
| ${{ steps.setup-haskell.outputs.cabal-store }} | |
| dist-newstyle | |
| key: ${{ env.CABAL_CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} | |
| mr-solver-tests: | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [macos-14] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| BUILD_TARGET_ARCH: ${{ runner.arch }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ matrix.os }}-bins" | |
| path: dist/bin | |
| - name: Update PATH to include SAW | |
| shell: bash | |
| run: | | |
| chmod +x dist/bin/* | |
| echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH | |
| - working-directory: examples/mr_solver | |
| shell: bash | |
| run: | | |
| saw monadify.saw | |
| saw mr_solver_unit_tests.saw | |
| heapster-tests: | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [macos-14] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| BUILD_TARGET_ARCH: ${{ runner.arch }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ matrix.os }}-bins" | |
| path: dist/bin | |
| - name: Update PATH to include SAW | |
| shell: bash | |
| run: | | |
| chmod +x dist/bin/* | |
| echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: 4.14.x | |
| - run: opam repo add coq-released https://coq.inria.fr/opam/released | |
| - run: opam install -y coq=8.15.2 coq-bits=1.1.0 | |
| # If you change the entree-specs commit below, make sure you update the | |
| # documentation in saw-core-coq/README.md accordingly. | |
| - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#62e916fe308d7b215363b80edf9e6d6d1602c737 | |
| # FIXME: the following steps generate Coq libraries for the SAW core to | |
| # Coq translator and builds them; if we do other Coq tests, these steps | |
| # should become their own build artifact, to avoid re-compiling the Coq | |
| # libraries | |
| - working-directory: saw-core-coq/coq | |
| shell: bash | |
| run: opam exec -- make -j | |
| - working-directory: heapster-saw/examples | |
| shell: bash | |
| run: opam exec -- make -j | |
| saw-remote-api-tests: | |
| runs-on: ${{ matrix.os }} | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| # TODO: saw-remote-api unit tests are disabled pending a fix for #1699 | |
| - name: Install on MacOS | |
| test: | | |
| cd saw-remote-api/python/ | |
| poetry install | |
| poetry run mypy --install-types --non-interactive saw_client/ || true | |
| poetry run mypy --install-types --non-interactive saw_client/ | |
| os: macos-14 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| BUILD_TARGET_ARCH: ${{ runner.arch }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ matrix.os }}-bins" | |
| path: dist/bin | |
| - uses: actions/setup-python@v2 | |
| with: | |
| # Ensure that this matches saw-remote-api/python/mypy.ini file | |
| # and that saw-remote-api/python/pyproject.toml file is compatible with this version | |
| python-version: '3.12' | |
| - uses: abatilo/actions-poetry@v2.0.0 | |
| with: | |
| poetry-version: 1.4.2 | |
| - name: ${{ matrix.name }} | |
| shell: bash | |
| run: | | |
| chmod +x dist/bin/* | |
| export PATH="$PWD/dist/bin:$PATH" | |
| echo "$PWD/dist/bin" >> "$GITHUB_PATH" | |
| abc -h || true | |
| yices --version | |
| yices-smt2 --version | |
| saw --version | |
| saw-remote-api --help | |
| ${{ matrix.test }} |