Simplify returning of proof results #376
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
| 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@v3 | |
| 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 devops@runtimeverification.com | |
| - 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@v3 | |
| - 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@v3 | |
| - 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@v3 | |
| 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 kevm-dist --verbose build -j`nproc` plugin foundry' | |
| - name: 'Run profiling' | |
| run: | | |
| PROF_ARGS=--numprocesses=8 | |
| [ ${{ matrix.backend }} == 'booster' ] && PROF_ARGS+=' --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: 180 | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v3 | |
| 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 kevm-dist --verbose build -j`nproc` plugin haskell foundry' | |
| - name: 'Run integration tests' | |
| run: | | |
| TEST_ARGS=--numprocesses=8 | |
| [ ${{ matrix.backend }} == 'booster' ] && TEST_ARGS+=' --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} | |
| 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@v3 | |
| 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 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 --use-booster --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} |