Skip to content

Refactor rule parsing #7077

Refactor rule parsing

Refactor rule parsing #7077

Workflow file for this run

name: 'Test PR'
on:
pull_request:
types: [opened, edited, reopened, synchronize]
branches:
- 'develop'
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
format-check:
name: 'Java: Linting'
runs-on: ubuntu-latest
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
submodules: recursive
- name: 'Set up Java 17'
uses: actions/setup-java@v4
with:
distribution: 'zulu'
java-version: 17
- name: 'Install Maven'
run: sudo apt-get update && sudo apt-get install --yes maven
- name: 'Check code is formatted correctly'
run: mvn spotless:check --batch-mode -U
pyk-code-quality-checks:
name: 'Pyk: Code Quality & Unit Tests'
runs-on: ubuntu-latest
timeout-minutes: 5
strategy:
fail-fast: false
matrix:
python-version: ['3.10', '3.11', '3.12', '3.13']
defaults:
run:
working-directory: ./pyk
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Set up environment'
uses: ./.github/actions/setup-pyk-env
with:
python-version: ${{ matrix.python-version }}
- name: 'Run code quality checks'
run: make check
- name: 'Run pyupgrade'
run: make pyupgrade
- name: 'Run unit tests'
run: make cov-unit
code-quality:
name: 'Code Quality Checks'
runs-on: ubuntu-latest
needs:
- format-check
- pyk-code-quality-checks
steps:
- run: true
test-k:
name: 'K: Source Build & Test'
runs-on: [self-hosted, linux, normal]
needs: code-quality
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
submodules: recursive
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
tag: k-ci-${{ github.sha }}
os: ubuntu
distro: jammy
llvm: 15
- name: 'Build and Test K'
run: docker exec -t "k-ci-${GITHUB_SHA}" /bin/bash -c 'mvn verify -Dspotless.check.skip=true --batch-mode -U'
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 "k-ci-${GITHUB_SHA}"
docker container rm --force "k-ci-${GITHUB_SHA}" || true
test-package-ubuntu-jammy:
name: 'K: Ubuntu Jammy Package'
runs-on: [self-hosted, linux, normal]
needs: code-quality
steps:
- uses: actions/checkout@v4
- name: 'Build and Test'
uses: ./.github/actions/test-package
with:
os: ubuntu
distro: jammy
llvm: 15
build-package: package/debian/build-package jammy kframework
test-package: package/debian/test-package
- name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page
if: failure()
uses: actions/upload-artifact@v4
with:
name: kore-exec.tar.gz
path: |
**/kore-exec.tar.gz
- name: 'On Success, Upload the package built to the Summary Page'
if: success()
uses: actions/upload-artifact@v4
with:
name: kframework.deb
path: kframework.deb
if-no-files-found: error
retention-days: 1
test-frontend-package-ubuntu-jammy:
name: 'K: Ubuntu Jammy Frontend Package'
runs-on: [self-hosted, linux, normal]
needs: code-quality
steps:
- uses: actions/checkout@v4
- name: 'Build and Test'
uses: ./.github/actions/test-package
with:
os: ubuntu
distro: jammy
llvm: 15
build-package: package/debian/build-package jammy kframework-frontend
test-package: package/debian/test-frontend-package
- name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page
if: failure()
uses: actions/upload-artifact@v4
with:
name: kore-exec.tar.gz
path: |
**/kore-exec.tar.gz
- name: 'On Success, Upload the package built to the Summary Page'
if: success()
uses: actions/upload-artifact@v4
with:
name: kframework-frontend.deb
path: kframework-frontend.deb
if-no-files-found: error
retention-days: 1
pyk-build-on-nix:
needs: code-quality
name: 'Pyk: Nix Build'
strategy:
matrix:
os: [ubuntu-latest, macos-14]
runs-on: ${{ matrix.os }}
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Install Nix'
uses: cachix/install-nix-action@v22
with:
install_url: https://releases.nixos.org/nix/nix-2.13.3/install
extra_nix_config: |
substituters = http://cache.nixos.org https://hydra.iohk.io
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
- name: 'Install Cachix'
uses: cachix/cachix-action@v14
with:
name: k-framework
skipPush: true
- name: 'Build original pyk flake'
run: GC_DONT_GC=1 nix build --print-build-logs .#pyk-python310
- name: 'Build pyk provided by K'
run: GC_DONT_GC=1 nix build --print-build-logs ./pyk#pyk-python310
compile-nix-flake:
needs: code-quality
name: 'K: Nix Build & Test'
strategy:
fail-fast: false
matrix:
include:
- runner: [self-hosted, linux, normal]
- runner: MacM1
os: self-macos-12
runs-on: ${{ matrix.runner }}
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Upgrade bash'
if: ${{ contains(matrix.os, 'macos') }}
run: brew install bash
- name: 'Install Nix'
if: ${{ !startsWith(matrix.os, 'self') }}
uses: cachix/install-nix-action@v22
with:
install_url: https://releases.nixos.org/nix/nix-2.13.3/install
extra_nix_config: |
substituters = http://cache.nixos.org https://hydra.iohk.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: ${{ !startsWith(matrix.os, 'self') }}
uses: cachix/cachix-action@v14
with:
name: k-framework
skipPush: true
- name: 'Build K Framework and push build time dependencies to cachix'
env:
NIX_PATH: 'nixpkgs=http://nixos.org/channels/nixos-22.05/nixexprs.tar.xz'
GC_DONT_GC: '1'
run: |
nix --version
JQ=$(nix-build '<nixpkgs>' -A jq --no-link)/bin/jq
export JQ
k=$(nix build . --print-build-logs --json | $JQ -r '.[].outputs | to_entries[].value')
drv=$(nix-store --query --deriver "$k")
nix-store --query --requisites "$drv" | cachix push k-framework
- name: 'Smoke test K'
run: GC_DONT_GC=1 nix build --print-build-logs .#smoke-test
# These tests take a really long time to run on other platforms, so we
# skip them unless we're on the M1 runner.
- name: 'Test K'
if: ${{ matrix.os == 'self-macos-12' }}
run: GC_DONT_GC=1 nix build --print-build-logs .#test
pyk-build-docs:
name: 'Pyk: Documentation'
needs: test-frontend-package-ubuntu-jammy
runs-on: [self-hosted, linux, normal]
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Download K package from the Summary Page'
uses: actions/download-artifact@v4
with:
name: kframework-frontend.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-docs-${{ github.sha }}
k-deb-path: kframework-frontend.deb
- name: 'Build documentation'
run: docker exec -u user k-pyk-docs-${{ github.sha }} make docs
- name: 'Tear down Docker'
if: always()
run: docker stop --time=0 k-pyk-docs-${{ github.sha }}
pyk-profile:
needs: test-frontend-package-ubuntu-jammy
name: 'Pyk: Profiling'
runs-on: [self-hosted, linux, normal]
timeout-minutes: 10
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Download K package from the Summary Page'
uses: actions/download-artifact@v4
with:
name: kframework-frontend.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-profile-${{ github.sha }}
k-deb-path: kframework-frontend.deb
distro: jammy
- name: 'Run profiling'
run: |
docker exec -u user k-pyk-profile-${{ github.sha }} make profile PROF_ARGS=-n4
docker exec -u user k-pyk-profile-${{ github.sha }} /bin/bash -c 'find /tmp/pytest-of-user/pytest-current/ -type f -name "*.prof" | sort | xargs tail -n +1'
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 k-pyk-profile-${{ github.sha }}
pyk-integration-tests:
needs: test-frontend-package-ubuntu-jammy
name: 'Pyk: Integration Tests'
runs-on: [self-hosted, linux, normal]
timeout-minutes: 30
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Download K package from the Summary Page'
uses: actions/download-artifact@v4
with:
name: kframework-frontend.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-integration-${{ github.sha }}
k-deb-path: kframework-frontend.deb
distro: jammy
- name: 'Run integration tests'
run: |
docker exec -u user k-pyk-integration-${{ github.sha }} make test-integration TEST_ARGS='-n4 --maxfail=0 --timeout=300'
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 k-pyk-integration-${{ github.sha }}
pyk-regression-tests:
needs: test-frontend-package-ubuntu-jammy
name: 'Pyk: Regression Tests'
runs-on: ubuntu-latest
timeout-minutes: 30
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Download K package from the Summary Page'
uses: actions/download-artifact@v4
with:
name: kframework-frontend.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-regression-${{ github.sha }}
k-deb-path: kframework-frontend.deb
distro: jammy
- name: 'Run K regression tests'
run: |
docker exec -u user k-pyk-regression-${{ github.sha }} make test-regression-new -j4
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 k-pyk-regression-${{ github.sha }}