Skip to content
This repository has been archived by the owner on Feb 15, 2024. It is now read-only.

Update dependency: deps/pyk_release #807

Update dependency: deps/pyk_release

Update dependency: deps/pyk_release #807

Workflow file for this run

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