Repository navigation
Conversation
|
Fresh coordination review at head 7d86fa6: this draft overlaps existing #419/#426 and the accepted #271 Host plan. I am arranging a bounded source/evidence review before deciding the delivery relationship; neither #419 nor the broad #271 is closed by this draft. The maintainer's sole active identity wave is #393 + #390 + #292 on release/v0.4, currently in its one official verification writer. The reviewed v0.5 source preparation already combines #405, landed Host/DF19/#396, initial #362, #437 and the active #433 pin inputs. Please report the exact writer/process state and immutable source/output evidence for this draft. If an atomic writer is already running, preserve its logs and finish it safely; do not start another identity/product wave or full matrix before the shared source integration is agreed. Keep authored changes distinct from derived outputs and preserve the known BS-09 failure rather than treating vector agreement as a complete pass. The 10 MiB certificate-part and 600-second timeout changes require their concrete failure evidence and contract review alongside the driver and cleanup plants. A source review is not final runtime, identity, corpus or gate acceptance. This PR remains draft while those obligations are unresolved; no duplicate implementation is being created. |
afflom
left a comment
There was a problem hiding this comment.
Source review of 7d86fa6 found a concrete renderer-identity omission. New calculus/rust/host.rs selects Host shapes and effect-specific driver parts, rewrites imports and prints src/main.rs (driver/main_rs). Yet calculus/rust/mod.rs::RENDERER_FILES and the canonical renderer unit's include_bytes array still contain nine files and omit host.rs. Changing this new output-producing source could therefore leave the renderer fingerprint unchanged. Include host.rs in both official ordered renderer inputs before the coordinated canonical pin/product regeneration; do not patch a literal digest or bypass the unit.
Existing renderer inputs mod.rs/package.rs also changed while the language-1.2 renderer pin remains the base pin, so the current partial checks/products are not final identity acceptance. Complete the authored source unit first and coordinate it with the existing v0.5 union; this review does not request another independent writer or full matrix. The new runtime asset's explicit 1.2 partition and matching landed Host interface are positive source observations, not proof of all runtime outcomes.
#419's accepted RB-24 work and ownership still need an explicit delivery/reconciliation record: this single commit is based on 2b039 and does not retain that contributor history. Keep #419/#426 and the broad #271 open pending that decision and accepted delivery. The reported BS-09 failure, configuration-limit evidence, missing artifacts and complete final gate also remain outstanding. This is a COMMENT review on a self-authored PR, not an approval.
afflom
left a comment
There was a problem hiding this comment.
Addressed the renderer-identity finding in 2aced32: host.rs is now in both ordered renderer input lists. The canonical unit failed against the old pin, computed a24f0546f398576cd7bf755dd5953be17db6f418cae95ae4bf40e7c1b5a53be8, and passed after recording that identity. Historical language-1.0 and 1.1 identities remain unchanged; the development compiler now reports language-1.2 identity b9816b388a3eb1800179f96aa9bc789620a46d7a7132f1b52ee9fa404c2092f7.
The commit and VERIFICATION.md explicitly credit the RB-24 port from humuhumu33's #419 through b70b546, on #396, and leave #419/#426/#271 open. The interrupted old-identity artifact run is not final acceptance. Final regeneration and the complete gate remain pending, so this PR remains a draft. Rule30 is proceeding against this development compiler while those upstream artifacts are completed.
afflom
left a comment
There was a problem hiding this comment.
Bounded source re-review confirms the prior renderer-input omission is fixed in 2aced32: host.rs appears in both matching ten-entry ordered input lists, and the canonical comparison remains intact. The four-file delta also includes a RuntimeValidate Context refactor; its changed reads/constructions preserve the imported/root/effect/package fields in source. Explicit #419 credit and the open-issue scope are now recorded.
This resolves that source finding, not final identity/runtime/product acceptance. The reported canonical fail/pass, b981 development identity and certificate measurements remain author-provided evidence; the old interrupted writer is not an accepted final run. Please retain its terminal log and report whether any new writer is active. Coordinate final source with the pending forward/Mathlib/formatting/Lean-upgrade integration before another identity/product wave or matrix. #419's delivery relationship still needs reconciliation; #419/#426/#271 remain open. The final BS-09 certificate/kernel evidence and full integrated gate are still required.
Register CL-25 and expose the existing Engine snapshot through the CLI. Preserve its exact linked IR and closure, normal selection, read-only behavior and registered failures. The named case failed before implementation; CL-01, CL-19 and CL-25 pass with Clippy. Language identities remain unchanged. Full driver and artifact acceptance remains pending in the draft PR.
afflom
left a comment
There was a problem hiding this comment.
Bounded review of b0e40ad against 2aced32: the ten-file delta adds the snapshot CLI adapter and its source contracts/projections. The earlier host.rs renderer-input correction remains intact; this delta does not change RuntimeValidate, renderer inputs, pins, negative fixtures or generated products. No additional standalone implementation blocker was found in this source inspection; reported test passes are not independently reproduced acceptance.
There is a concrete integration collision: the reviewed initial Mathlib preparation for #405/#362 already uses CL-25 for lexlean deps glossary, including its scenario, dispatch and named test. This draft uses CL-25 for lexlean snapshot. Preserve both capabilities and their complete acceptance obligations when reconciling the authoritative IdsCL/Chapter23 sources, scenario, dispatch, named tests and official projections; do not overwrite either registration. Please coordinate the identifier allocation before combining these sources. This does not make #439 an automatic prerequisite of the existing forward wave.
The body now reports no upstream writer active and deliberately stopped partial fixture generation. Preserve those terminal/interruption receipts and completed outputs; no additional identity/product wave or full matrix should start before the shared source freeze. This commit contains no new lock/golden/fixture completion evidence. BS-09 certificate acceptance, final products, full integrated CI and the #419 ownership/delivery relationship remain pending. #419/#426/#271 stay open.
|
To resolve the reviewed identifier collision concretely: retain CL-25 for the already prepared initial Mathlib Please make the bounded rename on this existing branch across the authoritative IdsCL/Chapter23 registration, scenario/tag, dispatch and named case, preserving the complete snapshot statement and every assertion. Keep both capabilities when combining sources. Generated model/SPEC/CONFORMANCE projections remain owned by the official writer in the coordinated source workflow; do not hand-edit them or start another identity/product wave for this allocation. Preserve the original fail-first and completed local evidence as history rather than rerunning unchanged functional work solely for the identifier change. No duplicate implementation or automatic inclusion in #405 is requested. Existing runtime/product/BS09/full-gate and #419 delivery obligations remain unchanged; #419/#426/#271 remain open. |
A production root with the Host step signature can now produce an executable Rust package. The driver is authored as LexLean RuntimeSyntax data, validates the admitted file/process effects, and retains child-process ownership through normal session destruction.
This ports and completes the command-driver work from #419 and the effect eligibility work from #389 on the v0.5 line after #396. It includes the LexLean bootstrap validator, conditional-platform validation, package-context encoding, negative capability cases, and child cleanup defect probes. The renderer identity now covers host.rs in both ordered input lists; VERIFICATION.md and the source commit explicitly credit humuhumu33's #419 work.
Native consumers also need the compiler's exact identity inputs. CL-25 exposes the existing public Engine snapshot through
lexlean snapshot, with normal discovery/selection and canonical JSON in both diagnostic modes. Each module's full linked_ir and the envelope's lexicon_closure reconstruct the semantic identity inputs. This command writes no artifacts and runs no backend. Its addition preserves all language identities.Validation completed:
The PR remains a draft. The expanded BS-09 corpus previously reached agreement for 747 compiled and 741 bounded evaluator vectors before its certificate-size failure; that is not a completed BS-09 pass. Final example verification, production exports, fixture completion and the full normative gate remain required. Bootstrap states a 10 MiB certificate-part limit and a 600-second child timeout based on measured failures. Large verification runs are serialized in the 16 GiB development workspace.
This is progress on #271; #419/#426/#271 remain open. Ordinary destruction terminates/reaps owned children; an external forced-termination watchdog is outside this change. No remote model is used.
Downstream validation: afflom/rule30#5 merged after its unchanged pre-commit gate, maintainer self-review, and successful CI. That change pins ancestor
2aced32e0f9c1ca0cf160f150a04819dedb4fc04, accepts all 64 API elaborations/kernel replays and production-preservation certificates, and exercises the generated native R30 entry. The snapshot-command integration on this PR's currentb0e40addhead is accepted downstream: afflom/rule30#6 merged after the unchanged pre-commit gate, maintainer self-review and successful CI. All 68 API elaborations/kernel replays, exact axiom policies and 27 production roots' certificates passed. Actual generated-Rust execution accepted a contextual proof after owned snapshot/verify processes; a valid source change between those successful processes preserved semantic identity but was rejected on source identity. Both cases left no owned child. This evidence does not replace the outstanding upstream acceptance work listed above.