Build

File-relative error reporting #10613

Workflow file for this run

	name: Build

	on:
	pull_request:
	merge_group:
	push:
	branches: [main]

	env:
	SOLUTION: Tools/BoogieToStrata/BoogieToStrata.sln

	jobs:
	get-branch-name:
	runs-on: ubuntu-latest
	steps:
	- name: Get branch name
	shell: bash
	# The workflow is triggered by pull_request so we use `GITHUB_BASE_REF`
	run: echo "branch_name=${GITHUB_BASE_REF}" >> $GITHUB_OUTPUT
	id: get_branch_name
	outputs:
	branch_name: ${{ steps.get_branch_name.outputs.branch_name }}

	build_and_test_lean:
	name: Build and test Lean
	runs-on: ubuntu-latest
	strategy:
	matrix:
	toolchain:
	- stable
	steps:
	- name: Checkout
	uses: actions/checkout@v6
	- name: Install cvc5
	uses: ./.github/actions/install-cvc5
	- name: Install z3
	uses: ./.github/actions/install-z3
	- name: Install .NET
	uses: actions/setup-dotnet@v5
	with:
	dotnet-version: '8.0.x'
	- name: Restore lake cache
	# Only use the caches on PRs because there is a risk of stale results:
	# https://github.com/strata-org/Strata/issues/952
	if: github.event_name == 'pull_request'
	uses: ./.github/actions/restore-lake-cache
	with:
	path: \|
	.lake
	StrataCLI/.lake
	StrataDDM/.lake
	StrataBoole/.lake
	StrataPython/.lake
	- name: Download ion-java jar for Java codegen test
	run: wget -q -O StrataTestExtra/Languages/Java/testdata/ion-java-1.11.11.jar https://github.com/amazon-ion/ion-java/releases/download/v1.11.11/ion-java-1.11.11.jar
	- name: Build StrataDDM
	uses: leanprover/lean-action@v1
	with:
	lake-package-directory: StrataDDM
	build-args: StrataDDM StrataDDMTest
	use-github-cache: false
	- name: Build and test Strata
	uses: leanprover/lean-action@v1
	with:
	use-github-cache: false
	test: false
	- name: Run tests
	run: lake test
	- name: Verify generated editor syntax files are up to date
	run: \|
	lake env lean --run editors/GenSyntax.lean all
	git diff --exit-code editors/vscode/syntaxes/ editors/emacs/
	- name: Build StrataPython
	uses: leanprover/lean-action@v1
	with:
	lake-package-directory: StrataPython
	build-args: StrataPython StrataPythonTest
	use-github-cache: false
	test: false
	- name: Build StrataCLI
	uses: leanprover/lean-action@v1
	with:
	lake-package-directory: StrataCLI
	use-github-cache: false
	- name: Save lake cache
	uses: ./.github/actions/save-lake-cache
	with:
	path: \|
	.lake
	StrataCLI/.lake
	StrataDDM/.lake
	StrataBoole/.lake
	StrataPython/.lake
	- name: Verify Java testdata is up to date
	run: \|
	StrataTestExtra/Languages/Java/regenerate-testdata.sh
	git diff --exit-code StrataTestExtra/Languages/Java/testdata/
	- name: Build and run strata verify
	run: lake exe strata verify ../Examples/SimpleProc.core.st
	working-directory: StrataCLI
	- name: Build StrataBoole
	run: lake build StrataBoole StrataBooleTest
	working-directory: StrataBoole
	- name: Build BoogieToStrata
	run: dotnet build -warnaserror ${SOLUTION}
	- name: Test BoogieToStrata
	run: dotnet test ${SOLUTION}
	- name: Test Strata Command line
	run: .github/scripts/testStrataCommand.sh
	- name: Validate examples against expected output
	working-directory: Examples
	shell: bash
	run: ./run_examples.sh
	- uses: actions/setup-python@v6
	with:
	python-version: '3.14'
	- name: Build using pip
	run: \|
	pip install ./Tools/Python-base
	pip install ./StrataPython/Tools/strata-python
	- name: Run pyInterpret golden-file tests
	working-directory: StrataPython/StrataPythonTest
	shell: bash
	run: ./run_py_interpret.sh
	- name: Run pyAnalyze SARIF tests
	working-directory: StrataPython/StrataPythonTest
	shell: bash
	run: python run_py_analyze_sarif.py
	- name: Run pyAnalyze golden-file tests
	working-directory: StrataPython/StrataPythonTest
	shell: bash
	run: ./run_py_analyze.sh
	- name: Run regex differential tests
	working-directory: StrataPython/StrataPythonTest/Regex
	run: python diff_test.py

	check_pending_python:
	needs: build_and_test_lean
	name: Check pending Python tests
	runs-on: ubuntu-latest
	permissions:
	contents: read
	steps:
	- uses: actions/checkout@v6
	- uses: actions/setup-python@v6
	with:
	python-version: '3.14'
	- name: Build using pip
	run: \|
	pip install ./Tools/Python-base
	pip install ./StrataPython/Tools/strata-python
	- name: Restore Lean build cache
	# The cache is safe to use here because we just saved it for this exact SHA
	# in the build_and_test_lean job
	# https://github.com/strata-org/Strata/issues/952
	uses: ./.github/actions/restore-lake-cache
	with:
	path: \|
	.lake
	StrataCLI/.lake
	StrataDDM/.lake
	StrataBoole/.lake
	StrataPython/.lake
	fail-on-cache-miss: "true"
	use-restore-keys: "false"
	- name: Install Lean
	uses: leanprover/lean-action@v1
	with:
	auto-config: false
	build: false
	- name: Install cvc5
	uses: ./.github/actions/install-cvc5
	with:
	install-to: system
	- name: Check pending tests for newly passing
	working-directory: StrataPython/StrataPythonTest
	shell: bash
	run: ./run_py_analyze.sh --check-pending

	lint_checks:
	name: Run lint checks
	runs-on: ubuntu-latest
	permissions:
	contents: read
	strategy:
	matrix:
	toolchain:
	- stable
	steps:
	- name: Checkout
	uses: actions/checkout@v6
	with:
	fetch-depth: 0
	- name: Check copyright headers
	run: python3 .github/scripts/check_copyright_headers.py .
	shell: bash
	- name: Check for trailing whitespace
	run: .github/scripts/lintWhitespace.sh
	- name: Check for import Lean
	run: .github/scripts/checkLeanImport.sh
	- name: Check Lean version consistncy
	run: .github/scripts/check_lean_consistency.sh
	- name: Check for new panic! usage
	run: .github/scripts/checkNoPanic.sh "origin/${{ github.base_ref \|\| 'main' }}"
	- name: Check for missing string interpolation prefix
	run: .github/scripts/checkMissingInterpolation.sh

	build_doc:
	name: Build documentation
	runs-on: ubuntu-latest
	permissions:
	contents: read
	actions: write
	steps:
	- uses: actions/checkout@v6
	- name: Build API documentation package
	uses: leanprover/lean-action@v1
	with:
	lake-package-directory: 'docs/api'
	- name: Restore lake cache
	uses: actions/cache/restore@v5
	with:
	path: \|
	.lake
	docs/verso/.lake
	key: docs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docs/verso/lean-toolchain') }}-${{ hashFiles('lake-manifest.json', 'docs/verso/lake-manifest.json') }}-${{ hashFiles('*/.st') }}-${{ github.sha }}
	restore-keys: \|
	docs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docs/verso/lean-toolchain') }}-${{ hashFiles('lake-manifest.json', 'docs/verso/lake-manifest.json') }}-${{ hashFiles('*/.st') }}
	- name: Build documentation package
	uses: leanprover/lean-action@v1
	with:
	build-args: '--wfail'
	lake-package-directory: 'docs/verso'
	use-github-cache: false
	- name: Build documentation
	run: ./generate.sh
	working-directory: docs/verso
	- name: Save lake cache
	uses: actions/cache/save@v5
	with:
	path: \|
	.lake
	docs/verso/.lake
	key: docs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docs/verso/lean-toolchain') }}-${{ hashFiles('lake-manifest.json', 'docs/verso/lake-manifest.json') }}-${{ hashFiles('*/.st') }}-${{ github.sha }}
	- name: Check for broken links
	uses: lycheeverse/lychee-action@v2
	with:
	args: --offline --no-progress --exclude-path './find/.' docs/verso/_out/
	fail: true

	build_python:
	needs: build_and_test_lean
	name: Build and test Python
	runs-on: ubuntu-latest
	permissions:
	contents: read
	strategy:
	matrix:
	python_version: [3.11, 3.12, 3.13, 3.14]
	steps:
	- uses: actions/checkout@v6
	- uses: actions/setup-python@v6
	with:
	python-version: ${{ matrix.python_version }}
	- name: Build using pip
	run: \|
	pip install ./Tools/Python-base
	pip install ./StrataPython/Tools/strata-python
	- name: Restore Lean build cache
	# The cache is safe to use here because we just saved it for this exact SHA
	# in the build_and_test_lean job from ci.yml
	# https://github.com/strata-org/Strata/issues/952
	uses: ./.github/actions/restore-lake-cache
	with:
	path: \|
	.lake
	StrataCLI/.lake
	StrataDDM/.lake
	StrataBoole/.lake
	StrataPython/.lake
	fail-on-cache-miss: "true"
	use-restore-keys: "false"
	- name: Install Lean (for lake env)
	uses: leanprover/lean-action@v1
	with:
	auto-config: false
	build: false
	use-github-cache: false
	- name: Install cvc5
	uses: ./.github/actions/install-cvc5
	with:
	install-to: system
	- name: Install z3
	shell: bash
	run: \|
	pip install z3-solver
	Z3_PATH=$(python -c "import z3; import os; print(os.path.join(os.path.dirname(z3.__file__), 'lib', 'z3'))")
	sudo cp "$Z3_PATH" /usr/local/bin/z3 \|\| true
	# Fallback: install from GitHub release
	if ! command -v z3 &> /dev/null; then
	wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.4/z3-4.13.4-x64-glibc-2.35.zip
	unzip z3-4.13.4-x64-glibc-2.35.zip
	sudo cp z3-4.13.4-x64-glibc-2.35/bin/z3 /usr/local/bin/
	fi
	- name: Run PySpec and dispatch tests
	run: PYTHON=python lake test
	working-directory: StrataPython
	- name: Run test script
	run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }}
	working-directory: StrataPython/Tools/strata-python

	cbmc:
	needs: build_and_test_lean
	permissions:
	contents: read
	uses: ./.github/workflows/cbmc.yml

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

File-relative error reporting #10613

Workflow file

File-relative error reporting #10613

Uh oh!

Workflow file for this run