|
| 1 | +== Changelog |
| 2 | + |
| 3 | +All notable changes to `+absolute-zero+` will be documented in this |
| 4 | +file. |
| 5 | + |
| 6 | +This file is generated from conventional commits by the |
| 7 | +https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`+changelog-reusable.yml+`] |
| 8 | +workflow (`+hyperpolymath/standards#206+`). Adopt the workflow in this |
| 9 | +repo’s CI to keep this file in sync automatically — see |
| 10 | +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+templates/cliff.toml+`] |
| 11 | +for the canonical config. |
| 12 | + |
| 13 | +The format follows https://keepachangelog.com/en/1.1.0/[Keep a |
| 14 | +Changelog]; this project aims to follow |
| 15 | +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. |
| 16 | + |
| 17 | +=== [Unreleased] |
| 18 | + |
| 19 | +==== Added |
| 20 | + |
| 21 | +* feat(proofs): complete CNO + OND pillars, verified across six provers |
| 22 | +(#100) — OND pillar authored (OND-1..5, zero axioms) in |
| 23 | +Coq/Lean/Agda/Z3; single gate `+proofs/verify-all-provers.sh+` → |
| 24 | +`+ALL-PROVERS-GREEN+`; Isabelle CNO repaired + OND added; Mizar |
| 25 | +`+CNO.miz+` rewritten and verifying; Idris ABI builds |
| 26 | +* feat(ci): add `+.github/workflows/proofs.yml+` (Coq + Z3 proof |
| 27 | +verification) |
| 28 | +* feat(absolute-zero): complete loadStore_preserves_memory proof — no |
| 29 | +sorry |
| 30 | + |
| 31 | +==== Fixed |
| 32 | + |
| 33 | +* fix(proofs): remove/correct three latent-unsound Coq axioms |
| 34 | +(`+no_cloning+`, `+Cconj_Cexp+`, `+eta_equivalence+`); discharge CNO |
| 35 | +axiom base 98 → small classified remainder (#100) |
| 36 | +* fix(abi): repair Idris packaging + 6 latent type errors — ABI builds |
| 37 | +clean (#100) |
| 38 | +* fix(baseline): repair main + estate-policy sweep (unblocks #41) (#42) |
| 39 | +* fix(governance): enumerate banned-language demos in .hypatia-ignore |
| 40 | +(#44) |
| 41 | +* fix(coq/cno): drop cno_decidable axiom (Rice’s theorem territory) |
| 42 | +(#36) |
| 43 | +* fix(licence): canonicalise to PMPL-1.0-or-later per authorship check |
| 44 | +(#133) (#34) |
| 45 | +* fix(lean4/cno): finish loadStore_preserves_memory cons-case build |
| 46 | +(#28) |
| 47 | +* fix(lean4/cno): finish loadStore_preserves_memory cons-case build |
| 48 | +(#23) |
| 49 | +* fix(licence): canonicalise to PMPL-1.0-or-later per authorship check |
| 50 | +(#133) (#22) |
| 51 | +* fix(licence): clear scaffold-placeholder leak (isolated; dirty repo) |
| 52 | +(#20) |
| 53 | +* fix(ci): sync hypatia-scan.yml to canonical (413: |
| 54 | +env.HOME+Phase-2+SARIF) (#18) |
| 55 | +* fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + |
| 56 | +Comment-step gate) (#16) |
| 57 | + |
| 58 | +==== Documentation |
| 59 | + |
| 60 | +* docs: Phase 1 per-axiom triage of 72 Coq Axioms (#58) |
| 61 | +* docs: seed docs/proof-debt.md per trusted-base policy (#52) |
| 62 | +* docs: record tech-debt audit findings (2026-05-26) (#47) |
| 63 | + |
| 64 | +==== CI |
| 65 | + |
| 66 | +* ci(rust): convert rust-ci.yml to thin wrapper (standards#174 refile) |
| 67 | +(#53) |
| 68 | +* ci: bump actions/upload-artifact SHA to current v4 (#12) |
| 69 | +* ci(secret-scanner): drop duplicate –fail from trufflehog extra_args |
| 70 | +(#11) |
| 71 | +* ci: fix workflow-linter YAML parse error + self-flag bug |
| 72 | +* ci(antipattern): fix top-level dir matching + benchmarks/lsp/bench |
| 73 | +filename allowlists (#9) |
| 74 | + |
| 75 | +=== Pre-history |
| 76 | + |
| 77 | +Prior commits to this file’s introduction are recorded in git history |
| 78 | +but not formally classified into Keep-a-Changelog sections. To backfill, |
| 79 | +run `+git cliff -o CHANGELOG.md+` locally using the canonical |
| 80 | +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+cliff.toml+`] |
| 81 | +— this is one-shot mechanical work. |
| 82 | + |
| 83 | +''''' |
0 commit comments