fix: repair the justfile's broken local gates + toolchain hygiene - #108
Merged
Conversation
Four justfile defects, all invisible to CI (which builds via the .ipkg):
- abi-check-hello / abi-gen-hello pointed at src/abi/packages/hello/
(lowercase); the real path is src/abi/Packages/Hello/. Rewritten
ipkg-level (idris2 --build from src/abi) since per-file --check is
additionally a module-name mismatch from repo root.
- pkg-build-hello mv'd into examples/packages/hello.zpkg/binaries/{arch}/
which never existed; now mkdir -p'd and gitignored.
- ffi-build-hello emitted libhello.so into lib/ — the OCaml SOURCE
directory; now emits to dist/ffi/.
- zig-ffi-check and validate-spec used Make-style $$f, which just passes
to bash verbatim: "$$f" expands to <PID>f, so the loops silently
no-oped — zig-ffi-check printed its ✓ having checked nothing.
Gates wired: ci now runs lint test zig-ffi-check guard-escape-hatches;
guard-escape-hatches ports the ci.yml escape-hatch grep byte-identical.
Toolchain: scripts/check-proofs.sh deleted (orphaned — nothing invoked
it; CI runs the same three steps inline; its install docs move to
docs/TOOLCHAIN.adoc). mise.toml deleted (estate boilerplate pinning
banned languages to "latest", no ocaml — .tool-versions is the pin and
mise reads it natively). .tool-versions gains zig 0.13.0 (the verified
FFI version; local 0.16 breaks on callconv(.C) — the known version-skew
trap).
Verified locally: just ci exit 0 (dune lint + 27 conformance tests +
4 zig ast-checks + no escape hatches), abi-check-hello builds all 8
ipkg modules, pkg-build-hello emits all three arch binaries.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 1 resolved / 1 findingsRepairs broken justfile recipes, toolchain hygiene, and local gate execution. Consider removing the unused generated/abi/hello directory created by the abi-gen-hello recipe.
✅ 1 resolved✅ Quality: abi-gen-hello creates unused generated/abi/hello dir
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 7 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
|
gitar-bot
Bot
dismissed
their stale review
August 3, 2026 18:54
✅ All code review findings resolved.
hyperpolymath
added a commit
that referenced
this pull request
Aug 4, 2026
…#111) Closes #68. Advances #63 (owner action below) and #79 (skeleton only; stays open). ## What - **CONTRIBUTING**: the `.md` was un-instantiated template rot — opened mid-code-fence, raw `{{MAIN_BRANCH}}` token, a repository tree with five nonexistent directories, ended mid-block. Real content rewritten into `CONTRIBUTING.adoc` (actual tree, `docs/TOOLCHAIN.adoc` + `.tool-versions` toolchain, proof-gate discipline); `.md` deleted; README link updated. - **GOVERNANCE / MAINTAINERS**: inverse situation — the `.adoc` twins are the rich repo-specific docs; the generic stubs (`GOVERNANCE.md`, bare `MAINTAINERS`) deleted. - **#79 skeleton**: `docs/learning-paths/README.adoc` seeds the end-user/developer/maintainer outline. ## Owner action — `.claude/CLAUDE.md` replacement (#63) The file is agent-edit-blocked (self-modification guardrail). Please replace its contents with the text below, which fixes: the six `.scm` references (now `.machine_readable/6a2/*.a2ml`), the phantom `guix.scm`/`deno.json` claims, and the foreign language-policy table (AffineScript/Deno/Tauri — a different project's stack). ```markdown ## Machine-Readable Artefacts Structured project metadata lives in `.machine_readable/6a2/` (A2ML format): - `STATE.a2ml` - Current project state and progress - `META.a2ml` - Architecture decisions and development practices - `ECOSYSTEM.a2ml` - Position in the ecosystem and related projects - `AGENTIC.a2ml` - AI agent interaction patterns - `NEUROSYM.a2ml` - Neurosymbolic integration config - `PLAYBOOK.a2ml` - Operational runbook - `0-AI-MANIFEST.a2ml` - Manifest Contractiles live in `.machine_readable/contractiles/`. --- # CLAUDE.md - AI Assistant Instructions ## This Repo's Stack (all pinned in .tool-versions) | Language/Tool | Use Case | |---------------|----------| | **OCaml 5.1.1 + dune** | The Oblíbený compiler (lib/, bin/, test/) | | **Idris2 0.7.0** | ABI proof layer (src/abi/, oblibeny-abi.ipkg) | | **Zig 0.13** | Crypto FFI + obli-pkg (ffi/zig/); 0.14+ breaks callconv(.C) | | **just** | Task runner — all operations go through the justfile | | **Bash/POSIX shell** | Scripts, kept minimal | | **Guile Scheme** | Root spec files (ANCHOR*.scm, SPEC*.scm, AUTHORITY*.scm) | Do not introduce Node/npm/TypeScript/Python/Go — this repo has no JS/Python surface and the estate bans them as replacements-available. ## The Proof Gate (non-negotiable) - CI (`ci.yml`) builds the OCaml language, runs the conformance suite, type-checks (= proves) the Idris2 ABI layer, compile-checks the Zig FFI, and rejects soundness escape hatches (`believe_me`, `postulate`, `assert_total`, `partial`, `idris_crash`, holes) in `src/abi/Crypto.idr` and `src/abi/Packages`. - Local mirror: `just ci` + `just proofs`. Never weaken a proof to make a change pass. ## Packaging - Containers: `Containerfile.bootstrap` / `Containerfile.minimal` / `Containerfile.liboqs` (podman-first). - `flake.nix` is legacy (estate ruling: Guix-only; a `guix.scm` migration is an open follow-up). ## Security Requirements - No MD5/SHA1 for security (use SHA256+) - HTTPS only (no HTTP URLs) - No hardcoded secrets - SHA-pinned dependencies (actions included) - SPDX license headers on all files ``` Suggested follow-up issue rather than folding in here: *"packaging: replace flake.nix with guix.scm"* (Nix-retired estate ruling). **Note**: `CONTRIBUTING.adoc` links `docs/TOOLCHAIN.adoc`, which lands in PR #108 — merge that first (they're ordered #108 → #109 → #110 → this). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 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.
What
Four justfile defects — all invisible to CI because CI builds via the
.ipkg, not these recipes:abi-check-hello/abi-gen-hello):src/abi/packages/hello/→ real pathsrc/abi/Packages/Hello/. Fixing the path exposed a second layer: per-fileidris2 --checkfrom repo root fails on module-name mismatch, soabi-check-hellois now ipkg-level (cd src/abi && idris2 --build oblibeny-abi.ipkg) — also the honest form, since per-file--checkis a known fake-gate pattern.pkg-build-hellomv'd intobinaries/{x86_64,aarch64,riscv64}/which never existed → recipe aborted on firstmv. Nowmkdir -p'd and gitignored.ffi-build-helloemittedlibhello.sointolib/— the OCaml source directory. Now emits todist/ffi/.zig-ffi-checkandvalidate-specused Make-style$$f;justpasses$verbatim to bash, so"$$f"expanded to<PID>fand the loops silently no-oped —zig-ffi-checkprinted its ✓ having checked nothing.Gates wired:
just cinow runslint test zig-ffi-check guard-escape-hatches(the last porting the ci.yml escape-hatch grep byte-identical, so local mirrors CI).Toolchain hygiene: deleted orphaned
scripts/check-proofs.sh(nothing invoked it; CI runs the same steps inline; its install docs now live indocs/TOOLCHAIN.adoc) andmise.toml(boilerplate pinning banned languages tolatest, no ocaml entry —.tool-versionsis the pin, mise reads it natively)..tool-versionsgainszig 0.13.0(verified FFI version; 0.14+ renamedcallconv(.C)→.c, so unpinned local zig breaks the FFI build).Verified locally
just ci→ exit 0: dune lint + 27 conformance tests + 4 zig ast-checks + escape-hatch guardjust abi-check-hello→ all 8 ipkg modules build (proofs pass)just pkg-build-hello→ all three arch binaries emitted (bug 2 proven fixed)just validate-spec→ now prints the three ✓ lines it silently skipped before (bug 4 proven fixed)🤖 Generated with Claude Code