Add a tcSmtFile REPL option
#2956
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
| name: Cryptol | |
| on: | |
| push: | |
| tags: ["[0-9]+.[0-9]+(.[0-9]+)?"] | |
| branches: [master, "release-**"] | |
| pull_request: | |
| schedule: | |
| - cron: "0 10 * * *" # 10am UTC -> 2/3am PST | |
| workflow_dispatch: | |
| env: | |
| # The solver package snapshot date. If you update this, make sure to also | |
| # update it in the following locations: | |
| # | |
| # - Dockerfile | |
| # - cryptol-remote-api/Dockerfile | |
| # - README.md | |
| # - dev/dev_setup.sh | |
| SOLVER_PKG_VERSION: "snapshot-20241119" | |
| # The CACHE_VERSION can be updated to force the use of a new cache if | |
| # the 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). | |
| CACHE_VERSION: 1 | |
| 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 }} | |
| release: ${{ steps.config.outputs.release }} | |
| retention-days: ${{ steps.config.outputs.retention-days }} | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| fetch-depth: 0 | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| - 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' }} | |
| run: | | |
| set -x | |
| .github/ci.sh output name cryptol-$(.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 | |
| RELEASE=$( \ | |
| [[ "refs/heads/release-$(.github/ci.sh ver)" == "${{ github.event.ref }}" ]] && \ | |
| [[ "refs/heads/release-$(git describe --tags --abbrev=0)" == "${{ github.event.ref }}" ]] && \ | |
| echo true || echo false) | |
| .github/ci.sh output release $RELEASE | |
| .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5) | |
| build: | |
| runs-on: ${{ matrix.os }} | |
| needs: [config] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-22.04] | |
| ghc-version: ["9.4.8", "9.6.5", "9.8.2"] | |
| cabal: [ '3.10.3.0' ] | |
| run-tests: [true] | |
| include: | |
| # We include one job from an older Ubuntu LTS release to increase our | |
| # coverage of possible Linux configurations. Since we already run the | |
| # tests with the newest LTS release, we won't bother testing this one. | |
| - os: ubuntu-20.04 | |
| ghc-version: 9.4.8 | |
| run-tests: false | |
| # Windows and macOS CI runners are more expensive than Linux runners, | |
| # so we only build one particular GHC version to test them on. We | |
| # include both an x86-64 macOS runner (macos-13) as well as an AArch64 | |
| # macOS runner (macos-14). | |
| - os: windows-2019 | |
| ghc-version: 9.4.8 | |
| run-tests: true | |
| - os: macos-13 | |
| ghc-version: 9.4.8 | |
| run-tests: true | |
| - os: macos-14 | |
| ghc-version: 9.4.8 | |
| run-tests: true | |
| outputs: | |
| test-lib-json: ${{ steps.test-lib.outputs.targets-json }} | |
| env: | |
| VERSION: ${{ needs.config.outputs.version }} | |
| RELEASE: ${{ needs.config.outputs.release }} | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| submodules: true | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| - uses: actions/setup-python@v2 | |
| with: | |
| # Ensure pyproject.toml and python/mypy.ini are kept in sync with the Python version here. | |
| python-version: '3.12' | |
| - uses: abatilo/[email protected] | |
| with: | |
| poetry-version: 1.4.2 | |
| - uses: haskell-actions/setup@v2 | |
| id: setup-haskell | |
| with: | |
| ghc-version: ${{ matrix.ghc-version }} | |
| 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: \"\"" | |
| - uses: actions/cache/restore@v3 | |
| name: Restore cache store cache | |
| with: | |
| path: | | |
| ${{ steps.setup-haskell.outputs.cabal-store }} | |
| dist-newstyle | |
| key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-${{ github.sha }} | |
| restore-keys: | | |
| ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}- | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| # The full zip file name for a what4-solvers bindist. If you update | |
| # this, make sure to also update it in the following locations: | |
| # | |
| # - The other BIN_ZIP_FILE in the `test` job | |
| # - Dockerfile | |
| # - cryptol-remote-api/Dockerfile | |
| BIN_ZIP_FILE: ${{ matrix.os }}-${{ runner.arch }}-bin.zip | |
| - shell: bash | |
| env: | |
| RELEASE: ${{ needs.config.outputs.release }} | |
| run: .github/ci.sh build | |
| - shell: bash | |
| run: .github/ci.sh setup_dist_bins | |
| - shell: bash | |
| run: .github/ci.sh check_docs | |
| if: runner.os != 'Windows' | |
| - shell: bash | |
| run: .github/ci.sh check_rpc_docs | |
| if: runner.os != 'Windows' | |
| - shell: bash | |
| name: Partition test-lib tests | |
| id: test-lib | |
| run: | | |
| set -x | |
| cabal v2-install --install-method=copy --installdir="./bin" test-lib | |
| cmd="cat \$1.stdout" | |
| if ${{ runner.os == 'Windows' }}; then | |
| cmd="cat \$1.stdout.mingw32 2>/dev/null || $cmd" | |
| elif ${{ runner.os == 'macOS' }}; then | |
| cmd="cat \$1.stdout.darwin 2>/dev/null || $cmd" | |
| fi | |
| ./bin/test-runner --ext=.icry -r ./output --exe=$(which bash) -F -c -F "$cmd" -F -- ./tests | |
| TARGETS_JSON=$(echo -n "$(ls -1 ./output/tests)" | jq -Rsc 'split("\n")') | |
| echo "::set-output name=targets-json::$TARGETS_JSON" | |
| - shell: bash | |
| run: .github/ci.sh bundle_files | |
| - if: runner.os == 'Windows' | |
| run: .github/wix.ps1 | |
| - if: runner.os == 'Windows' && 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 cryptol.msi | |
| - shell: bash | |
| run: | | |
| NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-${{ runner.arch }}" | |
| echo "NAME=$NAME" >> $GITHUB_ENV | |
| .github/ci.sh zip_dist $NAME | |
| env: | |
| OS_TAG: ${{ matrix.os }} | |
| ARCH_TAG: ${{ runner.arch }} | |
| - shell: bash | |
| run: | | |
| NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-${{ runner.arch }}" | |
| echo "NAME=$NAME" >> $GITHUB_ENV | |
| .github/ci.sh zip_dist_with_solvers $NAME | |
| env: | |
| OS_TAG: ${{ matrix.os }} | |
| ARCH_TAG: ${{ runner.arch }} | |
| - if: 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 | |
| .github/ci.sh sign ${NAME}-with-solvers.tar.gz | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ env.NAME }} (GHC ${{ matrix.ghc-version }}) | |
| path: "${{ env.NAME }}.tar.gz*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ env.NAME }}-with-solvers (GHC ${{ matrix.ghc-version }}) | |
| path: "${{ env.NAME }}-with-solvers.tar.gz*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - if: matrix.ghc-version == '9.4.8' && matrix.run-tests | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| path: dist/bin | |
| name: ${{ matrix.os }}-dist-bin | |
| - if: matrix.ghc-version == '9.4.8' && matrix.run-tests | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| path: bin | |
| name: ${{ matrix.os }}-bin | |
| - uses: actions/upload-artifact@v4 | |
| if: runner.os == 'Windows' | |
| with: | |
| name: Windows MSI installer (GHC ${{ matrix.ghc-version }}) | |
| path: "cryptol.msi*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - uses: actions/cache/save@v3 | |
| name: Save cache store cache | |
| if: always() | |
| with: | |
| path: | | |
| ${{ steps.setup-haskell.outputs.cabal-store }} | |
| dist-newstyle | |
| key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-${{ github.sha }} | |
| ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}- | |
| test: | |
| runs-on: ${{ matrix.os }} | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| suite: [test-lib] | |
| target: ${{ fromJson(needs.build.outputs.test-lib-json) }} | |
| os: [ubuntu-22.04, macos-14, windows-2019] | |
| continue-on-error: [false] | |
| include: | |
| - suite: rpc | |
| target: '' | |
| os: ubuntu-22.04 | |
| continue-on-error: false | |
| #- suite: rpc | |
| # target: '' | |
| # os: macos-13 | |
| # continue-on-error: false | |
| #- suite: rpc | |
| # target: '' | |
| # os: windows-2019 | |
| # continue-on-error: true # TODO: get Python client to work on Windows | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| submodules: true | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| # Homebrew installs packages in different directories depending on which | |
| # macOS architecture you are using: | |
| # | |
| # * /usr/local (X64) | |
| # * /opt/homebrew (ARM64) | |
| # | |
| # Clang automatically searches in /usr/local without any additional setup, | |
| # but it doesn't know about /opt/homebrew. As such, we have to teach Clang | |
| # to do so by setting the appropriate environment variables. | |
| # | |
| # This step is important for the FFI unit tests, which rely on a | |
| # Homebrew-provided version of gmp. | |
| - name: Teach Clang about Homebrew paths (macOS ARM64) | |
| run: | | |
| echo "CPATH=/opt/homebrew/include" >> $GITHUB_ENV | |
| echo "LIBRARY_PATH=/opt/homebrew/lib" >> $GITHUB_ENV | |
| if: matrix.suite == 'test-lib' && runner.os == 'macOS' && runner.arch == 'ARM64' | |
| - name: Install dependencies (Windows) | |
| uses: msys2/setup-msys2@v2 | |
| with: | |
| update: true | |
| # NB: Use CLANG64 here, not MINGW64. GHC 9.4 and later bundle a | |
| # Clang-based C toolchain on Windows, and the FFI-related tests work | |
| # best when the DLLs are compiled with Clang as well. | |
| msystem: CLANG64 | |
| # These are needed for the ffi tests on Windows | |
| install: | | |
| diffutils | |
| make | |
| mingw-w64-clang-x86_64-gcc | |
| mingw-w64-clang-x86_64-gmp | |
| if: matrix.suite == 'test-lib' && runner.os == 'Windows' | |
| - if: matrix.suite == 'rpc' | |
| uses: actions/setup-python@v2 | |
| with: | |
| # Ensure cryptol-remote-api/python/{pyproject.toml,mypy.ini} are kept in sync with the Python version here. | |
| python-version: '3.12' | |
| - if: matrix.suite == 'rpc' | |
| uses: abatilo/[email protected] | |
| with: | |
| poetry-version: 1.4.2 | |
| - uses: actions/[email protected] | |
| with: | |
| name: "${{ matrix.os }}-dist-bin" | |
| path: dist/bin | |
| - uses: actions/[email protected] | |
| with: | |
| name: "${{ matrix.os }}-bin" | |
| path: bin | |
| - shell: bash | |
| env: | |
| # The full zip file name for a what4-solvers bindist. If you update | |
| # this, make sure to also update it in the following locations: | |
| # | |
| # - The other BIN_ZIP_FILE in the `build` job | |
| # - Dockerfile | |
| # - cryptol-remote-api/Dockerfile | |
| BIN_ZIP_FILE: ${{ matrix.os }}-${{ runner.arch }}-bin.zip | |
| run: | | |
| set -x | |
| chmod +x dist/bin/cryptol | |
| chmod +x dist/bin/cryptol-remote-api | |
| chmod +x dist/bin/cryptol-eval-server | |
| chmod +x bin/test-runner | |
| .github/ci.sh install_system_deps | |
| .github/ci.sh deps bin/abc* | |
| .github/ci.sh deps bin/cvc4* | |
| .github/ci.sh deps bin/cvc5* | |
| .github/ci.sh deps bin/yices-smt2* | |
| .github/ci.sh deps bin/z3* | |
| - if: matrix.suite == 'test-lib' && runner.os != 'Windows' | |
| shell: bash | |
| continue-on-error: ${{ matrix.continue-on-error }} | |
| name: test-lib ${{ matrix.target }} | |
| run: | | |
| export PATH=$PWD/bin:$PWD/dist/bin:$PATH | |
| if ${{ matrix.target != 'ffi' }} || dist/bin/cryptol -v | grep -q 'FFI enabled'; then | |
| ./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }} | |
| fi | |
| - if: matrix.suite == 'test-lib' && runner.os == 'Windows' | |
| shell: msys2 {0} | |
| continue-on-error: ${{ matrix.continue-on-error }} | |
| name: test-lib ${{ matrix.target }} | |
| run: | | |
| export PATH=$PWD/bin:$PWD/dist/bin:$PATH | |
| if ${{ matrix.target != 'ffi' }} || dist/bin/cryptol -v | grep -q 'FFI enabled'; then | |
| ./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }} | |
| fi | |
| - if: matrix.suite == 'rpc' | |
| shell: bash | |
| continue-on-error: ${{ matrix.continue-on-error }} | |
| run: | | |
| export PATH=$PWD/bin:$PWD/dist/bin:$PATH | |
| cryptol-remote-api/run_rpc_tests.sh | |
| build-push-image: | |
| runs-on: ubuntu-22.04 | |
| needs: [config] | |
| if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true' | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - build-args: '' | |
| file: Dockerfile | |
| image: ghcr.io/galoisinc/cryptol | |
| cache: ghcr.io/galoisinc/cache-cryptol | |
| - build-args: PORTABILITY=true | |
| file: cryptol-remote-api/Dockerfile | |
| image: ghcr.io/galoisinc/cryptol-remote-api | |
| cache: ghcr.io/galoisinc/cache-cryptol-remote-api | |
| - build-args: PORTABILITY=false | |
| file: cryptol-remote-api/Dockerfile | |
| image: ghcr.io/galoisinc/cryptol-remote-api | |
| cache: ghcr.io/galoisinc/cache-cryptol-remote-api | |
| steps: | |
| - if: matrix.build-args == 'PORTABILITY=true' | |
| id: prefix | |
| run: echo "::set-output name=prefix::portable-" | |
| - uses: rlespinasse/[email protected] | |
| - id: common-tag | |
| run: echo "::set-output name=common-tag::${{ steps.prefix.outputs.prefix }}$GITHUB_REF_SLUG" | |
| - uses: docker/setup-buildx-action@v1 | |
| - uses: crazy-max/ghaction-docker-meta@v1 | |
| name: Labels | |
| id: labels | |
| with: | |
| images: ${{ matrix.image }} | |
| - uses: docker/login-action@v1 | |
| with: | |
| registry: ghcr.io | |
| username: ${{ github.actor }} | |
| password: ${{ secrets.CR_PAT }} | |
| - uses: docker/build-push-action@v2 | |
| with: | |
| tags: ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} | |
| labels: ${{ steps.labels.outputs.labels }} | |
| load: true | |
| push: false | |
| file: ${{ matrix.file }} | |
| build-args: ${{ matrix.build-args }} | |
| cache-from: | | |
| type=registry,ref=${{ matrix.cache }}:cache-${{ steps.prefix.outputs.prefix }}master | |
| type=registry,ref=${{ matrix.cache }}:cache-${{ steps.common-tag.outputs.common-tag }} | |
| - name: Cache image build | |
| uses: docker/build-push-action@v2 | |
| continue-on-error: true # Tolerate cache upload failures - this should be handled better | |
| with: | |
| tags: ${{ matrix.cache }}:${{ steps.common-tag.outputs.common-tag }} | |
| labels: ${{ steps.labels.outputs.labels }} | |
| push: true | |
| file: ${{ matrix.file }} | |
| build-args: ${{ matrix.build-args }} | |
| cache-to: type=registry,ref=${{ matrix.cache }}:cache-${{ steps.common-tag.outputs.common-tag }},mode=max | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| uses: actions/checkout@v3 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| uses: actions/setup-python@v2 | |
| with: | |
| # Ensure cryptol-remote-api/python/{pyproject.toml,mypy.ini} are kept in sync with the Python version here. | |
| python-version: '3.12' | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| uses: abatilo/[email protected] | |
| with: | |
| poetry-version: 1.4.2 | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| name: Test cryptol-remote-api | |
| run: ./cryptol-remote-api/test_docker.sh http ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| name: Test cryptol-remote-api (TLS) | |
| run: ./cryptol-remote-api/test_docker.sh https ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| uses: docker/build-push-action@v2 | |
| name: Build test-cryptol-remote-api | |
| with: | |
| tags: test-cryptol-remote-api:latest | |
| load: true | |
| push: false | |
| file: cryptol-remote-api/test.Dockerfile | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| name: Test cryptol-remote-api helm chart | |
| run: | | |
| set -x | |
| kind create cluster --wait 10m | |
| kind load docker-image ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} | |
| kind load docker-image test-cryptol-remote-api:latest | |
| helm install --wait cra-http ./helm/cryptol-remote-api \ | |
| --set image.repository=${{ matrix.image }} \ | |
| --set image.tag=${{ steps.common-tag.outputs.common-tag }} \ | |
| --set image.pullPolicy=Never \ | |
| --set server.connType=http | |
| helm install --wait cra-socket ./helm/cryptol-remote-api \ | |
| --set image.repository=${{ matrix.image }} \ | |
| --set image.tag=${{ steps.common-tag.outputs.common-tag }} \ | |
| --set image.pullPolicy=Never \ | |
| --set server.connType=socket | |
| kubectl run --rm --attach test-http \ | |
| --image=test-cryptol-remote-api:latest \ | |
| --image-pull-policy=Never \ | |
| --restart=Never \ | |
| -- http cra-http-cryptol-remote-api 8080 | |
| kubectl run --rm --attach test-socket \ | |
| --image=test-cryptol-remote-api:latest \ | |
| --image-pull-policy=Never \ | |
| --restart=Never \ | |
| -- socket cra-socket-cryptol-remote-api 8080 | |
| - if: needs.config.outputs.event-schedule == 'true' | |
| name: ${{ matrix.image }}:nightly | |
| run: | | |
| docker tag ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} ${{ matrix.image }}:nightly | |
| docker push ${{ matrix.image }}:nightly | |
| - if: needs.config.outputs.release == 'true' | |
| name: ${{ matrix.image }}:${{ needs.config.outputs.version }} | |
| run: | | |
| docker tag ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} ${{ matrix.image }}:${{ needs.config.outputs.version }} | |
| docker push ${{ matrix.image }}:${{ needs.config.outputs.version }} | |
| docker tag ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} ${{ matrix.image }}:latest | |
| docker push ${{ matrix.image }}:latest |