Lean Kernel Arena / tenet-jvm / con-leche

Checker: tenet-jvm · Version: 0.1.3 · 📄 Declaration · 🔗 Source

Test: con-leche · Expected: 👍 accept · Size: 525.9 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.33.0 · Timeout: 12.0 min · 📄 Declaration · 🔗 Source

Result: 👍 accepted · exit code 0 · wall time: 30.9 s · instructions: 361.8 G · max rss memory: 4.7 GB · run 2026-10-24 17:12:50 UTC

stdout:

lean 4.33.0, export format 3.1.0, 10043114 lines
checked 27959 constants ({AXIOM=3, DEF=11486, THM=14983, OPAQUE=10, QUOT=4}) and 333 inductive blocks in 30.75s
axioms declared: propext, Quot.sound, Classical.choice
all declarations verified

stderr:

... 1024 items, at DEF _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.exists_testBit_ne_of_ne.match_1_1
... 2048 items, at THM BitVec.lt_def
... 3072 items, at THM _private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?_eq_utf8DecodeChar?_extract._proof_1_9
... 4096 items, at DEF ConLeche.recRuleK
... 5120 items, at DEF ConLeche.ProjEntry.fireOk
... 6144 items, at DEF ConLeche.BasisDSL.u1N
... 7168 items, at DEF Std.DHashMap.Internal.bucket
... 8192 items, at DEF ConLeche.nativeFieldsOk.match_1
... 9216 items, at DEF _private.ConLeche.Verify.InferLemmas.0.ConLeche.inferTypeCore_lam_inv.match_1_16
... 10240 items, at THM _private.ConLeche.Verify.Cached.GuardsC.0.ConLeche.Expr.fvarLeavesGoC_spec._proof_1_26
... 11264 items, at DEF ConLeche.annotatePis.match_1
... 12288 items, at DEF _private.ConLeche.Verify.Extend.Iota.0.ConLeche.checkIotaRule_inv.match_1_26
... 13312 items, at DEF instSMulOfMul
... 14336 items, at THM _private.ConLeche.Model.Rules.RedSound.0.ConLeche.Model.Rules.Red.proj_sound._proof_1_2
... 15360 items, at DEF _private.ConLeche.Verify.InferLemmas.0.ConLeche.isUnitLikeTy_inv.match_1_33
... 16384 items, at THM ConLeche.Expr.constsResolve.eq_6
... 17408 items, at DEF _private.ConLeche.Model.BasisBlocks.0.ConLeche.Model.declBasisPB_natK.match_1_19
... 18432 items, at THM _private.ConLeche.Model.IndSubst.0.ConLeche.Model.AVExprSubst.inst_inst_comm._proof_1_14
... 19456 items, at DEF _private.Init.Data.List.Monadic.0.List.mapM'_eq_mapM.go._f
... 20480 items, at DEF ConLeche.Model.AnnotValid_mkPisAV_inv._f
... 21504 items, at DEF _private.ConLeche.Semantics.Tower.SumWire.0.ConLeche.Semantics.mkTowerGoUPos_below.match_1_1
... 22528 items, at THM ConLeche.Semantics.frP_of
... 23552 items, at THM ConLeche.Expr.fvarTysOk_fvar
... 24576 items, at THM _private.ConLeche.Model.Denotes.0.ConLeche.Model.Denotes_const_one
... 25600 items, at DEF _private.ConLeche.Frontend.Scan.Equiv.0.ConLeche.Frontend.naiveLineLoop.match_43.splitter
... 26624 items, at DEF _private.ConLeche.Frontend.Scan.Equiv.Objects.0.ConLeche.Frontend.scanIndDeclLoop.match_3.splitter