Record the current f03 staging gate #1425

Workflow file for this run

	name: CI

	on:
	push:
	branches: [main]
	pull_request:

	# A superseded five-hour run has no value. This also prevents a burst of PR
	# updates from consuming the entire hosted-runner pool with stale work.
	concurrency:
	group: ci-${{ github.workflow }}-${{ github.event.pull_request.number \|\| github.ref }}
	cancel-in-progress: true

	permissions:
	contents: read

	jobs:
	classify:
	name: Classify changes
	runs-on: ubuntu-latest
	timeout-minutes: 5
	outputs:
	source_changed: ${{ steps.changes.outputs.source_changed }}
	generated_changed: ${{ steps.changes.outputs.generated_changed }}
	run_checks: ${{ steps.changes.outputs.run_checks }}
	run_catalog: ${{ steps.changes.outputs.run_catalog }}
	selection_mode: ${{ steps.changes.outputs.selection_mode }}
	selected_problem_count: ${{ steps.changes.outputs.selected_problem_count }}
	selected_modules: ${{ steps.changes.outputs.selected_modules }}
	matrix: ${{ steps.changes.outputs.matrix }}
	steps:
	# actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
	with:
	fetch-depth: 0
	persist-credentials: false

	- name: Audit workflow action pins
	run: python scripts/action_pin_audit.py

	- name: Python syntax checks
	run: python -m py_compile scripts/.py scripts/security_probes/.py

	# Install the pinned Lean toolchain without building the project. The
	# dependency selector consumes a graph produced by Lean's header parser;
	# Python never attempts to parse Lean import syntax.
	- uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
	with:
	build: false
	test: false
	lint: false
	use-mathlib-cache: false
	use-github-cache: false

	- name: Export Lean import graph
	run: \|
	set -euo pipefail
	mkdir -p .ci
	lake build EvalTools.CIImportGraph
	lake env lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json

	- name: Select affected catalog problems
	id: changes
	env:
	BASE_SHA: ${{ github.event.pull_request.base.sha \|\| github.event.before }}
	HEAD_SHA: ${{ github.event.pull_request.head.sha \|\| github.sha }}
	run: \|
	set -euo pipefail
	python scripts/select_ci_problems.py \
	--event "$GITHUB_EVENT_NAME" \
	--base "$BASE_SHA" \
	--head "$HEAD_SHA" \
	--shards 8 \
	--import-graph .ci/import-graph.json \
	--github-output "$GITHUB_OUTPUT"

	checks:
	name: Repository checks
	needs: classify
	if: needs.classify.outputs.run_checks == 'true'
	runs-on: ubuntu-latest
	timeout-minutes: 90
	steps:
	- name: Free up disk space
	# jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
	with:
	tool-cache: false
	android: true
	dotnet: true
	haskell: true
	large-packages: true
	docker-images: true
	swap-storage: true

	# actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
	with:
	fetch-depth: 0
	persist-credentials: false

	# leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
	- uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
	with:
	use-mathlib-cache: true

	# Module compilation and tagged-declaration inventory now run in the
	# catalog shards. Keep the cheap whole-repository invariants here.
	- name: Validate manifest structure and module coverage
	run: lake exe lean-eval validate-manifest --structure-only

	- name: Validate catalog lifecycle metadata and frozen sets
	env:
	BASE_SHA: ${{ github.event.pull_request.base.sha \|\| github.event.before }}
	run: \|
	set -euo pipefail
	base_args=()
	if [ -n "$BASE_SHA" ] &&
	[ "$BASE_SHA" != "0000000000000000000000000000000000000000" ] &&
	git cat-file -e "$BASE_SHA^{commit}"; then
	base_args+=(--base-ref "$BASE_SHA")
	fi
	python scripts/validate_catalog.py "${base_args[@]}"

	# Source-only changes intentionally leave generated/index.json for the
	# trusted main regenerator. If a PR touches generated/ itself, however,
	# its committed global index must be current and it may not add an
	# unexpected workspace directory.
	- name: Validate generated index and unexpected directories
	if: needs.classify.outputs.source_changed != 'true' \|\| needs.classify.outputs.generated_changed == 'true'
	run: lake exe lean-eval validate-generated-catalog

	- name: Submission policy smoke check
	run: lake exe lean-eval validate-submission --file generated/two_plus_two/Solution.lean

	- name: Submission policy diff check
	if: github.event_name == 'pull_request'
	env:
	BASE_SHA: ${{ github.event.pull_request.base.sha }}
	HEAD_SHA: ${{ github.event.pull_request.head.sha }}
	run: \|
	set -euo pipefail
	mapfile -t changed_files < <(git diff --name-only "$BASE_SHA".."$HEAD_SHA")
	if [ "${#changed_files[@]}" -eq 0 ]; then
	echo "No changed files; skipping submission diff validation."
	exit 0
	fi
	for path in "${changed_files[@]}"; do
	if [[ ! "$path" =~ ^generated/ ]]; then
	echo "Diff includes repository source; skipping submission-only validation."
	exit 0
	fi
	done
	lake exe lean-eval validate-submission --base "$BASE_SHA" --head "$HEAD_SHA"

	- name: Run Lean unit tests
	run: \|
	lake exe test_validate_submission
	lake exe test_generate
	lake exe test_module_coverage
	lake exe test_check_comparator_installation

	- name: Run Python unit tests
	run: python -m unittest discover -s tests/python -p 'test_*.py'

	security:
	name: Security and scoring smoke tests
	needs: classify
	if: needs.classify.outputs.run_checks == 'true'
	runs-on: ubuntu-latest
	timeout-minutes: 60
	steps:
	- name: Free up disk space
	# jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
	with:
	tool-cache: false
	android: true
	dotnet: true
	haskell: true
	large-packages: true
	docker-images: true
	swap-storage: true

	# actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
	with:
	fetch-depth: 0
	persist-credentials: false

	# leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
	- uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
	with:
	use-mathlib-cache: true

	# actions/setup-go pinned to b7ad1dad (= refs/tags/v7.0.0 as of 2026-07-30).
	- uses: actions/setup-go@b7ad1dad31e06c5925ef5d2fc7ad053ef454303e
	with:
	go-version: '1.25.12'
	cache: false

	- name: Install landrun
	run: \|
	# landrun pinned to 5ed4a3db (zouuup/landrun main HEAD as of 2026-05-04).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	go install github.com/zouuup/landrun/cmd/landrun@5ed4a3db3a4ad930d577215c6b9abaa19df7f99f
	echo "$(go env GOPATH)/bin" >> "$GITHUB_PATH"

	- name: Build lean4export
	run: \|
	set -euo pipefail
	git clone https://github.com/leanprover/lean4export.git .ci/lean4export
	cd .ci/lean4export
	# lean4export pinned to 15f6055e (= refs/tags/v4.33.0 as of 2026-08-14).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	git checkout 15f6055e299ad5b89345e533cc2192f4cc00f659 # pin-audit: exempt -- SHA, see comment
	cp "$GITHUB_WORKSPACE/lean-toolchain" lean-toolchain
	lake build lean4export
	echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"

	- name: Build comparator
	run: \|
	git clone https://github.com/leanprover/comparator.git .ci/comparator
	cd .ci/comparator
	# comparator pinned to 71b52ec2 (leanprover/comparator, originally adopted before 2026-05-04).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	git checkout 71b52ec29e06d4b7d882726553b1ceb99a2499e0 # pin-audit: exempt -- SHA, see comment
	lake build comparator
	echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"

	- name: Build nanoda
	run: \|
	set -euo pipefail
	git clone https://github.com/robsimmons/nanoda_lib.git .ci/nanoda
	cd .ci/nanoda
	# nanoda pinned to 68d5ca9 (robsimmons/nanoda_lib HEAD as of 2026-07-29).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	git checkout 68d5ca9db226849b41a6fff59d796ff19d0a8840 # pin-audit: exempt -- SHA, see comment
	cargo build --release
	echo "$PWD/target/release" >> "$GITHUB_PATH"

	# These probes stay in the mandatory path. Parallelization must not
	# weaken the submission trust boundary.
	- name: Probe sandbox is engaged
	run: python scripts/sandbox_engaged_probe.py --require-tools

	- name: Probe env-var allowlist
	run: python scripts/security_probes/env_dump_probe.py --require-tools

	- name: Refresh smoke-test workspace
	run: lake exe lean-eval generate --problem two_plus_two

	- name: Check comparator installation
	run: lake exe lean-eval check-comparator-installation

	- name: Run eval workflow smoke test
	run: lake exe lean-eval check-eval-workflow

	catalog:
	name: Catalog validation (shard ${{ matrix.shard }}/${{ matrix.shard_count }})
	needs: classify
	if: needs.classify.outputs.run_catalog == 'true'
	runs-on: ubuntu-latest
	timeout-minutes: 60
	strategy:
	fail-fast: false
	matrix: ${{ fromJSON(needs.classify.outputs.matrix) }}
	steps:
	- name: Free up disk space
	# jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
	# Bump procedure: SECURITY.md > "Bumping pinned dependencies".
	uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
	with:
	tool-cache: false
	android: true
	dotnet: true
	haskell: true
	large-packages: true
	docker-images: true
	swap-storage: true

	# actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
	with:
	fetch-depth: 0
	persist-credentials: false

	# leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
	- uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
	with:
	use-mathlib-cache: true
	build: false
	test: false
	lint: false

	- name: Clear cached problem-module artifacts
	run: \|
	set -euo pipefail
	artifact_dir=.lake/build/lib/lean/LeanEval
	if [ -d "$artifact_dir" ]; then
	find "$artifact_dir" $ -type f -o -type l $ -delete
	fi

	- name: Build problem modules without warnings
	env:
	MODULES: ${{ matrix.modules }}
	SHARD_INDEX: ${{ matrix.shard }}
	run: \|
	set -euo pipefail
	IFS=',' read -r -a modules <<< "$MODULES"
	module_args=()
	for module in "${modules[@]}"; do
	module_args+=(--module "$module")
	done
	lake exe lean-eval check-problem-build "${module_args[@]}"
	mkdir -p .ci/problem-inventory
	lake exe lean-eval problem-inventory \
	".ci/problem-inventory/$SHARD_INDEX.json" "${module_args[@]}"

	- name: Generate or verify this shard
	env:
	PROBLEMS: ${{ matrix.problems }}
	SOURCE_CHANGED: ${{ needs.classify.outputs.source_changed }}
	GENERATED_CHANGED: ${{ needs.classify.outputs.generated_changed }}
	EVENT_NAME: ${{ github.event_name }}
	run: \|
	set -euo pipefail
	IFS=',' read -r -a selected <<< "$PROBLEMS"
	if [ "${#selected[@]}" -eq 0 ]; then
	echo "Shard is empty."
	exit 0
	fi
	printf 'Selected problems: %s\n' "${selected[*]}"

	generate_mode="none"
	if [ "$SOURCE_CHANGED" = true ]; then
	generate_mode="write"
	elif [ "$EVENT_NAME" = push ] && [ "$GENERATED_CHANGED" = true ]; then
	generate_mode="check"
	fi
	if [ "$generate_mode" != none ]; then
	for problem in "${selected[@]}"; do
	if [ "$generate_mode" = check ]; then
	lake exe lean-eval generate --problem "$problem" --check
	else
	lake exe lean-eval generate --problem "$problem"
	fi
	done
	fi

	# Every workspace has the same pinned Mathlib dependency. Reuse the
	# root cache with symlinks instead of cloning/decompressing it once
	# and hard-link-walking ~13 GB hundreds of times.
	for problem in "${selected[@]}"; do
	mkdir -p "generated/$problem/.lake"
	ln -s "$GITHUB_WORKSPACE/.lake/packages" \
	"generated/$problem/.lake/packages"
	done
	first="${selected[0]}"
	(cd "generated/$first" && lake update)
	for problem in "${selected[@]:1}"; do
	cp "generated/$first/lake-manifest.json" \
	"generated/$problem/lake-manifest.json"
	done

	build_args=()
	for problem in "${selected[@]}"; do
	build_args+=(--problem "$problem")
	done
	lake exe lean-eval check-generated-builds "${build_args[@]}"

	- name: Upload problem inventory
	# actions/upload-artifact pinned to 043fb46d (= refs/tags/v7.0.1 as of 2026-08-17).
	uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
	with:
	name: problem-inventory-${{ matrix.shard }}
	path: .ci/problem-inventory/${{ matrix.shard }}.json
	if-no-files-found: error
	retention-days: 1

	catalog_inventory:
	name: Manifest inventory aggregate
	needs: [classify, catalog]
	if: needs.classify.outputs.run_catalog == 'true'
	runs-on: ubuntu-latest
	timeout-minutes: 15
	steps:
	# actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
	with:
	persist-credentials: false

	# leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
	- uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
	with:
	use-mathlib-cache: true
	build: false
	test: false
	lint: false

	- name: Download problem inventories
	# actions/download-artifact pinned to 3e5f45b2 (= refs/tags/v8.0.1 as of 2026-08-17).
	uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c
	with:
	pattern: problem-inventory-*
	path: .ci/problem-inventory
	merge-multiple: true

	- name: Validate aggregated manifest inventory
	env:
	MODULES: ${{ needs.classify.outputs.selected_modules }}
	run: \|
	set -euo pipefail
	IFS=',' read -r -a modules <<< "$MODULES"
	module_args=()
	for module in "${modules[@]}"; do
	module_args+=(--module "$module")
	done
	lake exe lean-eval validate-manifest \
	--inventory-dir .ci/problem-inventory "${module_args[@]}"

	# Preserve the existing required-check name while making it an aggregate of
	# every parallel branch. A green `verify` now means the entire fan-out passed.
	verify:
	name: verify
	if: always()
	needs: [classify, checks, security, catalog, catalog_inventory]
	runs-on: ubuntu-latest
	timeout-minutes: 2
	steps:
	- name: Require every CI branch to pass
	env:
	CLASSIFY_RESULT: ${{ needs.classify.result }}
	CHECKS_RESULT: ${{ needs.checks.result }}
	SECURITY_RESULT: ${{ needs.security.result }}
	CATALOG_RESULT: ${{ needs.catalog.result }}
	CATALOG_INVENTORY_RESULT: ${{ needs.catalog_inventory.result }}
	run: \|
	set -euo pipefail
	for result in "$CLASSIFY_RESULT" "$CHECKS_RESULT" \
	"$SECURITY_RESULT" "$CATALOG_RESULT" \
	"$CATALOG_INVENTORY_RESULT"; do
	if [ "$result" != success ] && [ "$result" != skipped ]; then
	echo "A required CI branch ended with: $result" >&2
	exit 1
	fi
	done

Navigation Menu

Uh oh!

Record the current f03 staging gate #1425

Workflow file

Record the current f03 staging gate #1425

Uh oh!

Workflow file for this run