chore: delete the two dead Zig trees; fix the configs that pointed at them - #7
Merged
Conversation
… them
`bridge/` is the only live Zig tree — it builds and emits
`zig-out/lib/liblith_bridge.a`, exactly what `lakefile.lean` links
(`-Lbridge/zig-out/lib -llith_bridge`).
The other two are removed. Both were measured against the pinned Zig 0.16.0
and neither compiles:
bridge/zig/ build.zig:14 error: no field or member function named
'addStaticLibrary' in 'Build'
ffi/zig/ src/main.zig:82 error: root source file struct 'heap' has no
member named 'GeneralPurposeAllocator'
Nothing linked against either. 1,383 lines of code that could not build.
Two LIVE configs were still pointing at them — this is the same fault already
fixed in CI, which had been building bridge/zig/ rather than bridge/:
* `Containerfile` — `WORKDIR /workspace/bridge/zig`, i.e. the container built
the tree that cannot compile. Also had the build order inverted: `lake build`
ran BEFORE the Zig bridge, but the Lean link needs liblith_bridge.a to exist
already. Both steps were `|| echo "..."`, so a wholly broken build still
produced a "successful" image — the same swallow-the-failure shape as the
gates removed in #6. Now: bridge first, asserting the archive exists, then
`lake build`, neither masked.
* `selur-compose.yml` — mounted the zig-cache volume at
`/workspace/bridge/zig/.zig-cache`, a path that no longer exists.
`ABI-FFI-README.md` was still the unfilled RSR template: 385 lines, 27
`{{project}}`/`{{PROJECT}}` placeholders, opening with "delete this line and
fill out the template below", and documenting `ffi/zig/src/main.zig` as the FFI
implementation — a file that did not compile. `README.adoc` linked to it as
though it were real documentation. Replaced with an accurate description of
what exists: the three Idris2 ABI files, the bridge layout, the build order and
the 17 exported C functions, plus the unweighted-mean caveat on
`computeOverall` carried over from docs/THEORY.adoc.
`.gitignore` gains secret hygiene (`.env`, `.env.*`, `*.key`, `*.pem`,
`secrets/`), `.claude/`, sqlite artifacts and editor droppings. These were
sitting uncommitted in the working tree; the generic multi-language entries
alongside them (Chapel, Elixir, Haskell, Julia) were dropped as irrelevant here.
Verified after the deletions: `cd bridge && zig build && zig build test` passes
and still emits liblith_bridge.a; the proof gate passes; `selur-compose.yml` and
`mise.toml` both still parse.
Remaining `ffi/zig` mentions in GQL-DT-COMPLETION-2026-02-07.md and
docs/M6-PARSER-STATUS.md are left alone: they are dated historical snapshots,
accurate as records of what was true when written.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Governance began returning `startup_failure` with ZERO jobs on this branch, despite `.github/` being byte-identical to main. Not caused by the Zig cleanup. Root cause, measured: standards@0ced540e "chore: estate-wide security compliance" (2026-07-26) added `actions: read` to governance-reusable.yml's own `permissions:` block. A called reusable workflow cannot request MORE permissions than its caller grants. This caller granted only `contents: read`, so GitHub rejected the run before any job started — which is why there are zero jobs and no check run to click into. This caller pins the reusable at `@main`, not a SHA, so the upstream change arrived the moment it landed. Timeline: gnpl Governance was green 2026-07-21, the reusable changed 2026-07-26T13:53Z, and the next gnpl run (today) failed. hyperpolymath/standards' own main is red for the same reason, so this is estate-wide rather than local — filed upstream. Fix is to mirror the permission. Unrelated to the rest of this PR, but it blocks every PR in the repo, so it is folded in here rather than queued. Co-Authored-By: Claude Opus 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
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.
Follow-up to #6, clearing the stale artefacts that PR flagged but deliberately left alone.
The two dead Zig trees are gone
bridge/is the only live tree — it builds and emitszig-out/lib/liblith_bridge.a,exactly what
lakefile.leanlinks (-Lbridge/zig-out/lib -llith_bridge).The other two were measured against the pinned Zig 0.16.0. Neither compiles:
Nothing linked against either. 1,383 lines of code that could not build.
Two live configs were still pointing at them
Same fault as the one already fixed in CI, which had been building
bridge/zig/:ContainerfileWORKDIR /workspace/bridge/zig— built the tree that cannot compilebridge/, asserting the archive existsselur-compose.yml/workspace/bridge/zig/.zig-cache/workspace/bridge/.zig-cacheThe Containerfile had a second, worse problem. Build order was inverted —
lake buildran before the Zig bridge, but the Lean link needs
liblith_bridge.ato already exist.Both steps were
|| echo "...", so a wholly broken build still produced a "successful"image. That is the same swallow-the-failure shape as the three gates removed in #6; this is
a fourth. Now the bridge builds first and neither step is masked.
ABI-FFI-README.mdwas the unfilled RSR template385 lines, 27
{{project}}/{{PROJECT}}placeholders, opening with "Aditionallydelete this line and fill out the template below", documenting
ffi/zig/src/main.zigasthe FFI implementation — a file that did not compile.
README.adoclinked to it as thoughit were real documentation.
Replaced with what the repo actually contains: the three Idris2 ABI files
(
Types/Layout/Foreign), thebridge/layout, the build order, and the 17 exported Cfunctions grouped by role — carrying forward the unweighted-mean caveat on
computeOverallso it is stated where FFI consumers will see it.
.gitignoreAdds secret hygiene (
.env,.env.*,*.key,*.pem,secrets/),.claude/, sqliteartifacts (the bridge links libsqlite3) and editor droppings. These were sitting
uncommitted in the working tree. The generic multi-language entries alongside them (Chapel,
Elixir, Haskell, Julia) were dropped as irrelevant rather than swept in.
Verified after deletion
cd bridge && zig build && zig build test— passes, still emitsliblith_bridge.ascripts/check-lean-proofs.sh— passesselur-compose.ymlandmise.tomlboth still parseDeliberately left
ffi/zigmentions inGQL-DT-COMPLETION-2026-02-07.mdanddocs/M6-PARSER-STATUS.mdaredated historical snapshots — accurate as records of what was true when written.
🤖 Generated with Claude Code