The bit-exactness gate cannot see the compiler it proves things about - #2182
Merged
Conversation
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
emit-bitexact-gate.yml proves this project's central claim -- one spec, four
targets, bit-exact. Its paths: filter listed 11 entries and bootstrap/** was not
among them, while all four backends live in one file:
bootstrap/src/compiler.rs gen_zig:3437 gen_verilog:6741
gen_c:10522 gen_rust:14382 (31,077 lines)
So a PR that rewrote the C emitter merged with the cross-target proof never
having run. Added bootstrap/** and cli/**.
Second half: green did not mean proved. verify_multitarget.py exits 0 when t27c,
cc or rustc is missing. The job builds t27c itself and the runner ships the other
two, so a skip in CI means the environment broke -- and exit 0 makes 'proved'
indistinguishable from 'never ran'. --require turns every skip into a failure and
is now what CI passes; the script stays tolerant without it, so a contributor
lacking rustc is not blocked. Verified both ways.
The path filter was checked with a negative control rather than by eye:
bootstrap/src/compiler.rs, cli/tri/src/main.rs and tools/verify_multitarget.py
match; docs/README.md does not. The first attempt at this edit silently failed on
an indentation mismatch and the control is what caught it.
Closes #2183
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
force-pushed
the
loop/t27-bitexact-gate
branch
from
August 18, 2026 12:05
0590092 to
6df8e5b
Compare
Contributor
PR DashboardGenerated at: 2026-08-18 12:05:44 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
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.
.github/workflows/emit-bitexact-gate.ymlproves the central claim of this project — one spec, four targets, bit-exact. Itspaths:filter lists 11 entries andbootstrap/**is not among them.All four backends live in one file:
bootstrap/src/compiler.rsgen_ziggen_veriloggen_cgen_rust31,077 lines — and a PR that rewrites the C emitter merges with the cross-target proof never having run.
Second half: green does not mean proved.
tools/verify_multitarget.py:21-23—skip()callssys.exit(0)whent27c,ccorrustcis missing. The workflow buildst27citself (cargo build --release -p t27c) and GitHub runners shipccandrustc, so a skip in CI means the environment broke — and exit 0 makes proved indistinguishable from never ran.Fix
bootstrap/**andcli/**topaths:--requireso a missing prerequisite fails in CI, while a contributor withoutrustcis still not blocked locallyRelated but distinct from #2176, which is about
trinot building at all.Closes #2183
🤖 Generated with Claude Code