Build

Port main2 Python fixes to Strata-Python #7

Workflow file for this run

	name: Build

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

	jobs:
	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: strata-org/Strata/.github/actions/install-cvc5@main
	- name: Install z3
	uses: strata-org/Strata/.github/actions/install-z3@main
	- 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
	- name: Build StrataPython and compile-time tests
	# Building StrataPythonTest runs the compile-time test suite: the tests
	# are `#guard_msgs` / `#eval` checks that execute during elaboration.
	# This also resolves the `Strata` git dependency, cloning it into
	# `.lake/packages/Strata`.
	uses: leanprover/lean-action@v1
	with:
	build-args: StrataPython StrataPythonTest
	use-github-cache: false
	test: false
	- uses: actions/setup-python@v6
	with:
	python-version: '3.14'
	- name: Build using pip
	# `strata-base` (Tools/Python-base) and `strata-python` (Tools/strata-python)
	# both live in this repo.
	run: \|
	pip install ./Tools/Python-base
	pip install ./Tools/strata-python
	- name: Run pyInterpret golden-file tests
	working-directory: StrataPythonTest
	shell: bash
	run: ./run_py_interpret.sh
	- name: Run pyAnalyze SARIF tests
	working-directory: StrataPythonTest
	shell: bash
	run: python run_py_analyze_sarif.py
	- name: Run pyAnalyze golden-file tests
	working-directory: StrataPythonTest
	shell: bash
	run: ./run_py_analyze.sh
	- name: Run regex differential tests
	working-directory: StrataPythonTest/Regex
	run: python diff_test.py
	- name: Save lake cache
	uses: ./.github/actions/save-lake-cache
	with:
	path: .lake

	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: 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
	fail-on-cache-miss: "true"
	use-restore-keys: "false"
	- name: Build using pip
	run: \|
	pip install ./Tools/Python-base
	pip install ./Tools/strata-python
	- name: Install Lean
	uses: leanprover/lean-action@v1
	with:
	auto-config: false
	build: false
	- name: Install cvc5
	uses: strata-org/Strata/.github/actions/install-cvc5@main
	with:
	install-to: system
	- name: Check pending tests for newly passing
	working-directory: 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
	uses: strata-org/Strata/.github/actions/check-copyright-headers@main
	- name: Check for trailing whitespace
	uses: strata-org/Strata/.github/actions/lint-whitespace@main
	with:
	directory: .
	- name: Check for import Lean
	uses: strata-org/Strata/.github/actions/check-lean-import@main
	- name: Check for new panic! usage
	uses: strata-org/Strata/.github/actions/check-no-panic@main
	with:
	base-ref: "origin/${{ github.base_ref \|\| 'main' }}"

	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: 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
	fail-on-cache-miss: "true"
	use-restore-keys: "false"
	- name: Build using pip
	run: \|
	pip install ./Tools/Python-base
	pip install ./Tools/strata-python
	- 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: strata-org/Strata/.github/actions/install-cvc5@main
	with:
	install-to: system
	- name: Install z3
	uses: strata-org/Strata/.github/actions/install-z3@main
	with:
	install-to: system
	- name: Run PySpec and dispatch tests
	# Excludes the CPython differential test, which is run separately below
	# against a full CPython checkout; here it would be a no-op anyway since
	# CPYTHON_DIR is unset.
	run: PYTHON=python lake test -- --exclude CpythonDiffTest
	- name: Run CPython differential tests
	# Clones CPython at the matrix version and round-trips its whole test
	# suite through the Strata generator + Ion (de)serializer. The round-trip
	# check runs in-process inside the StrataPythonTestExtra/CpythonDiffTest
	# Lean test (driven by this script), so no separate `strata` CLI is built.
	run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }}
	working-directory: 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

Port main2 Python fixes to Strata-Python #7

Workflow file

Port main2 Python fixes to Strata-Python #7

Uh oh!

Workflow file for this run