-
-
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
trustfile.yml 'Check believe_me audit trail' cannot fail — three independent defects
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority: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.#212 In hyperpolymath/proven;62 of 67 DISCHARGED proof claims have never been verified; 4 confirmed false
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority: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.#211 In hyperpolymath/proven;f2833c2c deleted 22 .idr files under a 'feat: add' message — 4 still untracked
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourpriority:p1High - schedule nextHigh - schedule nextscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#210 In hyperpolymath/proven;⚠ The 245 uncommitted files are LOAD-BEARING: 42 .idr files do not parse on origin/main
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority:p1High - schedule nextHigh - schedule nextscope:repoConfined to this repositoryConfined to this repositoryStatus: Open.#209 In hyperpolymath/proven;SafeRegex/Matcher.idr blocks the build at 211/305 — diagnosed, four classes, file is untracked
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourpriority: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.#208 In hyperpolymath/proven;Census: 91 of 379 .idr files have own compile defects (47 parse failures) — revealed by fixing the module-1 stall
priority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorytech-debtKnown shortcut, drift, or hygiene owed - includes cleanupKnown shortcut, drift, or hygiene owed - includes cleanupStatus: Open.#204 In hyperpolymath/proven;SafeRateLimiter: Neg Nat at L74 and L115 blocks the package build at module 5 of 300
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority: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.#203 In hyperpolymath/proven;SafeMCP: idris2 --check does not terminate on 3 modules (same mechanism as the SafePolicy stall)
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority: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.#202 In hyperpolymath/proven;SafeMath.Proofs builds under neither idris2 0.7.0 nor 0.8.0; full proven.ipkg install stalls
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority:p1High - schedule nextHigh - schedule nextscope:repoConfined to this repositoryConfined to this repositoryStatus: Open.#184 In hyperpolymath/proven;Public description overclaims 'cannot crash / formally verified' vs honest MODULE-STATUS (4 proven, 37 safe-only)
bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlypriority: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.#161 In hyperpolymath/proven;proof-debt: paths-forward proposal for the remaining 268 OWED stubs (post-overly-cautious sweep)
priority:p3Low - nice to haveLow - nice to havescope:repoConfined to this repositoryConfined to this repositorytech-debtKnown shortcut, drift, or hygiene owed - includes cleanupKnown shortcut, drift, or hygiene owed - includes cleanupStatus: Open.#119 In hyperpolymath/proven;[umbrella] Phase 3 — proof discharge campaign (SafeUrl warm-up → SafeRegex)
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourpriority:p3Low - nice to haveLow - nice to havescope:repoConfined to this repositoryConfined to this repositoryStatus: Open.#90 In hyperpolymath/proven;