Skip to content

chore(licence): AGPL-3.0-or-later -> MPL-2.0 code, CC-BY-SA-4.0 docs … - #406

Merged
hyperpolymath merged 2 commits into
mainfrom
chore/licence-agpl-to-mpl
Oct 3, 2026
Merged

hyperpolymath merged 2 commits into
mainfrom
chore/licence-agpl-to-mpl

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

…(D262)

Owner ruling D262 re-rules ECHIDNA from the 2026-08 AGPL-3.0-or-later split to MPL-2.0 for code and the specification surface and CC-BY-SA-4.0 for documentation. echidna-playground/ was always MPL-2.0 and is untouched.

  • 727 SPDX headers AGPL-3.0-or-later -> MPL-2.0 and 4 -> CC-BY-SA-4.0 (base->head SPDX-set diff: no other transition); the prover and extractor header templates follow.
  • LICENSE is now the verbatim Mozilla MPL-2.0 text. NOTICE and .reuse/dep5 are rewritten for the new split; LICENSES/AGPL-3.0-or-later.txt is kept because ten .a2ml files and one training-data file still carry AGPL headers until their .deed conversion (separate PR).
  • Crate license fields (root, 5 crates, 3 interface crates) and build/guix.scm declare MPL-2.0.
  • docs/DEBT.adoc gains a current P0 section with an inverted check (no AGPL headers outside the documented interim set); the 2026-08-07 resolution is kept as history. README, CLAUDE.md, the wiki, site and humans.txt record the re-ruling; the PMPL-fallback comment in contractiles/_base.ncl is removed.

Claude-Session: https://claude.ai/code/session_01SJGZgoR9ArMgxKcqG7ChW8

Summary

Closes #

Type of change

  • 🐛 Bug fix (non-breaking change that fixes an issue)
  • ✨ New feature (non-breaking change that adds functionality)
  • 💥 Breaking change (would change existing behaviour)
  • 🕳️ Soundness fix (fixes a checker/proof false-negative)
  • 📖 Documentation
  • 🧹 Refactor / tech debt (behaviour-preserving)
  • ⚡ Performance
  • 🔧 Build / CI / tooling

How has this been verified?

Checklist

  • My commits are signed (git commit -S).
  • I ran the project's own checks/tests locally and they pass.
  • New files carry the correct SPDX-License-Identifier (code/config MPL-2.0,
    prose CC-BY-SA-4.0); I did not relicense existing files.
  • Docs are updated, and no public claim now overstates what the code does.
  • I have not introduced a soundness hole (or I have flagged where I might have).

Notes for reviewers

hyperpolymath and others added 2 commits October 2, 2026 00:32
…(D262)

Owner ruling D262 re-rules ECHIDNA from the 2026-08 AGPL-3.0-or-later
split to MPL-2.0 for code and the specification surface and CC-BY-SA-4.0
for documentation. echidna-playground/ was always MPL-2.0 and is untouched.

- 727 SPDX headers AGPL-3.0-or-later -> MPL-2.0 and 4 -> CC-BY-SA-4.0
  (base->head SPDX-set diff: no other transition); the prover and
  extractor header templates follow.
- LICENSE is now the verbatim Mozilla MPL-2.0 text. NOTICE and
  .reuse/dep5 are rewritten for the new split; LICENSES/AGPL-3.0-or-later.txt
  is kept because ten .a2ml files and one training-data file still carry
  AGPL headers until their .deed conversion (separate PR).
- Crate license fields (root, 5 crates, 3 interface crates) and
  build/guix.scm declare MPL-2.0.
- docs/DEBT.adoc gains a current P0 section with an inverted check (no
  AGPL headers outside the documented interim set); the 2026-08-07
  resolution is kept as history. README, CLAUDE.md, the wiki, site and
  humans.txt record the re-ruling; the PMPL-fallback comment in
  contractiles/_base.ncl is removed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01SJGZgoR9ArMgxKcqG7ChW8
@hyperpolymath
hyperpolymath merged commit b761b3a into main Oct 3, 2026
1 of 3 checks passed
@coderabbitai

coderabbitai Bot commented Oct 3, 2026

Copy link
Copy Markdown
Contributor

Important

Review skipped

Too many files!

This PR contains 286 files, which is 186 over the limit of 100.

To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch.

Upgrade to a paid plan to raise the limit.

This review couldn't start because sufficient usage credits or metered capacity aren't available. Add credits or update usage-based reviews in the billing tab, then retry.

⚙️ Run configuration
  • Configuration used: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: edf2faf8-af27-4d00-84c9-dcd9808307ae
📥 Commits

Reviewing files that changed from the base of the PR and between 985bb2e and 69f99dd.

