Reuse Lake builds in Codex worktrees #462

	name: Verifier Freshness

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

	jobs:
	freshness:
	name: Programs up to date
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v5

	# The verifier executable doesn't need Mathlib (see PR #12), so we
	# skip the mathlib cache entirely.
	- uses: leanprover/lean-action@v1
	with:
	lake-package-directory: verifier
	build-args: verifier
	use-mathlib-cache: false

	# Pre-install the rustc version pinned by programs/rust/rust-toolchain.toml
	# (with the wasm32 target it declares) so the first cargo invocation
	# doesn't have to download it mid-build.
	- name: Install pinned Rust toolchain
	working-directory: programs/rust
	run: rustup show active-toolchain \|\| rustup toolchain install

	# wasm-tools is needed by `verifier check` (wat printer).
	- name: Install wasm-tools
	uses: taiki-e/install-action@v2
	with:
	tool: wasm-tools

	# Re-emit every Program.lean from the committed wasm sources.
	# `--no-prove` skips the final `lake build` — proof correctness is
	# covered by the main CI job; here we only check for drift.
	- name: Regenerate programs
	working-directory: programs
	run: lake -d ../verifier exe verifier check --no-prove

	# Fail if any generated file changed.
	- name: Assert no drift
	run: \|
	git diff --exit-code -- programs/ \
	\|\| { echo ""; echo "Generated files are out of date. Re-run:"; \
	echo " cd programs && lake -d ../verifier exe verifier check --no-prove"; \
	exit 1; }

Provide feedback