Skip to content

Cryptol Projects

Cryptol Projects #2987

Workflow file for this run

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
name: Extract Cryptol executables to dist/bin/
run: .github/ci.sh setup_dist_bins
- shell: bash
name: Extract Cryptol API test suite executable to bin/
run: .github/ci.sh extract_exe "test:cryptol-api-tests" "bin"
- 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: api-tests
target: ''
os: ubuntu-22.04
continue-on-error: false
- 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/cryptol-api-tests
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
- if: matrix.suite == 'api-tests'
shell: bash
continue-on-error: ${{ matrix.continue-on-error }}
run: |
export PATH=$PWD/bin:$PWD/dist/bin:$PATH
./bin/cryptol-api-tests
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