name	updating-aeneas-charon
description	Use when bumping the pinned Charon or Aeneas release tag in this repo — walks the coupled set of values that must move together, the regeneration/build sequence, and the known drift points enforcement catches.

Updating Aeneas / Charon versions

Charon and Aeneas publish nightly pre-release tags; this repo pins specific ones for reproducibility. Aeneas bumps are the hard case because three values must stay in lockstep and a fourth (the patch list) often needs pruning.

Coupled values

#	File	Value
1	`scripts/gen_lean.sh`	`AENEAS_TAG` — the 40-hex suffix is the Aeneas release commit
2	`proof/lakefile.toml`	`rev` — must equal that 40-hex hash
3	`scripts/gen_lean.sh`	`LEAN_TOOLCHAIN` constant
4	`proof/lean-toolchain`	must equal `LEAN_TOOLCHAIN` exactly

Charon has its own tag (CHARON_TAG) and is independently versioned — don't force it to move in lockstep with Aeneas.

Workflow

Pick new CHARON_TAG and/or AENEAS_TAG from the GitHub release pages of AeneasVerif/charon and AeneasVerif/aeneas.
Update AENEAS_TAG in scripts/gen_lean.sh and the matching rev in proof/lakefile.toml.
If the new Aeneas release ships a different Lean toolchain (check backends/lean/lean-toolchain in the Aeneas tarball), update both LEAN_TOOLCHAIN in scripts/gen_lean.sh and proof/lean-toolchain to match.
Review the aeneas-patches block (Step 4 in gen_lean.sh) — remove patches for bugs now fixed upstream, add new ones if the release introduces them. If the list is unchanged, make a no-op whitespace touch so blockwatch sees the review.
Run make lean-bootstrap (downloads the pinned binaries) then cd proof && lake update && lake build.
If lake build fails, inspect the failure — either a new Aeneas bug needs a patch in Step 4, or the Lean toolchain is wrong.

What enforcement catches (and what it doesn't)

blockwatch (affects): forces aeneas-tag, aeneas-rev, lean-toolchain, and aeneas-patches to all appear in the same diff.
blockwatch (line-pattern): rejects malformed CHARON_TAG / AENEAS_TAG / LEAN_TOOLCHAIN / rev values (truncated hash, wrong shape).
scripts/check_versions.sh (pre-commit hook + gen_lean.sh preflight): asserts that the actual values agree — AENEAS_TAG suffix == lakefile.toml rev, and proof/lean-toolchain == LEAN_TOOLCHAIN.
Not caught statically: proof/lake-manifest.json drift (regenerated by lake update) and whether the committed proof/Simplex/{Types,Funs}.lean match a fresh make lean run. CI's lean-proof job catches the latter by building.

Common mistakes

Bumping AENEAS_TAG but forgetting rev in lakefile.toml — blockwatch blocks the commit, check_versions.sh catches the value mismatch.
Skipping lake update after changing rev — lake-manifest.json stays on the old hash; build may still work locally due to cache but CI will diverge.
Leaving stale patches in Step 4 when upstream has fixed them — Lean compilation often still works but the Funs.lean/Types.lean post-processing becomes a no-op that quietly drifts. Check each patch on every bump.
Assuming a Charon bump is independent — it usually is, but a Charon version that emits LLBC a newer Aeneas doesn't understand (or vice versa) will surface as an Aeneas error on step 2.

Updating Aeneas / Charon versions

Coupled values

File

Value

scripts/gen_lean.sh

AENEAS_TAG — the 40-hex suffix is the Aeneas release commit

proof/lakefile.toml

rev — must equal that 40-hex hash

scripts/gen_lean.sh

LEAN_TOOLCHAIN constant

proof/lean-toolchain

must equal LEAN_TOOLCHAIN exactly

Charon has its own tag (CHARON_TAG) and is independently versioned — don't force it to move in lockstep with Aeneas.

Workflow

Pick new CHARON_TAG and/or AENEAS_TAG from the GitHub release pages of AeneasVerif/charon and AeneasVerif/aeneas.

Update AENEAS_TAG in scripts/gen_lean.sh and the matching rev in proof/lakefile.toml.

If the new Aeneas release ships a different Lean toolchain (check backends/lean/lean-toolchain in the Aeneas tarball), update both LEAN_TOOLCHAIN in scripts/gen_lean.sh and proof/lean-toolchain to match.

Review the aeneas-patches block (Step 4 in gen_lean.sh) — remove patches for bugs now fixed upstream, add new ones if the release introduces them. If the list is unchanged, make a no-op whitespace touch so blockwatch sees the review.

Run make lean-bootstrap (downloads the pinned binaries) then cd proof && lake update && lake build.

If lake build fails, inspect the failure — either a new Aeneas bug needs a patch in Step 4, or the Lean toolchain is wrong.

What enforcement catches (and what it doesn't)

blockwatch (affects): forces aeneas-tag, aeneas-rev, lean-toolchain, and aeneas-patches to all appear in the same diff.

blockwatch (line-pattern): rejects malformed CHARON_TAG / AENEAS_TAG / LEAN_TOOLCHAIN / rev values (truncated hash, wrong shape).

scripts/check_versions.sh (pre-commit hook + gen_lean.sh preflight): asserts that the actual values agree — AENEAS_TAG suffix == lakefile.toml rev, and proof/lean-toolchain == LEAN_TOOLCHAIN.

Not caught statically: proof/lake-manifest.json drift (regenerated by lake update) and whether the committed proof/Simplex/{Types,Funs}.lean match a fresh make lean run. CI's lean-proof job catches the latter by building.

Common mistakes

Bumping AENEAS_TAG but forgetting rev in lakefile.toml — blockwatch blocks the commit, check_versions.sh catches the value mismatch.

Skipping lake update after changing rev — lake-manifest.json stays on the old hash; build may still work locally due to cache but CI will diverge.

Leaving stale patches in Step 4 when upstream has fixed them — Lean compilation often still works but the Funs.lean/Types.lean post-processing becomes a no-op that quietly drifts. Check each patch on every bump.

Assuming a Charon bump is independent — it usually is, but a Charon version that emits LLBC a newer Aeneas doesn't understand (or vice versa) will surface as an Aeneas error on step 2.

updating-aeneas-charon