This repository has been archived by the owner on Feb 15, 2024. It is now read-only.
Update dependency: deps/pyk_release #794
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: 'Check' | |
| on: | |
| pull_request: | |
| workflow_dispatch: | |
| 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@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 | |
| integration-tests: | |
| needs: code-quality-checks | |
| name: 'Integration Tests' | |
| runs-on: [self-hosted, linux, normal] | |
| steps: | |
| - name: 'Check out code' | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: 'Build Docker image' | |
| run: | | |
| COMMIT=$(git rev-parse --short=7 HEAD) | |
| K_VERSION=$(cat deps/k_release) | |
| docker build . \ | |
| --file .github/workflows/Dockerfile \ | |
| --build-arg K_VERSION=${K_VERSION} \ | |
| --tag runtimeverificationinc/proof-generation-ci:${COMMIT} | |
| docker run \ | |
| --name proof-generation-ci \ | |
| --rm \ | |
| --interactive \ | |
| --tty \ | |
| --detach \ | |
| --workdir /home/user \ | |
| runtimeverificationinc/proof-generation-ci:${COMMIT} | |
| docker cp . proof-generation-ci:/home/user | |
| docker exec proof-generation-ci chown -R user:user /home/user | |
| - name: 'Set Python version' | |
| run: docker exec --user user proof-generation-ci poetry env use 3.10 | |
| - name: 'Run integration tests' | |
| run: docker exec --user user proof-generation-ci make cov-integration COV_ARGS=-n8 | |
| - name: 'Verify Metamath proofs' | |
| run: docker exec --user user proof-generation-ci make test-metamath-prelude | |
| - name: 'Verify IMP definition using Metamath' | |
| run: docker exec --user user proof-generation-ci make test-metamath-imp | |
| - name: 'Tear down Docker container' | |
| if: always() | |
| run: | | |
| docker stop --time=0 proof-generation-ci |