Hide additional cells in TUI #6031
This file contains hidden or 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: | |
| code-quality-checks: | |
| name: 'Code Quality Checks' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v4 | |
| - name: 'Get uv release' | |
| id: uv_release | |
| run: | | |
| echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}" | |
| - name: 'Install uv' | |
| uses: astral-sh/setup-uv@v6 | |
| with: | |
| version: ${{ steps.uv_release.outputs.uv_version }} | |
| - 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: 'Get uv release' | |
| id: uv_release | |
| run: | | |
| echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}" | |
| - name: 'Install uv' | |
| uses: astral-sh/setup-uv@v6 | |
| with: | |
| version: ${{ steps.uv_release.outputs.uv_version }} | |
| - name: 'Run unit tests' | |
| run: make cov-unit | |
| profile: | |
| needs: code-quality-checks | |
| name: 'Profiling' | |
| runs-on: [self-hosted, linux, normal] | |
| 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 Kontrol' | |
| run: | | |
| docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*' | |
| - name: 'Run profiling' | |
| run: | | |
| PROF_ARGS='--numprocesses=8' | |
| 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] | |
| 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 Kontrol' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*' | |
| - name: 'Run integration tests' | |
| run: | | |
| TEST_ARGS='-vv --force-sequential -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation)" --numprocesses=3' | |
| 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] | |
| 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 Kontrol' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*' | |
| - name: 'Run CSE and Minimize tests' | |
| run: | | |
| TEST_ARGS='--numprocesses=5 --force-sequential -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} | |
| end-to-end-tests: | |
| needs: code-quality-checks | |
| name: 'End to End Sanity Tests' | |
| runs-on: [self-hosted, linux, normal, fast] | |
| timeout-minutes: 35 | |
| 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 Kontrol' | |
| run: | | |
| docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*' | |
| - name: 'Run end-to-end tests' | |
| run: | | |
| TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation"' | |
| 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: '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@a5dd4b0 | |
| 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 -O2 | |
| - 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: [normal, MacM1] # MacM1 / normal are 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@v31.2.0 | |
| with: | |
| install_url: https://releases.nixos.org/nix/nix-2.31.0/install | |
| extra_nix_config: | | |
| substituters = http://cache.nixos.org https://cache.iog.io | |
| trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= | |
| - name: 'Install Cachix' | |
| if: ${{ matrix.runner != 'MacM1' }} | |
| uses: cachix/cachix-action@v16 | |
| with: | |
| name: k-framework | |
| - 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 |