Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/workflows/idris2-abi.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ permissions:

jobs:
typecheck:
name: idris2 --typecheck abi.ipkg
name: idris2 --typecheck src/interface/abi.ipkg
runs-on: ubuntu-latest
timeout-minutes: 30
steps:
Expand All @@ -41,4 +41,4 @@ jobs:
- name: Typecheck the ABI
run: |
idris2 --version
idris2 --typecheck abi.ipkg
idris2 --typecheck src/interface/abi.ipkg
1 change: 1 addition & 0 deletions .machine_readable/root-allow.txt
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
CLAUDE.md
build/ # build orchestration: guix.scm relocated here (canon 1.2.1 guix-primary template_ref = "build/")
2 changes: 1 addition & 1 deletion HANDOFF.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ deno run --allow-read bin/evangeliser.js --kind false-friend # offline CLI
* *Required:* https://deno.land[Deno] (latest stable) — runs everything above.
* *Optional, now locally buildable* (these were "author-now / verify-in-CI" in
the cloud env because it could not fetch them; on a desktop you can actually
build/verify): *Idris2* (`idris2 --typecheck abi.ipkg`), *Zig* (the FFI mirror
build/verify): *Idris2* (`idris2 --typecheck src/interface/abi.ipkg`), *Zig* (the FFI mirror
under `src/interface/ffi/`).

== Next steps (pick up from ROADMAP M2/M4/M5)
Expand Down
2 changes: 1 addition & 1 deletion Justfile
Original file line number Diff line number Diff line change
Expand Up @@ -205,7 +205,7 @@ nix-shell:

# Guix build (if available)
guix-build:
@command -v guix >/dev/null && guix build -f guix.scm || echo "Guix not installed"
@command -v guix >/dev/null && guix build -f build/guix.scm || echo "Guix not installed"

# === HELP ===

Expand Down
2 changes: 1 addition & 1 deletion QUICKSTART-MAINTAINER.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ Output: `{{BUILD_OUTPUT_PATH}}`

[source,bash]
----
guix build -f guix.scm
guix build -f build/guix.scm
----

=== Nix
Expand Down
28 changes: 0 additions & 28 deletions guix.scm

This file was deleted.

4 changes: 2 additions & 2 deletions src/interface/Abi/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
= ABI seam — the correspondence model (Idris2)

The formally-typed core of the engine that *classifies* cross-language
correspondences. Typecheck with `idris2 --typecheck abi.ipkg` from the repo root.
correspondences. Typecheck with `idris2 --typecheck src/interface/abi.ipkg` from the repo root.

== Modules

Expand Down Expand Up @@ -34,7 +34,7 @@ The shapes are re-expressed here as fresh MPL-2.0 source rather than depended on

== Status

*Typechecks clean* under Idris2 0.8.0 (`idris2 --typecheck abi.ipkg`; `%default
*Typechecks clean* under Idris2 0.8.0 (`idris2 --typecheck src/interface/abi.ipkg`; `%default
total`, no escape hatches — verified 2026-06-18). The Zig FFI side of the seam
(`src/interface/ffi/`) and the AffineScript host binding that consumes this ABI
follow as later slices of the abstraction-model pivot.
4 changes: 2 additions & 2 deletions abi.ipkg → src/interface/abi.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
-- EVERY filesystem (Idris2 requires capitalised namespace components).
--
-- Typecheck with the package (not a bare --check, which warns on module/path):
-- idris2 --typecheck abi.ipkg (or --build)
-- idris2 --typecheck src/interface/abi.ipkg (or --build)

package abi

Expand All @@ -18,7 +18,7 @@ authors = "Jonathan D.A. Jewell"

brief = "Formally-typed ABI seam (Idris2): Concept/Form/Transition + the six CorrespondenceKinds, grounded in Dyadic + Echo"

sourcedir = "src/interface"
sourcedir = "."

depends = base

Expand Down
Loading