Test: pyk #4280
#3168
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: 'Test PR' | |
| on: | |
| pull_request: | |
| branches: | |
| - 'master' | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| version-bump: | |
| name: 'Version Bump' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| token: ${{ secrets.JENKINS_GITHUB_PAT }} | |
| fetch-depth: 0 | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| - name: 'Configure GitHub user' | |
| run: | | |
| git config user.name devops | |
| git config user.email [email protected] | |
| - name: 'Update version' | |
| run: | | |
| og_version=$(git show origin/${GITHUB_BASE_REF}:package/version) | |
| ./package/version.sh bump ${og_version} | |
| ./package/version.sh sub | |
| new_version=$(cat package/version) | |
| sed --in-place "s/^VERSION: Final = '.*'$/VERSION: Final = '${new_version}'/" src/kontrol/__init__.py | |
| git add --update && git commit --message "Set Version: $(cat package/version)" || true | |
| - name: 'Push updates' | |
| run: git push origin HEAD:${GITHUB_HEAD_REF} | |
| code-quality-checks: | |
| needs: version-bump | |
| name: 'Code Quality Checks' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| - name: 'Install Poetry' | |
| uses: Gr1N/setup-poetry@v8 | |
| - name: 'Run code quality checks' | |
| run: make check | |
| - name: 'Run pyupgrade' | |
| run: make pyupgrade | |
| unit-tests: | |
| needs: code-quality-checks | |
| name: 'Unit Tests' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| - name: 'Install Poetry' | |
| uses: Gr1N/setup-poetry@v8 | |
| - name: 'Run unit tests' | |
| run: make cov-unit | |
| profile: | |
| needs: code-quality-checks | |
| name: 'Profiling' | |
| runs-on: [self-hosted, linux, normal] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: ['legacy', 'booster'] | |
| timeout-minutes: 30 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-profile-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.foundry' | |
| - name: 'Run profiling' | |
| run: | | |
| PROF_ARGS=--numprocesses=8 | |
| [ ${{ matrix.backend }} == 'legacy' ] && PROF_ARGS+=' --no-use-booster' | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS="${PROF_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-profile-${GITHUB_SHA} | |
| integration-tests: | |
| needs: code-quality-checks | |
| name: 'Integration Tests' | |
| runs-on: [self-hosted, linux, normal, fast] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: ['legacy', 'booster'] | |
| timeout-minutes: 120 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-integration-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' | |
| - name: 'Run integration tests' | |
| run: | | |
| TEST_ARGS='--numprocesses=8 -vv -k "not test_kontrol_cse and not test_foundry_minimize_proof"' | |
| [ ${{ matrix.backend }} == 'legacy' ] && TEST_ARGS+=' --no-use-booster' | |
| docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA} | |
| cse-tests: | |
| needs: code-quality-checks | |
| name: 'CSE Tests' | |
| runs-on: [self-hosted, linux, normal, fast] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: ['booster'] | |
| timeout-minutes: 120 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Set up Docker' | |
| uses: ./.github/actions/with-docker | |
| with: | |
| container-name: kontrol-ci-integration-${{ github.sha }} | |
| - name: 'Build KEVM' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' | |
| - name: 'Run CSE and Minimize tests' | |
| run: | | |
| TEST_ARGS='--numprocesses=8 -vv -k "test_kontrol_cse or test_foundry_minimize_proof"' | |
| docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}" | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA} | |
| docker: | |
| needs: code-quality-checks | |
| name: 'Docker Tests' | |
| runs-on: [self-hosted, linux, normal] | |
| timeout-minutes: 30 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Login to Docker Hub | |
| uses: docker/login-action@v3 | |
| with: | |
| username: rvdockerhub | |
| password: ${{ secrets.DOCKERHUB_PASSWORD }} | |
| - name: 'Set environment' | |
| run: | | |
| echo "IMAGE_TAG=runtimeverificationinc/kontrol-${GITHUB_SHA}" >> ${GITHUB_ENV} | |
| echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV} | |
| echo "DOCKER_USER=user" >> ${GITHUB_ENV} | |
| echo "DOCKER_GROUP=user" >> ${GITHUB_ENV} | |
| echo "FOUNDRY_ROOT=/home/user/foundry" >> ${GITHUB_ENV} | |
| - name: 'Build Docker image' | |
| run: | | |
| K_VERSION=$(cat deps/k_release) | |
| Z3_VERSION=$(cat deps/z3) | |
| docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION} | |
| - name: 'Start Docker container' | |
| run: | | |
| docker run \ | |
| --name ${CONTAINER_NAME} \ | |
| --rm \ | |
| --interactive \ | |
| --tty \ | |
| --detach \ | |
| --user root \ | |
| ${IMAGE_TAG} | |
| docker cp src/tests/integration/test-data/foundry ${CONTAINER_NAME}:${FOUNDRY_ROOT} | |
| docker exec ${CONTAINER_NAME} chown -R ${DOCKER_USER}:${DOCKER_GROUP} ${FOUNDRY_ROOT} | |
| - name: 'Run forge build' | |
| run: | | |
| docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git foundry-rs/forge-std@75f1746 | |
| docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git runtimeverification/kontrol-cheatcodes | |
| docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge build | |
| - name: 'Run kontrol build' | |
| run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol build | |
| - name: 'Run kontrol prove' | |
| run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --match-test 'AssertTest.test_assert_true()' | |
| - name: 'Run kontrol show' | |
| run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol show 'AssertTest.test_assert_true()' | |
| - name: 'Tear down Docker' | |
| if: always() | |
| run: | | |
| docker stop --time=0 ${CONTAINER_NAME} | |
| nix: | |
| needs: code-quality-checks | |
| name: 'Nix Tests' | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| runner: [ubuntu-latest, macos-13, MacM1] # MacM1 is self-hosted | |
| runs-on: ${{ matrix.runner }} | |
| timeout-minutes: 60 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: 'Install Nix' | |
| if: ${{ matrix.runner != 'MacM1' }} | |
| uses: cachix/install-nix-action@v22 | |
| with: | |
| install_url: https://releases.nixos.org/nix/nix-2.13.3/install | |
| extra_nix_config: | | |
| access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} | |
| substituters = http://cache.nixos.org https://cache.iog.io | |
| trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= | |
| - name: 'Install Cachix' | |
| if: ${{ matrix.runner != 'MacM1' }} | |
| uses: cachix/cachix-action@v12 | |
| with: | |
| name: k-framework | |
| authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }} | |
| - name: 'Build Kontrol' | |
| env: | |
| NIX_PATH: 'nixpkgs=http://nixos.org/channels/nixos-22.05/nixexprs.tar.xz' | |
| GC_DONT_GC: '1' | |
| run: | | |
| set -euxo pipefail | |
| nix --version | |
| JQ=$(nix-build '<nixpkgs>' -A jq --no-link)/bin/jq | |
| KONTROL_BIN=$(nix build .#kontrol.solc_0_8_13 --print-build-logs --json | $JQ -r '.[].outputs | to_entries[].value')/bin | |
| echo $KONTROL_BIN >> $GITHUB_PATH | |
| - name: 'Run smoke test' | |
| run: cd package && ./test-package.sh |