As of main @ 0368e08, src/Proven/SafeMath/Proofs.idr fails to typecheck under both toolchains that were tried (2026-07-20), and a full idris2 --install proven.ipkg appears to hang. Found while wiring proven into metadatastician/idaptik-ums CI.
1. idris2 0.7.0: ItIsSucc vs NonZero
divByOne / modLtDivisor pass ItIsSucc where base-0.7.0's divNatNZ / boundModNatNZ want NonZero / SIsNonZero (the module header says the file was updated for 0.8.0, where the evidence type changed):
Error: While processing right hand side of modLtDivisor. When unifying:
IsSucc (S ?n)
and:
NonZero (S d)
Mismatch between: IsSucc (S ?n) and NonZero (S d).
Proven.SafeMath.Proofs:164:46--164:54
164 | modLtDivisor n (S d) = boundModNatNZ n (S d) ItIsSucc
(Same at Proofs.idr:150-151 for divByOne.) Swapping the three ItIsSucc occurrences to SIsNonZero makes the module build under 0.7.0 — verified locally.
2. idris2 0.8.0 (ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996..., idris2 0.8.0-6ca00e72e): Data.Nat.Division missing
Error: Module Data.Nat.Division not found
Proven.SafeMath.Proofs:21:1--21:25
21 | import Data.Nat.Division
base-0.8.0 in that image has no Data/Nat/Division.ttc (checked the installed package tree), so the "0.8.0-compatible" form of the module does not build on a stock 0.8.0 pack container either.
3. Full idris2 --install proven.ipkg stall (idris2 0.7.0)
A full install of proven.ipkg ran for 15+ minutes of CPU (chezscheme at 99%, >1.1 GB RSS) without writing a single TTC or emitting a single byte of output (/proc/<pid>/io wchar = 0) before being killed. The 13-module subset below installs in well under a minute, so the stall is somewhere in the full 180-module graph, not in the shared leaves.
Downstream workaround (idaptik-ums)
metadatastician/idaptik-ums CI now installs a minimal 13-module closure (scripts/proven-min.ipkg there) as package proven, pinned to 0368e08, after deleting the lone import public Proven.SafeMath.Proofs line from SafeMath.idr — nothing in SafeMath.idr or downstream references Proofs names. That sed + the module's exclusion should be reverted downstream once this is fixed.
Note: gcdZeroRight / gcdCommutative in the same file are declared with no bodies (documented as OWED), so they typecheck as forward declarations only — worth keeping in mind when deciding what "fixed" means for this module.
As of
main@ 0368e08,src/Proven/SafeMath/Proofs.idrfails to typecheck under both toolchains that were tried (2026-07-20), and a fullidris2 --install proven.ipkgappears to hang. Found while wiringprovenintometadatastician/idaptik-umsCI.1. idris2 0.7.0:
ItIsSuccvsNonZerodivByOne/modLtDivisorpassItIsSuccwhere base-0.7.0'sdivNatNZ/boundModNatNZwantNonZero/SIsNonZero(the module header says the file was updated for 0.8.0, where the evidence type changed):(Same at Proofs.idr:150-151 for
divByOne.) Swapping the threeItIsSuccoccurrences toSIsNonZeromakes the module build under 0.7.0 — verified locally.2. idris2 0.8.0 (ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996..., idris2 0.8.0-6ca00e72e):
Data.Nat.Divisionmissingbase-0.8.0 in that image has no
Data/Nat/Division.ttc(checked the installed package tree), so the "0.8.0-compatible" form of the module does not build on a stock 0.8.0 pack container either.3. Full
idris2 --install proven.ipkgstall (idris2 0.7.0)A full install of
proven.ipkgran for 15+ minutes of CPU (chezscheme at 99%, >1.1 GB RSS) without writing a single TTC or emitting a single byte of output (/proc/<pid>/iowchar = 0) before being killed. The 13-module subset below installs in well under a minute, so the stall is somewhere in the full 180-module graph, not in the shared leaves.Downstream workaround (idaptik-ums)
metadatastician/idaptik-umsCI now installs a minimal 13-module closure (scripts/proven-min.ipkgthere) as packageproven, pinned to 0368e08, after deleting the loneimport public Proven.SafeMath.Proofsline fromSafeMath.idr— nothing inSafeMath.idror downstream references Proofs names. That sed + the module's exclusion should be reverted downstream once this is fixed.Note:
gcdZeroRight/gcdCommutativein the same file are declared with no bodies (documented as OWED), so they typecheck as forward declarations only — worth keeping in mind when deciding what "fixed" means for this module.