RefMan: document that the FFI expects pure functions (#1558) #2051
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 | |
| SOLVER_PKG_VERSION: "snapshot-20230711" | |
| # 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@v2 | |
| 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' }} | |
| 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, macos-12, windows-2019] | |
| ghc-version: ["8.10.7", "9.2.8", "9.4.5"] | |
| cabal: [ '3.8.1.0' ] | |
| run-tests: [true] | |
| exclude: | |
| - os: windows-2019 | |
| ghc-version: 8.10.7 | |
| run-tests: true | |
| - os: windows-2019 | |
| ghc-version: 9.4.5 | |
| 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.2.8 | |
| run-tests: false | |
| 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@v2 | |
| with: | |
| submodules: true | |
| - uses: actions/setup-python@v2 | |
| with: | |
| python-version: '3.11' | |
| - 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@v2 | |
| name: Cache cabal store | |
| 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 }}-x86_64" | |
| echo "NAME=$NAME" >> $GITHUB_ENV | |
| .github/ci.sh zip_dist $NAME | |
| env: | |
| OS_TAG: ${{ matrix.os }} | |
| - shell: bash | |
| run: | | |
| NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64" | |
| echo "NAME=$NAME" >> $GITHUB_ENV | |
| .github/ci.sh zip_dist_with_solvers $NAME | |
| env: | |
| OS_TAG: ${{ matrix.os }} | |
| - 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@v2 | |
| 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@v2 | |
| 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.2.8' && matrix.run-tests | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| path: dist/bin | |
| name: ${{ runner.os }}-dist-bin | |
| - if: matrix.ghc-version == '9.2.8' && matrix.run-tests | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| path: bin | |
| name: ${{ runner.os }}-bin | |
| - uses: actions/upload-artifact@v2 | |
| if: runner.os == 'Windows' | |
| with: | |
| name: ${{ env.NAME }} (GHC ${{ matrix.ghc-version }}) | |
| path: "cryptol.msi*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| 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-12, windows-2019] | |
| continue-on-error: [false] | |
| include: | |
| - suite: rpc | |
| target: '' | |
| os: ubuntu-22.04 | |
| continue-on-error: false | |
| #- suite: rpc | |
| # target: '' | |
| # os: macos-12 | |
| # 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@v2 | |
| with: | |
| submodules: true | |
| - uses: haskell/actions/setup@v2 | |
| with: | |
| ghc-version: '9.2.8' | |
| - name: Install dependencies (Windows) | |
| uses: msys2/setup-msys2@v2 | |
| with: | |
| update: true | |
| msystem: MINGW64 | |
| # These are needed for the ffi tests on Windows | |
| install: | | |
| diffutils | |
| make | |
| mingw-w64-x86_64-gcc | |
| mingw-w64-x86_64-gmp | |
| if: matrix.suite == 'test-lib' && runner.os == 'Windows' | |
| - if: matrix.suite == 'rpc' | |
| uses: actions/setup-python@v2 | |
| with: | |
| python-version: '3.11' | |
| - if: matrix.suite == 'rpc' | |
| uses: abatilo/[email protected] | |
| with: | |
| poetry-version: 1.4.2 | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-dist-bin" | |
| path: dist/bin | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.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* | |
| ghc_ver="$(ghc --numeric-version)" | |
| cp cabal.GHC-"$ghc_ver".config cabal.project.freeze | |
| cabal v2-update | |
| - 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@v2 | |
| - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api' | |
| uses: actions/setup-python@v2 | |
| with: | |
| python-version: '3.11' | |
| - 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 |