From 20d4216e16d0f4a4d10f26a113e72fe4aaf2eba6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 16:56:03 +0100 Subject: [PATCH] chore(idris2): add estate-standard SPDX headers to idris2/src/*.idr (#134) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All 14 Idris2 source files under `idris2/src/` were missing the SPDX-License-Identifier + copyright header that the rest of the repo (`src/formal/Ephapax/Formal/*.idr` etc.) uses. PMPL-1.0-or-later is already the repo licence (`LICENSE`) and the canonical SPDX template across the estate is the three-line `-- SPDX… / -- Copyright… / --` block, byte-identical to the existing `RegionLinear.idr`/`Qualifier.idr` headers. Pure mechanical change — only the three header lines are added; no existing line is modified, trailing newlines preserved. Idris2 ignores `--`-line comments before `module …`, so the build is unaffected. Baseline rot under `ephapax-parse-tests.ipkg` (`testLexPositions` / `parseWithBuf` undefined) is pre-existing on `origin/main` and not in scope for this PR. Refs hyperpolymath/standards#124 #134 Co-Authored-By: Claude Opus 4.7 (1M context) --- idris2/src/Ephapax/Affine/Emit.idr | 3 +++ idris2/src/Ephapax/Affine/Typecheck.idr | 3 +++ idris2/src/Ephapax/IR/AST.idr | 3 +++ idris2/src/Ephapax/IR/Decode.idr | 3 +++ idris2/src/Ephapax/IR/SExpr.idr | 3 +++ idris2/src/Ephapax/Parse/Lexer.idr | 3 +++ idris2/src/Ephapax/Parse/Parser.idr | 3 +++ idris2/src/Ephapax/Parse/Stream.idr | 3 +++ idris2/src/Ephapax/Parse/TestMain.idr | 3 +++ idris2/src/Ephapax/Parse/Tests.idr | 3 +++ idris2/src/Ephapax/Parse/Util.idr | 3 +++ idris2/src/Ephapax/Parse/ZigBuffer.idr | 3 +++ idris2/src/Ephapax/Proven.idr | 3 +++ idris2/src/Main.idr | 3 +++ 14 files changed, 42 insertions(+) diff --git a/idris2/src/Ephapax/Affine/Emit.idr b/idris2/src/Ephapax/Affine/Emit.idr index 93813809..a7c98651 100644 --- a/idris2/src/Ephapax/Affine/Emit.idr +++ b/idris2/src/Ephapax/Affine/Emit.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Affine.Emit import Ephapax.IR.Decode diff --git a/idris2/src/Ephapax/Affine/Typecheck.idr b/idris2/src/Ephapax/Affine/Typecheck.idr index 9630fa0b..c8002142 100644 --- a/idris2/src/Ephapax/Affine/Typecheck.idr +++ b/idris2/src/Ephapax/Affine/Typecheck.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Affine.Typecheck import Data.List diff --git a/idris2/src/Ephapax/IR/AST.idr b/idris2/src/Ephapax/IR/AST.idr index 7d3dffad..5ba60832 100644 --- a/idris2/src/Ephapax/IR/AST.idr +++ b/idris2/src/Ephapax/IR/AST.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.IR.AST %default partial diff --git a/idris2/src/Ephapax/IR/Decode.idr b/idris2/src/Ephapax/IR/Decode.idr index 659da772..d9f63983 100644 --- a/idris2/src/Ephapax/IR/Decode.idr +++ b/idris2/src/Ephapax/IR/Decode.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.IR.Decode import Data.List diff --git a/idris2/src/Ephapax/IR/SExpr.idr b/idris2/src/Ephapax/IR/SExpr.idr index 395e40ef..bc34028c 100644 --- a/idris2/src/Ephapax/IR/SExpr.idr +++ b/idris2/src/Ephapax/IR/SExpr.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.IR.SExpr import Data.List diff --git a/idris2/src/Ephapax/Parse/Lexer.idr b/idris2/src/Ephapax/Parse/Lexer.idr index 438c4522..8644f63e 100644 --- a/idris2/src/Ephapax/Parse/Lexer.idr +++ b/idris2/src/Ephapax/Parse/Lexer.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.Lexer import Data.List diff --git a/idris2/src/Ephapax/Parse/Parser.idr b/idris2/src/Ephapax/Parse/Parser.idr index 6474197e..ea34c381 100644 --- a/idris2/src/Ephapax/Parse/Parser.idr +++ b/idris2/src/Ephapax/Parse/Parser.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.Parser import Data.List diff --git a/idris2/src/Ephapax/Parse/Stream.idr b/idris2/src/Ephapax/Parse/Stream.idr index f956d58d..ffd8b555 100644 --- a/idris2/src/Ephapax/Parse/Stream.idr +++ b/idris2/src/Ephapax/Parse/Stream.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.Stream import Ephapax.Parse.Lexer diff --git a/idris2/src/Ephapax/Parse/TestMain.idr b/idris2/src/Ephapax/Parse/TestMain.idr index 87dad2d3..bef7192d 100644 --- a/idris2/src/Ephapax/Parse/TestMain.idr +++ b/idris2/src/Ephapax/Parse/TestMain.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.TestMain import Ephapax.Parse.Tests diff --git a/idris2/src/Ephapax/Parse/Tests.idr b/idris2/src/Ephapax/Parse/Tests.idr index 02086fa2..01d5c822 100644 --- a/idris2/src/Ephapax/Parse/Tests.idr +++ b/idris2/src/Ephapax/Parse/Tests.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.Tests import Data.List diff --git a/idris2/src/Ephapax/Parse/Util.idr b/idris2/src/Ephapax/Parse/Util.idr index b06088d7..f9a16d21 100644 --- a/idris2/src/Ephapax/Parse/Util.idr +++ b/idris2/src/Ephapax/Parse/Util.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.Util import Data.List diff --git a/idris2/src/Ephapax/Parse/ZigBuffer.idr b/idris2/src/Ephapax/Parse/ZigBuffer.idr index ef09d4a6..2386549b 100644 --- a/idris2/src/Ephapax/Parse/ZigBuffer.idr +++ b/idris2/src/Ephapax/Parse/ZigBuffer.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Parse.ZigBuffer import System diff --git a/idris2/src/Ephapax/Proven.idr b/idris2/src/Ephapax/Proven.idr index 5800b651..ca099184 100644 --- a/idris2/src/Ephapax/Proven.idr +++ b/idris2/src/Ephapax/Proven.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Ephapax.Proven import Proven.SafeString.Escape diff --git a/idris2/src/Main.idr b/idris2/src/Main.idr index 2063ba68..2f1c1d4f 100644 --- a/idris2/src/Main.idr +++ b/idris2/src/Main.idr @@ -1,3 +1,6 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- module Main import System