Open
Conversation
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
_KNOWN_VERSIONSso downstream consumers can upgrade on their own cadence. Unblocks Aeneas, which requires Lean 4.28+.nightly-2026-02-07). Pure-Bazel, zero external host tools, usesCHARON_TOOLCHAIN_IS_IN_PATH=1to skip rustup.draft→in_progress.tests/charon_validator/— head-to-head evaluation harness used for the decision, preserved as a reusable tool.Why
Issue #1 is the pipeline blocker: the Rust → LLBC step (Charon) was missing. A Nix-based alternative was implemented in parallel and compared with a validator; rejected because pure-Bazel keeps the hermeticity contract identical to Lean/Mathlib toolchain handling (SHA-256 enforcement, no ambient host tools, no daemon requirement). See DD-007 in
artifacts/architecture.yamlfor the full rationale.Charon has no prebuilt for
linux_aarch64; that platform gets a fail-fast stub. Matches the Aeneas release's own platform coverage.Test plan
Not in this PR
Commits
`fac3749` bumps Lean + Mathlib. `5953a29` merges Track A with commit history preserved (`8d9ab42` + `c2be9f7`). `1692143` records the decision.
🤖 Generated with Claude Code