Charon Stage 2: charon_llbc + aeneas pipeline, shared mathlib shallow-fetch (#7/#8/#9) by avrabe · Pull Request #11 · pulseengine/rules_lean

avrabe · 2026-06-05T19:20:11Z

Lands the Charon Stage-2 work and the audit follow-ups, all CI-green on self-hosted runners.

What's in here

Pipeline (FEAT-006, advances #1):

charon_llbc rule (Rust → LLBC via charon rustc, Rust-sysroot wiring) — CI-proven.
aeneas_translate end-to-end Level 1 (LLBC → Lean via the aeneas binary), with a coherent dev-mode pin: charon build-2026.04.22 (unchanged) + aeneas build-2026.04.22.084123-1a89… + Lean 4.28.0-rc1.
Fixed: aeneas binary lives at the tarball root, not bin/ (CI caught it).

#7 — full mathlib-clone elimination, shared across BOTH libraries:

New lean/private/mathlib_fetch.bzl (shallow_fetch_mathlib + rewrite_git_require_to_local).
mathlib_repo refactored onto it (behavior-preserving; build-mathlib green).
aeneas_lean_lib now shallow-fetches mathlib v4.28.0-rc1 + redirects aeneas's lakefile instead of a full clone (build-aeneas-lean-lib green, ~15 min).

#8 — charon validator: routes all charon commands into tests/charon_smoke with the real //:charon_bin (the @charon_toolchain// label never existed).

#9 — hygiene: FEAT-006→DD-007 typed link, refreshed AGENTS.md counts, single-sourced the charon 0.1.181 version, fixed the smoke set -e RC capture. (#9's platform-map dedup was reassessed as a non-issue — the maps use different key vocabularies.)

CI / infra: merged main's #6+#7; migrated Linux jobs to the org self-hosted pool (light for queries, rust-cpu for builds); added build-charon, build-charon-llbc, build-aeneas-lean-lib jobs.

Validation

All 9 CI jobs green on the latest branch run, including the heavy build-aeneas-lean-lib. The full Rust → LLBC → Lean chain plus both Mathlib-fetching libraries are exercised end-to-end.

Not included (tracked)

Level-2 compile of the aeneas-generated Lean (needs TreeArtifact → lean_library; genuine FEAT-006 remainder — Finish Aeneas end-to-end pipeline: add hermetic Charon, reuse rules_verus sysroot pattern #1 stays open).
rivet validate status-vocabulary remap (a rivet tool update, unrelated).

Closes #7
Closes #8
Closes #9

🤖 Generated with Claude Code

Unblocks FEAT-006 (Aeneas integration): Aeneas main requires Lean 4.28+, which the previous 4.27.0 pin could not satisfy. 4.29.1 is the current latest stable; 4.27.0 stays registered so downstream consumers can upgrade at their own cadence. Exercises REQ-002 (Lean-Mathlib version match) and LS-001 (version bump without Mathlib bump) by changing both pins in lockstep. Verified hello_lean builds green under 4.29.1 with SHA-256 enforcement on. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Introduce CharonToolchainInfo + charon_toolchain_info rule alongside the existing Aeneas provider, plus aeneas/private/charon_repo.bzl with charon_release / charon_toolchains_hub. Extend the aeneas module extension with a charon_toolchain tag class and wire a version registry with real SHA-256 hashes for build-2026.04.22.081730 and its matching nightly-2026-02-07 Rust sysroot (rustc, rust-std, rustc-dev, rust-src for all three published platforms plus a fail-fast linux_aarch64 stub). Also adds tests/charon_smoke + docs/charon-integration.md describing the linux_aarch64 limitation and downstream env-var requirements (CHARON_TOOLCHAIN_IS_IN_PATH). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Load sh_test from rules_shell (required in Bazel 8), fix the alias selects to use per-platform config_setting targets (nested select is illegal), and add a supplementary genrule //tests/charon_smoke:charon_version_check that exercises the downloaded `charon version` at build time. The genrule run confirms `charon version output: 0.1.181` on darwin_aarch64. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Integrates charon_release repo rule with SHA-256-pinned downloads of Charon + matching Rust sysroot (rustc, rust-std, rustc-dev, rust-src from nightly-2026-02-07). Adds charon_toolchain_type, CharonToolchainInfo provider, charon_toolchains_hub, and _CharonToolchainTag on the aeneas extension. Smoke test builds `charon version` → "0.1.181" via a sandbox'd genrule; no rustup, no ~/.cargo, no Nix required. linux_aarch64 has a fail-fast stub (no upstream prebuilt). Track B (Nix-based alternative) was evaluated in parallel and rejected — see DD-007 for rationale. Validator in tests/charon_validator/. Unblocks FEAT-006 Aeneas end-to-end pipeline (charon_llbc rule follows). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…alidator DD-007 captures the Track A vs Track B comparison and the rationale for rejecting the Nix-based alternative: pure-Bazel keeps hermeticity contract identical to Lean/Mathlib, avoids a hard Nix-on-host dependency on every developer machine and CI runner, and reuses the rules_verus sysroot pattern for cross-ruleset consistency. FEAT-006 moves to in_progress: the Charon toolchain half is in; the charon_llbc build rule and end-to-end example remain. tests/charon_validator/ is the head-to-head evaluation harness used for the decision — left in place as a reusable tool for future toolchain-strategy comparisons. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

`lake update` clones mathlib4 (a large repo with full git history). On a cold cache / slower network the 600 s timeout killed the clone mid-fetch ("Server terminated abruptly: Socket closed"), failing the @mathlib repo rule. 3600 s gives the clone room to finish. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The validator built `@charon_toolchain//:charon_bin`, a repo that is never created — the aeneas extension makes per-platform `charon_<platform>` repos plus a host-select alias `//:charon_bin`, and that alias is wired ONLY in the tests/charon_smoke module (the root module does not use_repo the charon repos). So every gate failed on a clean tree: the label could not resolve at all. Route all charon bazel commands (build, smoke `run`, reproducibility build, and the `bazel info` helpers that locate the binary / cache) into tests/charon_smoke and use the package-relative `//:charon_bin`. Validated: `//:charon_bin` resolves there via `bazel query`; `bash -n` passes. The full comparison run needs two charon worktrees to exercise end-to-end and is not covered here. Left intentionally unchanged: the fallback `grep 'PASSED'` matches `bazel test` summary output, which is correct. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

#9) - Add a `derives-from` link from FEAT-006 to DD-007 (the Charon feature derives from the pure-Bazel design decision), clearing the `rivet validate` warning "prose mentions 'DD-007' but no typed link". `derives-from` is the established link type here (9 uses); `implements`/`traces-to` were unattested or weaker. - Regenerate AGENTS.md (`rivet init --agents`): artifact counts were stale (67→71 total, design-decision 6→7, loss-scenario 4→6, system-constraint 7→8). rivet validate now PASS with 9 warnings (was 10). CLAUDE.md left as its original markerless hand-authored shim — rivet's CLAUDE.md regen folds free-form content back inside the managed markers, so markerless is the safe state (rivet refuses to touch it without --force-regen). The "Documents: (none configured)" line is emitted by the generator itself despite rivet.yaml's `documents:` block — a rivet quirk, not a project artifact issue. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…re (#9) The expected `charon version` string "0.1.181" was hardcoded in three places that could silently desync on a toolchain bump: - tests/charon_smoke/BUILD.bazel genrule - tests/charon_smoke/charon_version_smoke.sh - tests/charon_validator/run.sh Single-source it on the new `CHARON_EXPECTED_VERSION` constant in tests/charon_smoke/BUILD.bazel: the genrule reads it via cmd .format(), the sh_test passes it as argv[2] (the script now reads $2), and the validator derives its default by grepping that constant (env var still overrides). The remaining literals are only safety fallbacks for manual invocation. Also fix the latent bug the audit flagged in charon_version_smoke.sh: under `set -euo pipefail`, `OUTPUT=$(...); RC=$?` aborted before the RC check could run on a non-zero `charon version`; wrap the capture in `set +e`/`set -e` so the "FAIL: charon version exited N" diagnostic is reachable. Validated: `bash -n` on both scripts, the validator's grep extracts "0.1.181" from the BUILD constant, and the charon_smoke targets resolve via `bazel query`. Full execution needs a charon build (not in CI; local disk-blocked). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Adds a `build-charon` CI job that builds //:charon_version_check (the genrule that downloads the pinned charon + Rust sysroot and asserts the version) and runs the //:charon_version_smoke sh_test, from the tests/charon_smoke module (which wires the Charon toolchain — the root module does not). On ubuntu-latest the host is linux_x86_64, a real prebuilt rather than the linux_aarch64 fail-fast stub. This is the missing validation path for the Charon track: it makes the charon build provable in CI, which in turn unblocks validating the deferred full-mathlib-clone elimination in aeneas_lean_lib (#7) and any further charon hygiene. It runs once feature/charon-stage-2 is pushed / PR'd to main (the workflow triggers on main; tests/charon_smoke exists only on this branch). YAML validated (parses; 6 jobs) and both target labels resolve via `bazel query`. First real execution happens on push. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Temporary: adds the branch to push triggers (and workflow_dispatch) so the new Charon smoke job runs before charon-stage-2 lands on main. Remove the branch from the trigger list once merged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

@rpath

…on (FEAT-006) Completes the charon_llbc half of the Aeneas pipeline (FEAT-006 remaining work). - aeneas/private/charon.bzl: charon_llbc rule — translates Rust sources to a single .llbc via `charon rustc --preset=aeneas`, wiring the bundled Rust sysroot (PATH + DYLD/LD_LIBRARY_PATH so charon-driver resolves librustc_driver at @rpath without rustup). Provides CharonLlbcInfo for aeneas_translate. - aeneas/defs.bzl: export charon_llbc + CharonLlbcInfo. - tests/charon_llbc: minimal Rust crate + charon_llbc target + a build-time genrule asserting a non-empty .llbc. - ci.yml: build-charon-llbc job builds //:hello_llbc_check on Linux — the validation path now available because build-charon proved the charon toolchain + Rust sysroot download on CI. The LLBC→Lean half (aeneas_translate + @aeneas_lean_lib) and the aeneas_lean_lib full-clone elimination (#7) are the next step, tracked separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Brings the validated #6 (mathlib shallow-fetch + skew-fail) and #7 (aeneas_lean_lib fail-loud hardening) fixes, plus the smithy CI canary, onto the Charon branch so the aeneas pipeline can build aeneas_lean_lib without the 600s full-clone timeout. Conflict resolution: - lean/private/repo.bzl: took main's #6 shallow-fetch rewrite (supersedes the charon-side 600→3600 timeout band-aid 77b419a). - .github/workflows/ci.yml: took main's jobs (nightly ℝ cold-cache, ℝ build/test, skew test, smithy canary) and re-added the charon jobs (build-charon, build-charon-llbc) + the feature/charon-stage-2 push trigger. - lean/extensions.bzl auto-merged: main's skew-fail rewrite + charon's 4.29.1 registry entry both retained. - aeneas/private/repo.bzl: main's #7 hardening (charon never changed it). - MODULE.bazel / examples: kept charon's 4.29.1 pin. Note: `rivet validate` now reports status-vocabulary errors (reviewed/accepted/ in_progress no longer allowed) — a rivet tool update, NOT from this merge (artifacts/ is byte-identical to pre-merge). Tracked separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…affold Wires the Aeneas binary toolchain so the pipeline reaches Lean, using a coherent same-era pin (research notes below). Dev-mode: no sha256 yet — pin once green. Pinned set (all from 2026-04-22, so charon/aeneas LLBC formats align): - charon: build-2026.04.22.081730-2d35584… (UNCHANGED — already CI-green). - aeneas: build-2026.04.22.084123-1a89… (rev 1a8946778f…). - lean_version: 4.28.0-rc1 — this aeneas's backends/lean/lean-toolchain. Aeneas always tracks bleeding-edge Lean (4.28.0-rc1 in April, 4.30.0-rc2 now), none of which rules_lean stably pins, so the aeneas Lean lib uses the RC directly. tests/charon_llbc: - MODULE.bazel: add aeneas.toolchain(...) + use_repo the aeneas repos + register @aeneas_toolchains//:all. - BUILD.bazel: aeneas_translate(:hello_lean) over the charon LLBC + a genrule asserting ≥1 .lean file. This is Level 1 — it runs the aeneas BINARY (LLBC→.lean) but does NOT compile, so it avoids the heavy @aeneas_lean_lib build (and #7's full-clone path). - ci.yml: build-charon-llbc also builds //:hello_lean_check. Validated structurally (bazel query resolves //:hello_lean[_check]); full execution pending CI (runners currently contended). Level 2 (compile the generated Lean against @aeneas_lean_lib) + #7's full-clone elimination follow once Level 1 is green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…tern) ubuntu-latest (GitHub-hosted Linux) is no longer allocated for this repo — heavy jobs queued indefinitely while only verify-rules (migrated to self-hosted by the smithy canary) ran. Sibling repos (synth, meld, loom, rivet) use a self-hosted pool with two labels: 'light' for query/lint jobs and 'rust-cpu' for heavy builds. Apply that pattern: - query jobs (test-hash-enforcement, test-platform-downloads) -> light - build jobs (build, build-mathlib, nightly, build-charon, build-charon-llbc) -> rust-cpu - macos-latest kept (GitHub-hosted mac still works). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Extract the #6 shallow-fetch-mathlib logic into lean/private/mathlib_fetch.bzl so the single source serves both Mathlib-fetching repo rules: - shallow_fetch_mathlib(rctx, rev): git init + origin remote + `git fetch --depth 1 <rev>` + checkout FETCH_HEAD + lakefile sanity-check; returns the local checkout path. (Keeps .git + origin for `lake exe cache get`.) - rewrite_git_require_to_local(rctx, lakefile, dep, path): rewrite a downloaded lakefile's `require <dep> from git ... @ "..."` to a local-path require. mathlib_repo (lean/private/repo.bzl): now calls the helper instead of the inline git dance — behavior-preserving (validated: skew query + build-mathlib path). aeneas_lean_lib (aeneas/private/repo.bzl): THE #7 DEEP FIX. Aeneas's backends/lean/lakefile.lean does `require mathlib from git @ "v<lean>"`, which made `lake update` full-clone mathlib4 (~2 GB). Now we shallow-fetch that exact rev ("v"+lean_version, which is what Aeneas pins) and redirect the require at the local checkout, so `lake update` only resolves the small transitive deps — the same elimination @mathlib already got, now shared. Lean side validates via build-mathlib (CI). Aeneas side executes only when @aeneas_lean_lib is built (Level-2 compile, wired next). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

CI caught it: aeneas_translate failed with 'aeneas_linux_x86_64/bin/aeneas: No such file or directory' (exit 127). The aeneas release tarball ships the binary as `aeneas` at the root (with backends/ as a sibling), unlike charon's bin/ layout. Point the filegroup + chmod at `aeneas`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…fetch Forces @aeneas_lean_lib to fetch+build, exercising the #7 deep fix (shallow-fetch mathlib v4.28.0-rc1 + lakefile redirect) on a real CI build. Heavy (mathlib + aeneas lib), so a separate 60-min job. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

avrabe and others added 19 commits April 22, 2026 20:04

ci: drop temporary feature/charon-stage-2 push trigger (landing on main)

3f35cb4

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

avrabe merged commit 364ab19 into main Jun 5, 2026
10 checks passed

avrabe deleted the feature/charon-stage-2 branch June 5, 2026 19:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Charon Stage 2: charon_llbc + aeneas pipeline, shared mathlib shallow-fetch (#7/#8/#9)#11

Charon Stage 2: charon_llbc + aeneas pipeline, shared mathlib shallow-fetch (#7/#8/#9)#11
avrabe merged 19 commits into
mainfrom
feature/charon-stage-2

avrabe commented Jun 5, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

avrabe commented Jun 5, 2026

What's in here

Validation

Not included (tracked)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant