Assume the rule remainder condition when checking ensures #6887

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'

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Assume the rule remainder condition when checking ensures #6887

Workflow file

Assume the rule remainder condition when checking ensures #6887

Jobs

Run details

Workflow file for this run