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
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,6 @@ dist/
!/build/
!/build/**

# ...but never track Idris2 typecheck output. `idris2 --typecheck abi.ipkg`
# ...but never track Idris2 typecheck output. `idris2 --typecheck src/interface/abi.ipkg`
# writes compiled .ttc/.ttm under build/ttc/; these are generated artifacts.
/build/ttc/
1 change: 0 additions & 1 deletion .machine_readable/root-allow.txt
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ CHANGELOG.adoc # Current changelog after the AsciiDoc migration.
# ─── Build entry points (must live at root for their tooling) ────────────────
Justfile # delegates phases to build/just/*.just
coordination.k9 # repo-local session binding (template-mandated)
abi.ipkg # Idris2 package for the ABI seam; sourcedir=src/interface (estate canon: root-level *-abi.ipkg). Single case-consistent src/interface/Abi/ dir. Typecheck: `idris2 --typecheck abi.ipkg`.

# ─── Conventional dotfiles (tool-required at root) ───────────────────────────
.editorconfig
Expand Down
10 changes: 5 additions & 5 deletions Justfile
Original file line number Diff line number Diff line change
Expand Up @@ -83,14 +83,14 @@ import? "build/just/assess.just"
# Build the project (debug mode)
build *args:
@echo "Building {{project}} (debug)..."
idris2 --build abi.ipkg
idris2 --build src/interface/abi.ipkg
cd src/interface/ffi && zig build {{args}}
@echo "Build complete"

# Build in release mode with optimizations
build-release *args:
@echo "Building {{project}} (release)..."
idris2 --build abi.ipkg
idris2 --build src/interface/abi.ipkg
cd src/interface/ffi && zig build -Doptimize=ReleaseFast {{args}}
@echo "Release build complete"

Expand Down Expand Up @@ -118,14 +118,14 @@ clean-all: clean
# Run all tests
test *args:
@echo "Running tests..."
idris2 --typecheck abi.ipkg
idris2 --typecheck src/interface/abi.ipkg
cd src/interface/ffi && zig build test {{args}}
@echo "Tests passed!"

# Run tests with verbose output
test-verbose:
@echo "Running tests (verbose)..."
idris2 --typecheck abi.ipkg
idris2 --typecheck src/interface/abi.ipkg
cd src/interface/ffi && zig build test --summary all

# Smoke test — compiles but does not run
Expand Down Expand Up @@ -204,7 +204,7 @@ fmt-check:
# real warnings/errors on typecheck/build, so use those as the lint gate.
lint:
@echo "Linting source files..."
idris2 --typecheck abi.ipkg
idris2 --typecheck src/interface/abi.ipkg
cd src/interface/ffi && zig build

# ═══════════════════════════════════════════════════════════════════════════════
Expand Down
4 changes: 2 additions & 2 deletions docs/QUICKSTART.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ Get up and running in 60 seconds.
git clone https://github.com/hyperpolymath/panoply
cd panoply
just deps # verify idris2/zig/just are on PATH
just build # idris2 --build abi.ipkg + zig build
just test # idris2 --typecheck abi.ipkg + zig build test
just build # idris2 --build src/interface/abi.ipkg + zig build
just test # idris2 --typecheck src/interface/abi.ipkg + zig build test
----

== Project Structure
Expand Down
4 changes: 2 additions & 2 deletions docs/status/TEST-NEEDS.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Idris2 ABI / Zig FFI scaffold, not language semantics.
| *FFI modules* | 1 | `src/interface/ffi/src/main.zig` (11 exported functions)
| *Unit tests* | 3 | Inline `test` blocks in `main.zig` (lifecycle, error handling, version)
| *Integration tests* | 15 | `src/interface/ffi/test/integration_test.zig` — exercises every exported FFI function (lifecycle, process, process_array incl. null-buffer, strings, version/build_info, error handling, callbacks)
| *E2E tests* | 1 | `tests/e2e.sh` — preflight (idris2/zig on PATH) + `idris2 --build abi.ipkg` + `zig build test`
| *E2E tests* | 1 | `tests/e2e.sh` — preflight (idris2/zig on PATH) + `idris2 --build src/interface/abi.ipkg` + `zig build test`
| *Aspect tests* | 1 | `tests/aspect_tests.sh` — SPDX header coverage + dangerous-pattern scan (real gate; currently reports one known false positive on doc prose mentioning "Admitted"/"sorry")
| *Workflow tests* | 1 | `tests/workflows/validate_workflows_test.sh`
| *Benchmarks* | 3 | `benches/template_bench.sh` (Zig build, Zig tests, workflow validation)
Expand All @@ -27,7 +27,7 @@ Idris2 ABI / Zig FFI scaffold, not language semantics.
== Verified 2026-07-27

* `zig fmt --check .` — exit 0
* `idris2 --build abi.ipkg` — exit 0 (builds `Abi.Types`, `Abi.Layout`, `Abi.Foreign`)
* `idris2 --build src/interface/abi.ipkg` — exit 0 (builds `Abi.Types`, `Abi.Layout`, `Abi.Foreign`)
* `cd src/interface/ffi && zig build` — exit 0
* `zig build test --summary all` — exit 0, 20/20 tests pass (3 unit + 17 integration checks across 15 `test` blocks)
* `bash tests/e2e.sh` — PASS=2 FAIL=0
Expand Down
4 changes: 2 additions & 2 deletions abi.ipkg → src/interface/abi.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
-- A bare `idris2 --check src/interface/Abi/Foo.idr` still warns ("module name
-- does not match file name") because Idris derives the expected module from the
-- full path; that is expected. Use the package for a real typecheck:
-- idris2 --typecheck abi.ipkg (or --build)
-- idris2 --typecheck src/interface/abi.ipkg (or --build)
--
-- The RSR validators accept either Abi/ (canonical, case-consistent) or a
-- lowercase abi/ for downstream repos that ship lowercase — but never both.
Expand All @@ -27,7 +27,7 @@ authors = "Jonathan D.A. Jewell"

brief = "Formally-typed ABI/FFI seam (Idris2 type + layout proofs) for an RSR-templated repository"

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

depends = base

Expand Down
8 changes: 4 additions & 4 deletions tests/e2e.sh
Original file line number Diff line number Diff line change
Expand Up @@ -88,16 +88,16 @@ echo ""
# ═══════════════════════════════════════════════════════════════════════
# Section 1: Idris2 ABI build
# ═══════════════════════════════════════════════════════════════════════
bold "Section 1: Idris2 ABI (abi.ipkg)"
bold "Section 1: Idris2 ABI (src/interface/abi.ipkg)"

cd "$PROJECT_DIR"
ABI_OUTPUT=$(idris2 --build abi.ipkg 2>&1)
ABI_OUTPUT=$(idris2 --build src/interface/abi.ipkg 2>&1)
ABI_STATUS=$?
if [ "$ABI_STATUS" -eq 0 ]; then
green " PASS: idris2 --build abi.ipkg"
green " PASS: idris2 --build src/interface/abi.ipkg"
PASS=$((PASS + 1))
else
red " FAIL: idris2 --build abi.ipkg"
red " FAIL: idris2 --build src/interface/abi.ipkg"
echo "$ABI_OUTPUT" | tail -20
FAIL=$((FAIL + 1))
fi
Expand Down
Loading