ci: !benchmark fixes - #575
Merged
Merged
Conversation
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
samuelburnham
enabled auto-merge (squash)
August 20, 2026 01:06
arthurpaulino
approved these changes
Aug 20, 2026
Merged
johnchandlerburnham
added a commit
that referenced
this pull request
Aug 20, 2026
Since #575 stopped exporting RUSTFLAGS, .cargo/config.toml's -Ctarget-cpu=native is authoritative in CI. That is the point for the warp jobs (bench artifact reuse, with CPU provenance logged), but rust-test runs on ubuntu-latest — a heterogeneous fleet sharing one cargo cache. A proc-macro dylib or test binary compiled native on an AVX-512 runner SIGILLs when a later run lands on a non-AVX-512 one; clippy-driver died with SIGILL checking aiur off a cached tracing-attributes exactly this way, and nextest --run-ignored all executes release test binaries with the same exposure. Pin the job to -Ctarget-cpu=x86-64-v3 (AVX2 — the baseline every GitHub-hosted x64 runner provides). RUSTFLAGS participates in the rust-cache key, so this also re-keys away from the poisoned native-built cache entries.
johnchandlerburnham
added a commit
that referenced
this pull request
Aug 20, 2026
…e surgery + egress hints channel (#578) * fix(kernel): emit the [app diff] dump on stderr The IX_APP_DIFF AppTypeMismatch trace logged through the log facade, but no log backend is installed in the CLI or test binaries, so every dump was silently dropped — the same failure mode #571 fixed for the inductive.rs canonicity dumps. Emit on stderr like those, and include the failing constant's debug label in the header line since the dump is only legible next to the constant it fired in. * fix(egress): carry the per-name hints channel through ixon_egress rebuild_named copied a Named entry's meta and original fields but dropped hints. Decompile reconstructs DefinitionVal.hints from the per-name channel (absent → Opaque), and roundtrip_block Phase B validates each decompiled aux constant's Lean-level hash — which includes hints — against the source env. On the kernel egress leg every regenerated .casesOn/.recOn/.below/.brecOn therefore failed that validation (Opaque vs Abbrev, 4846 spurious Pass-2 errors on a full env), recovery's own hash check failed the same way, and the raw generated form shipped in place of the metadata-restored one. That substitution was invisible while raw regeneration was name-faithful; it surfaced as kernel-ixon-roundtrip mismatches once two things landed on top of it: #571's Phase-3b below.casesOn regeneration (whose below-rec input is regenerated in the decompile work env, where the original below ctors are not yet present, so the IH binder falls back to a bare `ih`) and v4.33's _hygCtx hygienic binder names in IndPredBelow output (ih._@.<module>.<hash>._hygCtx ._hyg.N), which made the fallback visibly diverge for every inductive predicate's below.casesOn (Nat.le, List.Forall₂, DHashMap.Raw.WF, …). With hints preserved, Phase B's restoration lands and the full-env kernel roundtrip is clean again: 169194 constants verified, 0 errors, 0 aux_gen diffs. * fix(compile): call-site surgery for Prop-below ctors and below.casesOn On a Prop-valued MUTUAL inductive-predicate family, IndPredBelow's .below is itself a mutual inductive whose parameters are the parent params followed by the parent motives — in Lean's source member order. The canonical below family is generated from the canonical parent rec, so when sort_consts orders the members differently from source (the BelowPredicate EvenP/OddP fixture flipped to (OddP, EvenP) under the v4.33 content hashes), the canonical below's motive-parameter order diverges from Lean's authored one. .below HEAD applications in user constants were already reconciled by below_call_site_plans, and .brecOn by its derived plans — but a Prop-below family exposes two more user-referencable surfaces with the same leading params+motives telescope: the .below CONSTRUCTORS and the regenerated .below.casesOn wrapper. Matchers compiled by structural recursion over the predicates reference both (the BelowPredicate match_2 matchers apply OddP.below.succ / EvenP.below.zero and OddP.below.casesOn with source-order motives), so the kernel rejected them with AppTypeMismatch — 2 failures in kernel-check-env. Register the same derived plan under each below ctor name and the .below.casesOn name (Prop families only — Type-level .below is a definition with neither). The apply site discriminates the two telescope shapes by the key's last component (below/below_N = head, which keeps its indices+major application floor; anything else = family member, with NO floor, since a field-less below ctor like EvenP.below.zero is fully applied at exactly params+motives). In both shapes everything after the motive segment is kept in place, so the below branch now emits one identity tail — byte-identical entries to the old fixed/extra split for heads. X.below.rec is deliberately not registered: only regenerated wrappers reference it, and those skip surgery via the aux-regen guard. Mirrored in lockstep across the Rust and pure-Lean compilers (apply, compile-side registration, decompile-side plan install — the latter derives the ctor names from the parent inductive via the same suffix transplant buildBelowIndcCtor uses, since the below inductive is not yet regenerated at install time). CallSite metadata makes the rewrite self-describing, so decompile restores the source-order spelling with no changes; aux-gen-diff and decompile-diff gates stay byte-identical and validate-aux is clean. * test: pin BelowPredicate matchers; add kernel-roundtrip-ns diagnostic focusConsts gains the two _private BelowPredicate match_2 matchers — the constants that pinned the Prop-below ctor/casesOn call-site gap — so kernel-check-const reproduces that class of regression in ~10s without a full-env pass. Tests/Main.lean gains a kernel-roundtrip-ns=<prefixes> special arg mirroring rust-compile: the same compile → ingress → egress → decompile → hash-compare pipeline as kernel-ixon-roundtrip, but over the transitive closure of the name-prefix-matched constants only. kernel-roundtrip-ns=Nat.le reproduced the below.casesOn binder-name regression on a 98-constant closure in 40ms. * style: rustfmt One over-split method chain in install_decompile_call_site_plans from the below-family plan registration; whitespace-only. * ci: portable codegen for the GitHub-hosted rust-test job Since #575 stopped exporting RUSTFLAGS, .cargo/config.toml's -Ctarget-cpu=native is authoritative in CI. That is the point for the warp jobs (bench artifact reuse, with CPU provenance logged), but rust-test runs on ubuntu-latest — a heterogeneous fleet sharing one cargo cache. A proc-macro dylib or test binary compiled native on an AVX-512 runner SIGILLs when a later run lands on a non-AVX-512 one; clippy-driver died with SIGILL checking aiur off a cached tracing-attributes exactly this way, and nextest --run-ignored all executes release test binaries with the same exposure. Pin the job to -Ctarget-cpu=x86-64-v3 (AVX2 — the baseline every GitHub-hosted x64 runner provides). RUSTFLAGS participates in the rust-cache key, so this also re-keys away from the poisoned native-built cache entries.
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
3 participants
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.
rustflagsin CI, respecting.cargo/config.tomland thus ensuring AVX-512 codegen on supported machinesfreshargumentixbinaries and.ixeenvironments whenfreshis passed to!benchmark, so a toolchain bump PR can correctly measure across versions