chore: remove Guix/build scaffolding (complete the interrupted sweep)#13
Merged
Merged
Conversation
The build/ directory (contractile.just, guix.scm, .guix-channel, setup.sh, just/*.just section imports) was RSR template scaffolding, not systemet content. Its deletion was already staged uncommitted in two estate repos (systemet + anytype) as an interrupted sweep; this commit completes it here so nothing dangles: - Justfile: drop the 7 dead `import?` lines, their section headers, and the guix-shell/guix-build recipes; `automate update` now calls recipes that exist (validate-claude-md, validate-coapt) - .envrc: drop the guix-shell block - .gitignore: keep the !/build/ exemption (build/just/proofs.just returns with the proof-gate PR) but correct the comment - root-allow.txt: remove the build/ entry; fix the Justfile justification - PLAYBOOK.a2ml / CONTRIBUTING.md / container docs / install-tools.sh: update prose that described the retired layout `just proofs`/`just validate` gates return for real (prover-absent = FAIL) in the forthcoming proof-gate PR. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…tion ledger (#15) ## Summary The core spec deliverable of the completion sequence: `docs/theory/` goes from empty taxonomy scaffolding to the formal home of Equality Theory. - **One doc per layer/gate** (00-notation … 08-l4-effects-tea, 09-catalogue), each with an explicit status (`specified` / `sketched` / `OPEN`), derived strictly from the existing README/EXPLAINME prose — no silent theory extensions (the few design *expectations* are marked non-normative). - **`OBLIGATIONS.adoc`** — the single citable ledger **ET-1..ET-15** with statement, prose source, status, and mechanization slot. TEA erasure (**ET-14**) is headlined **OPEN — never cite as proven**. A prospective ET-16 (L0 lowering correctness) is flagged as ADR-needed and deliberately NOT numbered in. - **Honesty fix:** the README's L3 row claimed "specified" while zero L3 rules existed anywhere in the repo. It now says **sketched**; `06-l3-guarded-recursion.adoc` carries the honesty note plus a clearly-labelled *candidate* Nakano-style rule set awaiting an owner ADR. - README Status section links `docs/theory/` + the ledger; AffineScript linked where named. PR-3 of the sequence (after #11, #12, #13). The mechanization PR (Lean4 L1 conversion + L2 grade-algebra laws) targets the MECH-1/MECH-2 slots this ledger names. ## Verification - Nothing in this PR claims a proof; every status is specified/sketched/OPEN. - All ET statements carry their source section in README/EXPLAINME. - AsciiDoc only under docs/ (estate rule). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…IS-NOT enforced) (#16) ## Summary PR-4 of the completion sequence (after #11, #12, #13, #15). systemet's IS-NOT says no runnable code lives here — this PR makes the repo match: - **`src/` + `abi.ipkg` + ABI-FFI doc removed** (git history is the quarantine). `validate-template.sh` now *enforces their absence* — the ABI checks are inverted into IS-NOT checks, and it requires `docs/theory/OBLIGATIONS.adoc` instead. - **Generic proof stubs removed** (idris2 ABI/, lean4 `ApiTypes.lean` that never compiled, agda/coq/tlaplus placeholders). `verification/proofs/README.adoc` now specifies the MANIFEST-gated Lean4 layout the mechanization PR fills. - **`docs/status/` localized to systemet**: ROADMAP (M1–M4 real milestones), PROOF-NEEDS (tier **T1**; master list = the ET ledger by reference; ABI category retired), PROOF-STATUS (ET obligation rows + MECH-1/MECH-2 slots; honest **0% proven**), TEST-NEEDS (actual verifiable surfaces), READINESS (X→**E**, real scan values, pending owner countersign). - root-allow/gitignore/eclexiaiser references cleaned. AFFIRMATION anchor fields intentionally untouched — filled at signing time in the final anchor PR. ## Verification - `bash -n scripts/validate-template.sh` clean; Phase 4 requirements (docs/theory present, src/ absent) hold on post-#15 main. - `grep -rn "sorry|believe_me|Admitted|assert_total"` over proof files: none exist (prose lists only). - No workflow files touched. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…ECH-2 complete) with hard gates (#17) PR-5 of the completion sequence (#11 → #12 → #13 → #15 → #16 → this). ## What is proven (all under Lean 4.32.0, hermetic, no mathlib, no `sorry`, no user axioms) **MECH-2 — complete.** `Systemet.L2.GradeAlgebra` is the precise ET-4 statement: an ordered-semiring law set whose 16 fields *are* the proof obligations. Instances: `Affine` {0,1,ω}, tropical `Cost` (min/+, ∞ identity), the **generic theorem** that every bounded distributive lattice is a grade algebra (instantiated at `Level` = Low≤High), and the componentwise product `R × S` — ET-5's "same rules, different algebra", proven once. **MECH-1 — totality core + stability.** Intrinsically-kinded type-level STLC (Keller–Altenkirch toolkit); β-normal forms with left-nested spines; **hereditary substitution and the normalizer are total** by a `(kindSize, tag, size)` lexicographic measure — the Totality Gate (ET-1) discharged by construction. `DefEq` stated; stability `nf_emb : nf (embNf n) = n` proven. Soundness/completeness (`defEq_iff_nf`, `decDefEq`) are **OPEN**, stated in `Conversion.lean`'s docstring and PROOF-STATUS — never stubbed. ## Gates (wire-first; every one watched to fail before its green was trusted) | Gate | Verified failure mode | |---|---| | `check-proofs.sh lean4` — MANIFEST-driven, absent prover = FAIL, per-module + package build | broken proof → FAIL; prover off PATH → FAIL; unlisted file on disk → FAIL | | mandatory axiom audit (`Systemet/Audit.lean`, 12 `#print axioms`) pinned to the three-axiom trusted base | a smuggled `axiom cheat : False` **compiles green and still fails the gate**, named in output | | `scan-dangerous.sh` (comment-aware; incl. `axiom`/`admit`/`native_decide`) | fixed Lean block-comment stripping (`{- -}` → `/- -/`) — was false-positive-prone; canary-tested both directions | | `check-proof-status.sh` — PROOF-STATUS.adoc must match MANIFEST counts | doctored count → FAIL | CI (`proofs.yml`): sha-pinned `actions/checkout` + `actions/cache`, elan 4.2.3 from a checksum-verified release tarball, toolchain from the committed `lean-toolchain`, cache keyed on that pin. Note: the sha `9c091bb2…` used across this repo's workflows is actually **v7.0.0** (some existing comments mislabel it v6.0.1). ## Honesty ledger - ET-1 ✓ (for the mechanized calculus) · ET-4 ✓ · ET-5 ✓ · ET-2 partial (stability only) · ET-14 and everything else remain OPEN, listed in PROOF-STATUS. - Local run: 11/11 modules PASS, coverage clean, `lake build` clean, audit 12/12, drift gate PASS. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…h (PR-6, closes the sequence) (#21) Final PR of the completion sequence (#11 → #12 → #13 → #15 → #16 → #17 → this). - **STATE.a2ml** — completion 15→32 with per-phase justification comments; blockers echo #18/#19 + the anytype audit trail (anytype #13–#19, PR #20). - **AFFIRMATION.adoc** — anchor filled (main @ `a11c9877`, 2026-07-21T14:43Z, Lean 4.32.0/elan 4.2.3) in the same session that re-ran every check listed; every "affirmed-ran" row corresponds to a command actually executed. NOT-claims list keeps ET-2 closure, ET-6..9, ET-10..13, ET-14 explicitly open. - **Justfile** — `test`/`lint`/`fmt-check` were template echo-stubs (fake green). Now: `test` = proof gate + drift gate; `lint` = dangerous-construct scan, md-in-docs, root-shape, template validation; `fmt-check` honestly reports that nothing is checked. `check-no-vlang.sh` deferred to #19 (tracked, not silently skipped). `.machine_readable/root-allow.txt` updated for root entries landed by #14/#17. - **README** — badge `theory_(no_proofs_yet)` → `theory_(L2_proven, L1_core_proven, rest_OPEN)`; Status section states precisely what is machine-checked vs open. Verification (all run in this session at the anchor SHA): `./scripts/check-proofs.sh lean4` PASS (audit 12/12); `./scripts/scan-dangerous.sh` PASS; `./scripts/check-proof-status.sh` PASS; `./scripts/validate-template.sh` PASS (4 warnings); `just test && just quality` PASS end-to-end. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The entire
build/directory deletion was sitting uncommitted in the working copy (identically in anytype — an interrupted estate sweep). This PR commits it and completes the sweep so nothing dangles: Justfile imports,.envrcguix block,.gitignorecomment,root-allow.txt, PLAYBOOK/CONTRIBUTING/container prose,install-tools.sh.build/just/proofs.just(and a realjust proof-check-*gate that FAILS when the prover is absent) returns in the mechanization PR — the!/build/gitignore exemption is kept for that reason.PR-2 of the systemet spec-completion sequence (after #11, #12).
Verification
just --listparses clean after the import removals.grep -rn "build/just\|guix.scm"— remaining hits are only: workflows (untouched,guix-policy.ymlhandles absence gracefully and workflow edits need theworkflowOAuth scope), the normative contractile snapshot,verification/proofs/README.adoc(recipe names return verbatim in the proofs PR), AFFIRMATION (rewritten in the final anchor PR), and generic template docs slated for the residue-purge PR.🤖 Generated with Claude Code