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
File renamed without changes.
File renamed without changes.
4 changes: 2 additions & 2 deletions .github/workflows/dogfood-gate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ jobs:

- name: Validate A2ML manifests
if: steps.detect.outputs.count > 0
run: bash .githooks/validate-a2ml.sh
run: bash .github/hooks/validate-a2ml.sh
- name: Write summary
run: |
A2ML_COUNT="${{ steps.detect.outputs.count }}"
Expand Down Expand Up @@ -86,7 +86,7 @@ jobs:

- name: Validate K9 contracts
if: steps.detect.outputs.k9_count > 0
run: bash .githooks/validate-k9.sh
run: bash .github/hooks/validate-k9.sh
- name: Write summary
run: |
K9_COUNT="${{ steps.detect.outputs.k9_count }}"
Expand Down
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/
6 changes: 3 additions & 3 deletions .machine_readable/root-allow.txt
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,11 @@ CONTRIBUTING.md # REQUIRED AT ROOT by scorecard-enforcer/openssf-comp
SECURITY.md # REQUIRED AT ROOT by scorecard-enforcer CI + the security-policy contractile (test -f SECURITY.md). See CONTRIBUTING.md note re: the .github/ copy.
LICENSE
LICENSES/ # REUSE licence texts (MPL-2.0.txt + CC-BY-SA-4.0.txt) for the dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0)
CHANGELOG.md
CHANGELOG.adoc # AsciiDoc is the estate-standard documentation format

# ─── 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 All @@ -40,7 +39,8 @@ abi.ipkg # Idris2 package for the ABI seam; sourcedir=src/inte
# ─── Directories ─────────────────────────────────────────────────────────────
.devcontainer/ # VS Code dev container spec; tool-required at root
.git/
.github/ # CONTRIBUTING.md, CODE_OF_CONDUCT.md, SECURITY.md, workflows/
.github/ # CONTRIBUTING.md, CODE_OF_CONDUCT.md, SECURITY.md, workflows/, hooks/
www/ # site-operations bundle; canonical .well-known/ lives at www/.well-known/ (issue #53)
.machine_readable/ # AI manifests, contractiles, custom-format configs
.well-known/
build/ # contractile.just, setup.sh, flake.{nix,lock}, guix.scm, .guix-channel, Containerfile
Expand Down
12 changes: 6 additions & 6 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 @@ -123,20 +123,20 @@ 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 without running the test suite
test-smoke:
@echo "Smoke test..."
idris2 --typecheck abi.ipkg
idris2 --typecheck src/interface/abi.ipkg
cd src/interface/ffi && zig build

# Run end-to-end tests (full pipeline: build → run → verify)
Expand Down Expand Up @@ -204,7 +204,7 @@ fmt-check:
# build are where real warnings/errors from either toolchain surface.
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/onboarding/QUICKSTART-DEV.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -40,15 +40,15 @@ just setup-dev

[source,bash]
----
idris2 --build abi.ipkg
idris2 --build src/interface/abi.ipkg
cd src/interface/ffi && zig build
----

== Test

[source,bash]
----
idris2 --typecheck abi.ipkg
idris2 --typecheck src/interface/abi.ipkg
cd src/interface/ffi && zig build test --summary all
----

Expand Down
2 changes: 1 addition & 1 deletion docs/onboarding/QUICKSTART-MAINTAINER.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ the honest current state.

== Build-Time Dependencies

* Idris2 0.7.0+ (typed ABI seam, `abi.ipkg`)
* Idris2 0.7.0+ (typed ABI seam, `src/interface/abi.ipkg`)
* Zig 0.16+ (FFI implementation, `src/interface/ffi/`)
* `just` (task runner)

Expand Down
2 changes: 1 addition & 1 deletion docs/onboarding/QUICKSTART-USER.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ cd scaffoldia
just build
----

This builds the typed ABI (Idris2, `abi.ipkg`) and the FFI implementation
This builds the typed ABI (Idris2, `src/interface/abi.ipkg`) and the FFI implementation
(Zig, `src/interface/ffi/`) into a static library. There is no interactive
application to run yet.

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 @@ -18,7 +18,7 @@ section instead describes the test infrastructure scaffoldia actually has.
| *Source modules* | 6 | 3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI (build.zig, main.zig), 1 Zig integration test module
| *Unit tests* | 3 | Inline `test` blocks in `src/interface/ffi/src/main.zig` (lifecycle, error handling, version)
| *Integration tests* | 10 | `src/interface/ffi/test/integration_test.zig` — real tests against the exported FFI (lifecycle, operations, strings, version, build_info, error handling)
| *E2E tests* | 1 | `tests/e2e.sh` — real preflight + `idris2 --build abi.ipkg` + `zig build`/`zig build test`
| *E2E tests* | 1 | `tests/e2e.sh` — real preflight + `idris2 --build src/interface/abi.ipkg` + `zig build`/`zig build test`
| *Aspect tests* | 1 | `tests/aspect_tests.sh` — SPDX header coverage + dangerous-pattern grep (real, pre-existing, unchanged by the cure)
| *Workflow tests* | 1 | `tests/workflows/validate_workflows_test.sh` (unchanged by the cure)
| *Benchmarks* | 3 | `benches/template_bench.sh` — Zig build, Zig tests, workflow validation
Expand All @@ -29,7 +29,7 @@ section instead describes the test infrastructure scaffoldia actually has.
* `zig fmt --check .` — exit 0
* `cd src/interface/ffi && zig build` — exit 0
* `cd src/interface/ffi && zig build test --summary all` — exit 0, **13/13 tests pass** (3 unit + 10 integration)
* `idris2 --build abi.ipkg` — exit 0 (2 pre-existing shadowing warnings in `Abi.Layout`, unrelated to this cure, out of scope)
* `idris2 --build src/interface/abi.ipkg` — exit 0 (2 pre-existing shadowing warnings in `Abi.Layout`, unrelated to this cure, out of scope)

== What Changed From the Template State

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 @@ -84,16 +84,16 @@ green " zig found: $(command -v zig)"
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"
if IDRIS_OUTPUT=$(idris2 --build abi.ipkg 2>&1); then
if IDRIS_OUTPUT=$(idris2 --build src/interface/abi.ipkg 2>&1); then
# A from-scratch build prints "N/M: Building ..." lines; an incremental
# no-op rebuild prints nothing at all — both are success (exit 0).
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 "$IDRIS_OUTPUT" | tail -20
FAIL=$((FAIL + 1))
fi
Expand Down
Loading