Skip to content

HOTFIX abort rewrite when SMT solver times out #6907

HOTFIX abort rewrite when SMT solver times out

HOTFIX abort rewrite when SMT solver times out #6907

Workflow file for this run

name: "Test"
on:
workflow_dispatch:
pull_request:
concurrency:
# head_ref is defined for PRs only, so we use run_id (unique) in case
# we want to run on the main branch, to ensure all commits are built
group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
cancel-in-progress: true
env:
ghc_version: "9.6.5"
stack_version: "2.15.1"
hpack_version: '0.36'
jobs:
formatting:
name: 'Formatting and Style'
runs-on: ubuntu-22.04
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
ref: ${{ github.event.pull_request.head.ref }}
fetch-depth: 0
submodules: recursive
token: ${{ secrets.JENKINS_GITHUB_PAT }}
- name: 'Install Nix'
uses: cachix/install-nix-action@v25
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://cache.iog.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
authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
- name: Format
run: nix develop .#style --command bash -c './scripts/fourmolu.sh'
- name: Update branch
env:
GITHUB_EVENT_NAME: ${{ github.event_name }}
run: |
if git status -s -b | grep -q '^##.*(no branch)$'; then
echo 2>&1 "Error: Git is in detached HEAD state"
exit 1
fi
if [ -n "$(git status --porcelain '*.hs')" ]; then
git config --global user.name github-actions
git config --global user.email [email protected]
git add '*.hs'
git commit -m "Format with fourmolu"
git show --stat
git push
echo "Reformatted code pushed, aborting this workflow" | tee -a $GITHUB_STEP_SUMMARY
exit 1
fi
# could run hlint here, but then no more jobs would run if the code is not accepted
# - name: 'Check style with hlint'
# run: nix develop .#style --command bash -c './scripts/hlint.sh'
nix-build:
name: 'Nix / Unit Tests'
needs: formatting
strategy:
fail-fast: false
matrix:
include:
- runner: ubuntu-22.04
os: ubuntu-22.04
nix: x86_64-linux
- runner: MacM1
os: self-macos-12
nix: aarch64-darwin
runs-on: ${{ matrix.runner }}
steps:
- name: Check out code
uses: actions/checkout@v4
with:
# Check out pull request HEAD instead of merge commit.
ref: ${{ github.event.pull_request.head.sha }}
submodules: recursive
- name: 'Upgrade bash'
if: ${{ contains(matrix.os, 'macos') }}
run: brew install bash
# Do the Following only on Public Runners; Mac Runner is pre-installed with build tools
- name: 'Install Nix'
if: ${{ !startsWith(matrix.os, 'self') }}
uses: cachix/install-nix-action@v25
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://cache.iog.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 }}'
- name: Build
run: GC_DONT_GC=1 nix build .#kore-exec .#kore-rpc-booster
- name: Test
run: GC_DONT_GC=1 nix develop .#cabal --command bash -c "hpack ./booster && hpack dev-tools && cabal update && cabal build all && cabal test --enable-tests --test-show-details=direct kore-test unit-tests"
nix-integration:
name: 'Nix / Integration'
needs: formatting
runs-on: [self-hosted, linux, normal]
steps:
- name: Check out code
uses: actions/checkout@v4
with:
# Check out pull request HEAD instead of merge commit.
ref: ${{ github.event.pull_request.head.sha }}
submodules: recursive
- name: Install Nix
uses: cachix/install-nix-action@v26
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://cache.iog.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
- uses: dorny/paths-filter@v3
id: changes
with:
filters: |
kore:
- 'kore/**'
kore_rpc_types:
- 'kore-rpc-types/**'
booster:
- 'booster/**'
dev_tools:
- 'dev-tools/**'
project:
- 'stack.yaml*'
- 'cabal.project*'
- 'Makefile'
- '*.mk'
- 'flake.nix'
- 'deps/*'
- scripts/booster-integration-tests.sh
kore_tests:
- 'test/**'
- name: Build
run: GC_DONT_GC=1 nix build .#kore-exec .#kore-rpc-booster
- name: Run booster integration tests
if: ${{ (steps.changes.outputs.booster == 'true' || steps.changes.outputs.kore == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.project == 'true') }}
run: |
GC_DONT_GC=1 nix develop .#cabal --command bash -c "scripts/booster-integration-tests.sh"
- name: Run kore integration tests
# do not run this unless anything has changed in a relevant directory
if: ${{ (steps.changes.outputs.kore == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.kore_tests == 'true' || steps.changes.outputs.project == 'true') }}
run: |
GC_DONT_GC=1 nix develop github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
--override-input haskell-backend . --update-input haskell-backend \
--command bash -c "cd test && make -j2 --output-sync test"
stack:
name: 'Stack / Unit Tests'
needs: formatting
runs-on: ubuntu-22.04
steps:
- name: Install prerequisites
run: |
sudo apt install --yes debhelper z3 libsecp256k1-dev
- uses: actions/checkout@v4
with:
# Check out pull request HEAD instead of merge commit.
ref: ${{ github.event.pull_request.head.sha }}
submodules: recursive
- name: Cache Stack root
uses: actions/cache@v4
with:
path: ~/.stack
key: stack-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }}-${{ hashFiles('stack.yaml.lock') }}
restore-keys: |
stack-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }}
stack-${{ runner.os }}-ghc-${{ env.ghc_version }}
- uses: haskell-actions/[email protected]
id: setup-haskell-stack
with:
ghc-version: ${{ env.ghc_version }}
stack-version: ${{ env.stack_version }}
enable-stack: true
stack-setup-ghc: true
- name: Build dependencies
run: |
stack build --test --only-dependencies
if [ -n "$(git status --porcelain)" ]; then
git diff
exit 1
fi
- name: Build all packages (preparing for test)
run: stack build --test --no-run-tests --pedantic
- name: Run unit tests
run: stack test kore:kore-test hs-backend-booster:unit-tests
- name: Build Ubuntu package
run: ./package/debian/build-package jammy k-haskell-backend.deb
hlint:
name: 'HLint'
needs: formatting
runs-on: ubuntu-22.04
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
ref: ${{ github.event.pull_request.head.ref }}
fetch-depth: 0
submodules: recursive
- name: 'Install Nix'
uses: cachix/install-nix-action@v25
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://cache.iog.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
authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
- name: Format
run: nix develop .#style --command bash -c './scripts/hlint.sh'