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 @@ -42,7 +42,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 @@ -87,7 +87,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
3 changes: 1 addition & 2 deletions .machine_readable/root-allow.txt
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ CITATION.cff # citation metadata (surfaced at root by #96)
# ─── 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 Expand Up @@ -83,7 +82,7 @@ flake.guix
# these are this project's real top-level shape. Moving them would
# break every path that references them, to satisfy a map that was
# never written for it. Read from the estate-rules gate's own output.
.githooks/ # Top-level component directory of this project.
.github/hooks/ # Top-level component directory of this project.
GOVERNANCE.md # Project documentation.
MAINTAINERS # Project file that must remain at the repository root.
REQUIRES_INITIALISATION.md # Project documentation.
Expand Down
75 changes: 0 additions & 75 deletions CONTRIBUTING.adoc

This file was deleted.

4 changes: 2 additions & 2 deletions scripts/validate-template.sh
Original file line number Diff line number Diff line change
Expand Up @@ -305,8 +305,8 @@ fi
# path / import breakage that a bare per-file `idris2 --check` masks as a
# tolerated "module name does not match file name" warning.
if command -v idris2 &> /dev/null; then
if [ -f "$REPO_ROOT/abi.ipkg" ]; then
if (cd "$REPO_ROOT" && idris2 --typecheck abi.ipkg) > /dev/null 2>&1; then
if [ -f "$REPO_ROOT/src/interface/abi.ipkg" ]; then
if (cd "$REPO_ROOT" && idris2 --typecheck src/interface/abi.ipkg) > /dev/null 2>&1; then
log_pass "Idris2 ABI typechecks (abi.ipkg)"
else
log_error "Idris2 ABI does NOT typecheck (abi.ipkg)"
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
Loading