Repository navigation
t27o --check: t27b test judges first, t27c test-report only when t27b cannot (Closes #10525) - #10538
Merged
Merged
Conversation
… cannot (Closes #10525) On rust_std.t27 the two runners gave the same 10/10 verdict in 0.89 s (t27b) and 94 s (t27c test-report, through Zig). ledger.t27 now maps t27b's exit codes (cli/t27b/README.md) to the oracle outcomes it already defines: 0 pass and 1 fail are verdicts; 2 unsupported and 5 codegen limit are unsupported; 3 front end, 4 JIT/interpreter disagreement and any code outside the table are unknown. needs_reference() says when t27c must run. Two tests, one a negative control; a mutant that returns pass for an unknown code fails both. t27b 12/12, test-report 12/12 with 0 vacuous. cmd_t27o glue: 9 lines (mod line, the t27b run, the fallback message, the --check doc). gen/rust/tools/t27o/ledger.rs is gen-rust of the spec. Checked by hand: bitmask.rs --check now prints "t27b test exited 2 (unsupported), so t27c test-report judges instead"; the defects that run exposed are #10534. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
This was referenced Oct 18, 2026
gHashTag
disabled auto-merge
October 18, 2026 17:38
…10525) own-language (check_budget) fails a diff whose counted hand-written foreign lines gain more than they lose. The t27b-first judge in cmd_t27o is now 3 lines instead of 6, and the diff deletes cclk_variant_and_xadc_envelope_check from cli/tri/src/fpga.rs: no caller and no test in the tree (its unit tests were already gone); the Lean theorem it mirrored stays in proofs/lean4/Trinity/TernaryFPGABoot.lean. Behaviour of --check is unchanged; cargo check -p tri is clean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
October 18, 2026 17:39
gHashTag
pushed a commit
that referenced
this pull request
Oct 18, 2026
… the scratchpad (Closes #10541) #10538 failed the required own-language check with +9/-0 hand lines in cli/tri/src/main.rs: check_budget refuses a diff whose counted foreign lines gain more than they lose, on top of the 40/80 cap. tri-pipeline says so under PRs; the t27o skill adds the numstat one-liner. The scratchpad was wiped on a session resume (worktrees, cargo target, measurements); $TMPDIR survived, so loop worktrees live there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 18, 2026
Contributor
PR DashboardGenerated at: 2026-10-18 18:29:48 UTC
Summary
Seal Status
|
gHashTag
added a commit
that referenced
this pull request
Oct 18, 2026
…e) and a t27o skill (Closes #10541) (#10542) * skills: tri-pipeline fast path (t27b first, frontier --only seal reuse) and a t27o skill (Closes #10541) tri-pipeline: t27b test for the inner loop (rust_std.t27 0.89 s against 94 s for t27c test-report), t27c frontier --only for unchanged specs (REUSE = the sealed verdict stands; 5 specs in about 5 s), test-report once as the final gate, symlinked release binaries instead of rebuilds, t27b exit codes, the sandbox ZIG cache trap, git add -f for gen files; drop the stale "tri test does not yet fail on vacuous" (#10507 landed). t27o: where its truth lives, making a refusal class convertible and measuring it, --check, the loop tick for #10522, tonight's traps. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * skills: the net-zero hand-line rule of own-language, and $TMPDIR over the scratchpad (Closes #10541) #10538 failed the required own-language check with +9/-0 hand lines in cli/tri/src/main.rs: check_budget refuses a diff whose counted foreign lines gain more than they lose, on top of the 40/80 cap. tri-pipeline says so under PRs; the t27o skill adds the numstat one-liner. The scratchpad was wiped on a session resume (worktrees, cargo target, measurements); $TMPDIR survived, so loop worktrees live there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude <claude@anthropic.com> Co-authored-by: Claude Opus 5.5 <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
2 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.
Closes #10525. Part of #10522 (t27o overnight loop, linked to #10486 M2).
What
tri t27o <file.rs> --checknow judges the converted spec witht27b test(the native JIT) and runst27c test-reportonly when t27b's exit code is not a verdict.t27c test-reportt27b test(bench Mac, 2026-10-18, under load from two loops.)
Where the rule lives
specs/tools/t27o/ledger.t27, beside the oracle outcomes it already defines:T27B_PASS..T27B_CODEGEN_LIMIT: the exit codes ofcli/t27b/README.md.t27b_outcome(code): 0 -> pass, 1 -> fail, 2 and 5 -> unsupported, 3, 4 and anything else (usage, I/O, a signal) -> unknown. Never a pass.needs_reference(outcome): true unless pass or fail.gen/rust/tools/t27o/ledger.rsist27c gen-rustof the spec (first time ledger.t27 is wired intotri); seal re-saved,--verifyMATCH.Glue
cli/tri/src/main.rs: 9 added lines -- the#[path]mod, thet27b testrun, the fallback with a message naming the code, and a doc line on--check. No other change tocmd_t27o; the SPICE dispatch of #10509 is untouched (different hunks).Evidence
t27b test specs/tools/t27o/ledger.t27: 12 passed, 0 failed.t27c test-report specs/tools/t27o/ledger.t27: 12/12,vacuous passes 0 of 12.only_t27b_pass_and_fail_are_verdicts_every_other_code_falls_back_to_t27c,negative_control_a_code_outside_t27b_table_is_unknown_never_a_pass).cargo build --release -p tri: ok.tri t27o bootstrap/src/host/bitmask.rs --checkprintst27o: target/release/t27b test exited 2 (unsupported), so t27c test-report judges instead. The converter defects that run exposed (integer!written as boolean not, a missingusefor the oracle tests, a harness that keepsno_std) are filed as [bug] t27o: integer ! miscompiled as boolean not; oracle tests miss the type_text use; the oracle harness keeps #![no_std] #10534; they are not in this PR.🤖 Generated with Claude Code