Skip to content

Add per-backend md_selector parameters to booster_kompile #5629

Add per-backend md_selector parameters to booster_kompile

Add per-backend md_selector parameters to booster_kompile #5629

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']
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
pyk-build-docs:
name: 'Pyk: Documentation'
runs-on: ubuntu-latest
defaults:
run:
working-directory: ./pyk
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Set up environment'
uses: ./.github/actions/setup-pyk-env
- name: 'Build documentation'
run: make docs
code-quality:
name: 'Code Quality Checks'
runs-on: ubuntu-latest
needs:
- format-check
- pyk-code-quality-checks
- pyk-build-docs
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
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
pyk-build-on-nix:
needs: code-quality
name: 'Pyk: Nix Build'
strategy:
matrix:
os: [ubuntu-latest, macos-13]
defaults:
run:
working-directory: ./pyk
runs-on: ${{ matrix.os }}
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- 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: |
access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
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
authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
skipPush: true
- name: 'Build pyk'
run: GC_DONT_GC=1 nix build --print-build-logs .#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: macos-13
os: macos-13
- 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: |
access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
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
authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
skipPush: true
- name: 'Build K Framework and push build time dependencies to cachix'
env:
CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
NIX_PATH: 'nixpkgs=http://nixos.org/channels/nixos-22.05/nixexprs.tar.xz'
GC_DONT_GC: '1'
run: |
nix --version
export JQ=$(nix-build '<nixpkgs>' -A jq --no-link)/bin/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-profile:
needs: test-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.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-profile-${{ github.sha }}
k-deb-path: kframework.deb
- 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-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.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-integration-${{ github.sha }}
k-deb-path: kframework.deb
- 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-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.deb
- name: 'Set up Docker'
uses: ./.github/actions/with-k-docker
with:
container-name: k-pyk-regression-${{ github.sha }}
k-deb-path: kframework.deb
- 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 }}
performance-tests:
name: 'K: Profiling'
runs-on: [self-hosted, linux, performance]
needs: test-package-ubuntu-jammy
steps:
- uses: actions/checkout@v4
- name: 'Download K package from the Summary Page'
uses: actions/download-artifact@v4
with:
name: kframework.deb
- name: 'Set up Docker Test Image'
env:
BASE_OS: ubuntu
BASE_DISTRO: jammy
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
BENCHER_API_TOKEN: ${{ secrets.BENCHER_API_TOKEN }}
BENCHER_PROJECT: k-framework
BENCHER_ADAPTER: json
run: |
set -euxo pipefail
workspace=$(pwd)
docker run --name k-profiling-tests-${GITHUB_SHA} \
--rm -it --detach \
-e BENCHER_API_TOKEN=$BENCHER_API_TOKEN \
-e BENCHER_PROJECT=$BENCHER_PROJECT \
-e BENCHER_ADAPTER=$BENCHER_ADAPTER \
-e GITHUB_HEAD_REF=$GITHUB_HEAD_REF \
-e GITHUB_BASE_REF=$GITHUB_BASE_REF \
-e GITHUB_TOKEN=$GITHUB_TOKEN \
-e GITHUB_ACTIONS=true \
-e GITHUB_EVENT_NAME=$GITHUB_EVENT_NAME \
-e GITHUB_EVENT_PATH=$GITHUB_EVENT_PATH \
-e GITHUB_REPOSITORY=$GITHUB_REPOSITORY \
-e GITHUB_REF=$GITHUB_REF \
--workdir /opt/workspace \
-v "${workspace}:/opt/workspace" \
-v "${GITHUB_EVENT_PATH}:${GITHUB_EVENT_PATH}" \
${BASE_OS}:${BASE_DISTRO}
- name: 'Install K from Package'
run: |
set -euxo pipefail
docker exec -t k-profiling-tests-${GITHUB_SHA} /bin/bash -c './k-distribution/tests/profiling/setup_profiling.sh'
- name: 'Profiling Performance Tests'
run: |
set -euxo pipefail
docker exec -t k-profiling-tests-${GITHUB_SHA} /bin/bash -c 'cd k-distribution/tests/profiling && make'
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 k-profiling-tests-${GITHUB_SHA}
docker container rm --force k-profiling-tests-${GITHUB_SHA} || true