Skip to content

Commit 2c2df18

Browse files
hyperpolymathclaude
andcommitted
fix(idris): // -> -- on Owner header line (restores idris2 --build)
Line 2 of 8 Idris ABI/formal files (.ipkg + .idr) was `// Owner: ...` — `//` is not an Idris comment (Idris uses `--`), so `idris2 --build` died at tokenisation ("Can't recognise token") on both ephapax-abi.ipkg and ephapax-formal.ipkg. Delimiter-only change (`//` -> `--`); owner string and the line-1 `|||` SPDX doc-comment unchanged. Both ipkgs now build (exit 0): Region/Qualifier/RegionLinear and Types/Invariants/Foreign. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 818492f commit 2c2df18

8 files changed

Lines changed: 8 additions & 8 deletions

File tree

src/abi/Ephapax/ABI/Foreign.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
||| SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
||| Ephapax ABI: FFI Boundary Obligations
44
|||
55
||| The Zig/WASM-FFI side of the Ephapax ABI seam. The Rust pipeline

src/abi/Ephapax/ABI/Invariants.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
||| SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
||| Ephapax ABI: Correctness-Critical Invariants
44
|||
55
||| Type-level statements of the invariants the Ephapax compiler

src/abi/Ephapax/ABI/Types.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
||| SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
||| Ephapax ABI: Boundary Types
44
|||
55
||| Idris2 statements of the data types that the Ephapax Rust pipeline

src/abi/ephapax-abi.ipkg

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
-- SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
-- Build/typecheck package for the Ephapax Rust↔SPARK ABI seam.
44
--
55
-- The seam modules are namespaced `Ephapax.ABI.*`; Idris2 requires the

src/formal/Ephapax/Formal/Qualifier.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
-- SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
44
--
55
||| Binding Qualifiers for the Ephapax Dyadic Type System

src/formal/Ephapax/Formal/Region.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
-- SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
44
--
55
||| Region Type System for Ephapax

src/formal/Ephapax/Formal/RegionLinear.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
-- SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
44
--
55
||| Region-Linear Fusion: The Core of Ephapax Memory Safety

src/formal/ephapax-formal.ipkg

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
-- SPDX-License-Identifier: MPL-2.0
2-
// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2+
-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
-- Ephapax Formal Specification Package
44
--
55
-- Machine-checked proofs of the Ephapax type system properties,

0 commit comments

Comments
 (0)