-
-
Notifications
You must be signed in to change notification settings - Fork 0
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Proofs red on main since b7c780f (#174): census requires CNO.MalbolgeCore; FilesystemCNO.lean does not compile
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlyfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p0Critical - drop other workCritical - drop other workproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositoryStatus: Open.#176 In hyperpolymath/absolute-zero;docs(vocab): 'residue list' collides with the shared glossary's Residue; OND/CNO connection rows proposed for the type-family map
documentationDocs, prose, diagrams, READMEs, ADRsDocs, prose, diagrams, READMEs, ADRsfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p3Low - nice to haveLow - nice to havescope:estateAffects many or all repos across the estateAffects many or all repos across the estateStatus: Open.#175 In hyperpolymath/absolute-zero;Coq: 73 of 182 theorems rest on axioms and the 38 Axiom/Parameter declarations use four tag forms — unify the tag grammar, generate the census
feeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked uptech-debtKnown shortcut, drift, or hygiene owed - includes cleanupKnown shortcut, drift, or hygiene owed - includes cleanupStatus: Open.#171 In hyperpolymath/absolute-zero;Scorecard: 5 high alerts on main from the first real analysis (Token-Permissions ×3, Code-Review, Branch-Protection)
priority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#170 In hyperpolymath/absolute-zero;Lean: port the Coq concrete filesystem model so the FilesystemCNO law axioms become theorems (follow-up to #125/#165)
feeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes theremigrationPorting between languages or toolchains (e.g. -> AffineScript)Porting between languages or toolchains (e.g. -> AffineScript)priority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked uptech-debtKnown shortcut, drift, or hygiene owed - includes cleanupKnown shortcut, drift, or hygiene owed - includes cleanupStatus: Open.#167 In hyperpolymath/absolute-zero;docs/proof-debt.adoc: QuantumCNO §(d) table breaks asciidoctor (literal |0⟩ pipes); y_not_cno comment cites a stale triage line
documentationDocs, prose, diagrams, READMEs, ADRsDocs, prose, diagrams, READMEs, ADRsfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#166 In hyperpolymath/absolute-zero;EchoBridgeCNO.agdahas no--safe --without-Kpragma and is not checked by proofs.yml, while PROOF-STATUS:154 says it type-checks under--safebugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlyfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#162 In hyperpolymath/absolute-zero;Proofsis not a gate:paths: proofs/**filter,z3 … || true, Isabelle/Mizar skipped without failing, no assumption check in CIbugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlyfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#161 In hyperpolymath/absolute-zero;governance: decide whether a Bustfile runner is wanted (old bust.ncl referenced nonexistent ../_base.ncl)
choreRoutine maintenance with no behaviour changeRoutine maintenance with no behaviour changecicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesCI/CD: workflows, actions, lockfiles, pins, runners, release gatesgovernancePolicy, rulesets, standards, compliance, and their enforcementPolicy, rulesets, standards, compliance, and their enforcementpriority:p3Low - nice to haveLow - nice to havescope:repoConfined to this repositoryConfined to this repositoryStatus: Open.#81 In hyperpolymath/absolute-zero;automation: automate docs/wiki → GitHub Wiki sync
automationBots, schedulers, dispatch, self-healing, fan-outBots, schedulers, dispatch, self-healing, fan-outdocumentationDocs, prose, diagrams, READMEs, ADRsDocs, prose, diagrams, READMEs, ADRspriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#80 In hyperpolymath/absolute-zero;docs: consolidate root MAINTAINERS.adoc (estate, 65L) vs docs/MAINTAINERS.adoc (48L)
documentationDocs, prose, diagrams, READMEs, ADRsDocs, prose, diagrams, READMEs, ADRspriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#79 In hyperpolymath/absolute-zero;governance: .machine_readable/svc/README.adoc orphaned after k9 → self-validating rename
documentationDocs, prose, diagrams, READMEs, ADRsDocs, prose, diagrams, READMEs, ADRsgovernancePolicy, rulesets, standards, compliance, and their enforcementPolicy, rulesets, standards, compliance, and their enforcementpriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#78 In hyperpolymath/absolute-zero;