⛔ Files ignored due to path filters (14)
  • generated/abi/echidna_boj.h is excluded by !**/generated/**
  • generated/abi/echidna_ffi.h is excluded by !**/generated/**
  • generated/abi/echidna_overlay.h is excluded by !**/generated/**
  • generated/abi/echidna_tentacles.h is excluded by !**/generated/**
  • generated/abi/echidna_typell.h is excluded by !**/generated/**
  • generated/alloyiser/run-analysis.sh is excluded by !**/generated/**
  • proofs/tptp/contradiction.p is excluded by !**/*.p
  • proofs/tptp/disjunction_elim.p is excluded by !**/*.p
  • proofs/tptp/double_negation.p is excluded by !**/*.p
  • proofs/tptp/group_left_identity.p is excluded by !**/*.p
  • proofs/tptp/modus_ponens.p is excluded by !**/*.p
  • proofs/tptp/socrates.p is excluded by !**/*.p
  • proofs/tptp/symmetry_eq.p is excluded by !**/*.p
  • proofs/tptp/transitivity.p is excluded by !**/*.p
📒 Files selected for processing (286)
  • .clusterfuzzlite/Containerfile
  • .clusterfuzzlite/Dockerfile
  • .clusterfuzzlite/build.sh
  • .clusterfuzzlite/project.yaml
  • .containerization/Containerfile
  • .containerization/Containerfile.full
  • .containerization/Containerfile.mcp
  • .containerization/Containerfile.wave3
  • .containerization/build.sh
  • .echidnabot.toml
  • .editorconfig
  • .gitattributes
  • .github/CODEOWNERS
  • .github/FUNDING.yml
  • .github/canonical-references/prover-counts.yml
  • .github/dependabot.yml
  • .github/hooks/validate-a2ml.sh
  • .github/hooks/validate-k9.sh
  • .github/workflows/agda-meta-checker.yml
  • .github/workflows/boj-build.yml
  • .github/workflows/bridge-gate.yml
  • .github/workflows/cargo-audit.yml
  • .github/workflows/cflite_batch.yml
  • .github/workflows/cflite_pr.yml
  • .github/workflows/chapel-ci.yml
  • .github/workflows/codeql.yml
  • .github/workflows/container-ci.yml
  • .github/workflows/dogfood-gate.yml
  • .github/workflows/dogfood-proofs-ci.yml
  • .github/workflows/formal-verification.yml
  • .github/workflows/generator-generic-ossf-slsa3-publish.yml
  • .github/workflows/ghcr-publish.yml
  • .github/workflows/governance.yml
  • .github/workflows/hypatia-scan.yml
  • .github/workflows/idris2-abi-ci.yml
  • .github/workflows/live-provers.yml
  • .github/workflows/mirror.yml
  • .github/workflows/mvp-smoke.yml
  • .github/workflows/pages.yml
  • .github/workflows/proof-safety.yml
  • .github/workflows/rust-ci.yml
  • .github/workflows/s4-loop.yml
  • .github/workflows/scorecard.yml
  • .github/workflows/secret-scanner.yml
  • .github/workflows/security-scan.yml
  • .github/workflows/server-boot-gate.yml
  • .github/workflows/spark-theatre-gate.yml
  • .github/workflows/verification-proofs-cron.yml
  • .github/workflows/workflow-linter.yml
  • .gitignore
  • .gitlab-ci.yml
  • .guix-channel
  • .machine_readable/contractiles/_base.ncl
  • .pre-commit-config.yaml
  • .reuse/dep5
  • CHANGELOG.adoc
  • CLAUDE.md
  • Cargo.toml
  • Containerfile
  • HOL-o-extension/activate.sh
  • HOL-o-extension/overlays/default.sml
  • HOL-o-extension/overlays/security.sml
  • HOL-o-extension/tactics/neurosymbolicTac.sml
  • HOL-o-extension/theories/echidnaTrustScript.sml
  • LICENSE
  • Mustfile
  • NOTICE
  • Project.toml
  • README.adoc
  • alloyiser.toml
  • benches/proof_benchmarks.rs
  • benches/routing_benchmarks.rs
  • build.rs
  • build/guix.scm
  • config/config.ncl
  • config/solver-manifest.toml
  • container/.gatekeeper.yaml
  • container/Containerfile
  • container/compose.toml
  • container/ct-build.sh
  • container/deploy.k9.ncl
  • container/entrypoint.sh
  • container/vordr.toml
  • contractile.just
  • crates/echidna-core-spark/Cargo.toml
  • crates/echidna-core-spark/rust-toolchain.toml
  • crates/echidna-core-spark/src/axiom_tracker.rs
  • crates/echidna-core-spark/src/lib.rs
  • crates/echidna-core-spark/src/pareto.rs
  • crates/echidna-core/Cargo.toml
  • crates/echidna-core/src/core.rs
  • crates/echidna-core/src/lib.rs
  • crates/echidna-core/src/types.rs
  • crates/echidna-mcp/Cargo.toml
  • crates/echidna-mcp/src/main.rs
  • crates/echidna-wire/Cargo.toml
  • crates/echidna-wire/build.rs
  • crates/echidna-wire/schemas/verisim_er.capnp
  • crates/echidna-wire/src/lib.rs
  • crates/typed_wasm/Cargo.toml
  • crates/typed_wasm/src/lib.rs
  • data/synonyms/_conceptnet_seed.toml
  • data/synonyms/_disciplines.toml
  • data/synonyms/_msc2020.toml
  • data/synonyms/_wordnet_math.toml
  • data/synonyms/acl2.toml
  • data/synonyms/agda.toml
  • data/synonyms/coq.toml
  • data/synonyms/dafny.toml
  • data/synonyms/fstar.toml
  • data/synonyms/hol4.toml
  • data/synonyms/hol_light.toml
  • data/synonyms/idris2.toml
  • data/synonyms/isabelle.toml
  • data/synonyms/isabelle_afp.toml
  • data/synonyms/lean4.toml
  • data/synonyms/metamath.toml
  • data/synonyms/mizar.toml
  • data/synonyms/why3.toml
  • deploy/hetzner/Caddyfile
  • deploy/hetzner/Containerfile.caddy
  • deploy/hetzner/caddy.container
  • deploy/hetzner/echidna.container
  • deploy/hetzner/echidna.network
  • deploy/hetzner/env.example
  • docs-site/config/policy.yml
  • docs-site/lib/echidna_docs/application.ex
  • docs-site/lib/echidna_docs/gateway_config.ex
  • docs-site/mix.exs
  • docs-site/src/api_explorer.ecl
  • docs-site/src/app.ecl
  • docs-site/src/routes.ecl
  • docs/DEBT.adoc
  • docs/PROVER_COUNT.adoc
  • docs/academic/arcvix-neurosymbolic-theorem-proving.bib
  • docs/academic/arcvix-neurosymbolic-theorem-proving.tex
  • docs/wiki/FAQ.md
  • docs/wiki/Home.md
  • eclexiaiser.toml
  • examples/aspect_tagging_demo.rs
  • ffi/zig/build.zig
  • ffi/zig/src/boj.zig
  • ffi/zig/src/capnp_bridge.zig
  • ffi/zig/src/main.zig
  • ffi/zig/src/overlay.zig
  • ffi/zig/src/provers/atp.zig
  • ffi/zig/src/provers/autoactive.zig
  • ffi/zig/src/provers/constraint.zig
  • ffi/zig/src/provers/declarative.zig
  • ffi/zig/src/provers/interactive.zig
  • ffi/zig/src/provers/smt.zig
  • ffi/zig/src/provers/vcl_ut.zig
  • ffi/zig/src/tentacles.zig
  • ffi/zig/src/typell.zig
  • ffi/zig/test/benchmark.zig
  • ffi/zig/test/core_native_test.zig
  • ffi/zig/test/integration_test.zig
  • ffi/zig/test/overlay_benchmark.zig
  • ffi/zig/test/overlay_integration_test.zig
  • ffi/zig/test/overlay_native_test.zig
  • fuzz/Cargo.toml
  • fuzz/fuzz_targets/fuzz_axiom_tracker.rs
  • fuzz/fuzz_targets/fuzz_input.rs
  • fuzz/fuzz_targets/fuzz_proof_state.rs
  • fuzz/fuzz_targets/fuzz_trust_pipeline.rs
  • guix-channel/echidna.scm
  • guix/echidna/packages.scm
  • hooks/pre-commit
  • hooks/pre-push
  • k9iser.toml
  • manifests/live-provers.scm
  • meta-checker/echidna-meta.agda-lib
  • meta-checker/src/Echidna/AxiomSafety.agda
  • meta-checker/src/Echidna/AxiomTrackerCompleteness.agda
  • meta-checker/src/Echidna/Dispatch.agda
  • meta-checker/src/Echidna/MetaChecker.agda
  • meta-checker/src/Echidna/Portfolio.agda
  • meta-checker/src/Echidna/TrustLevel.agda
  • metrics/MetricsSuite.jl
  • metrics/alignment_rate.jl
  • metrics/corpus_loader.jl
  • metrics/floor_progress.jl
  • metrics/heaps_beta.jl
  • metrics/msc_taxonomy_coverage.jl
  • metrics/oov_rate.jl
  • metrics/prover_floor.jl
  • metrics/run_all.jl
  • metrics/tactic_cluster_purity.jl
  • metrics/triangulation_rate.jl
  • metrics/verisim_sink.jl
  • metrics/zipf_s.jl
  • proofs/agda/AxiomMonotonicity.agda
  • proofs/agda/CertificateChain.agda
  • proofs/agda/DispatchOrdering.agda
  • proofs/agda/IdentityLaws.agda
  • proofs/agda/List.agda
  • proofs/agda/Nat.agda
  • proofs/agda/ParallelSoundness.agda
  • proofs/agda/PortfolioConsistency.agda
  • proofs/agda/ProofComposition.agda
  • proofs/agda/Propositional.agda
  • proofs/agda/SoundnessPreservation.agda
  • proofs/agda/TrustLattice.agda
  • proofs/agda/echidna-proofs.agda-lib
  • proofs/coq/algebra/GroupTheory.v
  • proofs/dimacs/graph_3color.cnf
  • proofs/dimacs/pigeonhole_3_2.cnf
  • proofs/dimacs/satisfiable_basic.cnf
  • proofs/dimacs/unsatisfiable_basic.cnf
  • proofs/dimacs/xor_chain.cnf
  • proofs/isabelle/ROOT
  • proofs/isabelle/algebra/GroupTheory.thy
  • proofs/lean/Basic.lean
  • proofs/lean/ECHIDNA.lean
  • proofs/lean/List.lean
  • proofs/lean/Nat.lean
  • proofs/lean/Propositional.lean
  • proofs/lean/algebra/GroupTheory.lean
  • proofs/metamath/broken.mm
  • proofs/metamath/tiny.mm
  • rustfmt.toml
  • schemas/echidna.capnp
  • scripts/a2ml_emit.jl
  • scripts/align_premises.jl
  • scripts/balance_corpus.jl
  • scripts/ban-npm.sh
  • scripts/collect-field-signal.sh
  • scripts/extract_abc.jl
  • scripts/extract_abella.jl
  • scripts/extract_acl2.jl
  • scripts/extract_acl2s.jl
  • scripts/extract_afp.jl
  • scripts/extract_agda.jl
  • scripts/extract_all.sh
  • scripts/extract_alloy.jl
  • scripts/extract_arend.jl
  • scripts/extract_athena.jl
  • scripts/extract_boogie.jl
  • scripts/extract_cameleer.jl
  • scripts/extract_cbmc.jl
  • scripts/extract_coqgym.jl
  • scripts/extract_dafny.jl
  • scripts/extract_dedukti.jl
  • scripts/extract_dreal.jl
  • scripts/extract_framac.jl
  • scripts/extract_fstar.jl
  • scripts/extract_hol4.jl
  • scripts/extract_hol_light.jl
  • scripts/extract_idris2.jl
  • scripts/extract_isabelle_tropical.jl
  • scripts/extract_isabelle_zf.jl
  • scripts/extract_key.jl
  • scripts/extract_lambda_prolog.jl
  • scripts/extract_lean3.jl
  • scripts/extract_mathcomp.jl
  • scripts/extract_mathlib4.jl
  • scripts/extract_matita.jl
  • scripts/extract_mercury.jl
  • scripts/extract_metamath.jl
  • scripts/extract_minizinc.jl
  • scripts/extract_mizar.jl
  • scripts/extract_naproche.jl
  • scripts/extract_nitpick.jl
  • scripts/extract_nunchaku.jl
  • scripts/extract_nusmv.jl
  • scripts/extract_opentheory.jl
  • scripts/extract_prism.jl
  • scripts/extract_proverif.jl
  • scripts/extract_pvs.jl
  • scripts/extract_sat_benchmarks.jl
  • scripts/extract_seahorn.jl
  • scripts/extract_smtlib.jl
  • scripts/extract_spin.jl
  • scripts/extract_tamarin.jl
  • scripts/extract_tlaps.jl
  • scripts/extract_tlc.jl
  • scripts/extract_tptp.jl
  • scripts/extract_typechecker_ecosystem.jl
  • scripts/extract_typed_wasm.jl
  • scripts/extract_uppaal.jl
  • scripts/extract_viper.jl
  • scripts/extract_why3.jl
  • scripts/extractor_save_common.jl
  • scripts/final_complete_merge.jl
  • scripts/final_normalization.jl
  • scripts/gen-provers-a2ml.sh

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

  • Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@hyperpolymath
hyperpolymath deleted the chore/licence-agpl-to-mpl branch October 3, 2026 10:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant