From 2e61a4445d36f03f375fa09c98976982a6a5400c Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 24 Jun 2026 17:21:33 +0100 Subject: [PATCH] chore(licence): normalise to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) - LICENSES/ = {MPL-2.0.txt, CC-BY-SA-4.0.txt}; root LICENSE = verbatim MPL-2.0 (GitHub display) - SPDX: code -> MPL-2.0, docs (.md/.adoc) -> CC-BY-SA-4.0; metadata/badge fixes; vendored untouched Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/copilot-instructions.md | 2 +- .github/workflows/scorecard.yml | 2 +- .github/workflows/secret-scanner.yml | 2 +- .machine_readable/licensing-policy.toml | 2 +- CHANGELOG.md | 2 +- CODE_OF_CONDUCT.md | 2 +- CONTRIBUTING.md | 2 +- LICENSE | 4 ++-- LICENSING.adoc | 4 ++-- SECURITY.md | 2 +- academic/formal-verification/agda/Phronesis.agda | 2 +- academic/formal-verification/agda/PhronesisEcho.agda | 2 +- academic/formal-verification/coq/Phronesis.v | 2 +- academic/formal-verification/lean4/Phronesis.lean | 2 +- academic/formal-verification/lean4/lakefile.lean | 2 +- 15 files changed, 17 insertions(+), 17 deletions(-) diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index 0e9129a..79fa46e 100644 --- a/.github/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -1,5 +1,5 @@ ## Code Review Guidelines diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 2552c7d..8ba6367 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# SPDX-License-Identifier: CC-BY-SA-4.0 +# SPDX-License-Identifier: MPL-2.0 name: Scorecards supply-chain security on: branch_protection_rule: diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 2b873b7..65310b6 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# SPDX-License-Identifier: CC-BY-SA-4.0 +# SPDX-License-Identifier: MPL-2.0 name: Secret Scanner on: pull_request: diff --git a/.machine_readable/licensing-policy.toml b/.machine_readable/licensing-policy.toml index f34fb98..1020974 100644 --- a/.machine_readable/licensing-policy.toml +++ b/.machine_readable/licensing-policy.toml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# SPDX-License-Identifier: CC-BY-SA-4.0 +# SPDX-License-Identifier: MPL-2.0 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) # # Machine-readable form of LICENSING.adoc. Tools enforce from this; humans read diff --git a/CHANGELOG.md b/CHANGELOG.md index f819f32..3557aef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,5 @@ # Changelog diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md index 5c80c98..bd4d0ab 100644 --- a/CODE_OF_CONDUCT.md +++ b/CODE_OF_CONDUCT.md @@ -1,5 +1,5 @@ # Code of Conduct diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 5696af9..a1bd8c8 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,5 +1,5 @@ # Contributing to Phronesis diff --git a/LICENSE b/LICENSE index d0a1fa1..14e2f77 100644 --- a/LICENSE +++ b/LICENSE @@ -35,7 +35,7 @@ Mozilla Public License Version 2.0 means any form of the work other than Source Code Form. 1.7. "Larger Work" - means a work that combines Covered Software with other material, in + means a work that combines Covered Software with other material, in a separate file or files, that is not Covered Software. 1.8. "License" @@ -357,7 +357,7 @@ Exhibit A - Source Code Form License Notice This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed with this - file, You can obtain one at https://mozilla.org/MPL/2.0/. + file, You can obtain one at http://mozilla.org/MPL/2.0/. If it is not possible or desirable to put the notice in a particular file, then You may include the notice in a location (such as a LICENSE diff --git a/LICENSING.adoc b/LICENSING.adoc index 2e91010..6140a94 100644 --- a/LICENSING.adoc +++ b/LICENSING.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Phronesis — Licensing @@ -20,7 +20,7 @@ syntax: [source] ---- -SPDX-License-Identifier: MPL-2.0 +SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-License-Identifier: CC-BY-SA-4.0 ---- diff --git a/SECURITY.md b/SECURITY.md index 698780d..7a8ff2d 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -1,5 +1,5 @@ # Security Policy diff --git a/academic/formal-verification/agda/Phronesis.agda b/academic/formal-verification/agda/Phronesis.agda index f0d04d6..f23123a 100644 --- a/academic/formal-verification/agda/Phronesis.agda +++ b/academic/formal-verification/agda/Phronesis.agda @@ -1,5 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 --- SPDX-License-Identifier: CC-BY-SA-4.0 +-- SPDX-License-Identifier: MPL-2.0 -- Phronesis Formalization in Agda -- Intrinsically typed representation with dependent types diff --git a/academic/formal-verification/agda/PhronesisEcho.agda b/academic/formal-verification/agda/PhronesisEcho.agda index 512f391..ac9286a 100644 --- a/academic/formal-verification/agda/PhronesisEcho.agda +++ b/academic/formal-verification/agda/PhronesisEcho.agda @@ -1,5 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 --- SPDX-License-Identifier: CC-BY-SA-4.0 +-- SPDX-License-Identifier: MPL-2.0 -- Copyright (c) 2026 Jonathan D.A. Jewell -- -- ===================================================================== diff --git a/academic/formal-verification/coq/Phronesis.v b/academic/formal-verification/coq/Phronesis.v index 4637aa3..d5078af 100644 --- a/academic/formal-verification/coq/Phronesis.v +++ b/academic/formal-verification/coq/Phronesis.v @@ -1,5 +1,5 @@ (* SPDX-License-Identifier: MPL-2.0 *) -(* SPDX-License-Identifier: CC-BY-SA-4.0 *) +(* SPDX-License-Identifier: MPL-2.0 *) (* Phronesis Formalization in Coq *) (* Complete mechanized proofs of type safety, termination, and security properties *) diff --git a/academic/formal-verification/lean4/Phronesis.lean b/academic/formal-verification/lean4/Phronesis.lean index 3835b5e..1fdc95d 100644 --- a/academic/formal-verification/lean4/Phronesis.lean +++ b/academic/formal-verification/lean4/Phronesis.lean @@ -1,5 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 --- SPDX-License-Identifier: CC-BY-SA-4.0 +-- SPDX-License-Identifier: MPL-2.0 -- Phronesis Formalization in Lean 4 -- Mechanized proofs of type safety, termination, and security properties. -- diff --git a/academic/formal-verification/lean4/lakefile.lean b/academic/formal-verification/lean4/lakefile.lean index 670b686..ac61c37 100644 --- a/academic/formal-verification/lean4/lakefile.lean +++ b/academic/formal-verification/lean4/lakefile.lean @@ -1,5 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 --- SPDX-License-Identifier: CC-BY-SA-4.0 +-- SPDX-License-Identifier: MPL-2.0 -- Minimal Lake build for the Phronesis Lean 4 metatheory. -- No external dependencies (no Mathlib): builds on core Lean only, so CI -- needs nothing but the toolchain pinned in `lean-toolchain`.