Lean Kernel Arena / con-leche

Version: c26f793 · 📄 Declaration · 🔗 Source

Test "bugs/constlevels"

Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 25 ms · instructions: 25.8 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 20 records, busy 0.000s (28.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive True (#13); 0.000s inductive Bool (#10); 0.000s def Not (#11); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 4 workers, 8 records, busy 0.000s (30.6%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (40.6%)
con-leche: stats: slowest checks: 0.000s theorem Eq.symm (#16); 0.000s theorem false_ne_true (#17); 0.000s definition Ne (#12); 0.000s definition Not (#11); 0.000s definition Eq.casesOn (#18)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: let value type mismatch [at theorem _test, fold position 19] (--verified) t=0.0s

Test "bugs/ctor-num-fields"

Expected: ✋ reject · Size: 34.1 KB · Lines: 622 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 22.3 M · max rss memory: 20.1 MB

stderr:

con-leche: invalid: constructor _private.Test.0.S.mk declares 0 fields at 0 parameters; its type has 1 binders (--verified)

Test "bugs/eta-ctor-alias"

Expected: ✋ reject · Size: 7.2 KB · Lines: 122 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 24.0 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (29.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (8.7%)
con-leche: stats: slowest installs: 0.000s inductive Box (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (26.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (49.8%)
con-leche: stats: slowest checks: 0.000s theorem etaCtorAlias (#13); 0.000s definition BoxFn (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem etaCtorAlias [at theorem etaCtorAlias, fold position 13] (--verified) t=0.0s

Test "bugs/k-rec-conv"

Expected: ✋ reject · Size: 12.6 KB · Lines: 232 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 25.9 M · max rss memory: 21.4 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 18 records, busy 0.000s (18.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive OfNat (#12); 0.000s inductive Bool (#10); 0.000s def T (#11); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 4 workers, 6 records, busy 0.000s (27.6%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (31.7%)
con-leche: stats: slowest checks: 0.000s theorem bad (#17); 0.000s definition t1 (#15); 0.000s definition T (#11); 0.000s definition instOfNatNat (#14); 0.000s definition t2 (#16)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem bad [at theorem bad, fold position 17] (--verified) t=0.0s

Test "bugs/large-elim-param"

Expected: ✋ reject · Size: 6.2 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

inductive MyBool.{u} : Sort u | tt | ff

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 23.7 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 6 records, busy 0.000s (2.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Empty (#2); 0.000s inductive False (#3)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: generated recursor: large eliminator on a block whose sort may be Prop (official: elim_only_at_universe_zero) [at inductive MyBool, fold position 12] (--verified) t=0.0s

Test "bugs/large-elim-prop-bool"

Expected: ✋ reject · Size: 22.6 KB · Lines: 438 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 25.0 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 18 records, busy 0.000s (17.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (25.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive NewBool (#16); 0.000s inductive Eq (#0); 0.000s def Eq.ndrec (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: generated recursor: large eliminator on a block whose sort may be Prop (official: elim_only_at_universe_zero) [at inductive NewBool, fold position 16] (--verified) t=0.0s

Test "bugs/level-imax-leq"

Expected: ✋ reject · Size: 5.6 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 19.7 M · max rss memory: 20.2 MB

stderr:

con-leche: invalid: recursor False.rec declares k := true; the generated recursor of this block is not K-like (--verified)

Test "bugs/level-imax-normalization"

Expected: ✋ reject · Size: 5.8 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 24.0 M · max rss memory: 21.3 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.001s (31.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (10.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive True (#11); 0.000s def myProp (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (24.8%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (32.6%)
con-leche: stats: slowest checks: 0.000s definition proof_of_false (#14); 0.000s definition down (#12); 0.000s definition myProp (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition down [at def down, fold position 12] (--verified) t=0.0s

Test "bugs/nat-rec-k-lie"

Expected: ✋ reject · Size: 6.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 19.8 M · max rss memory: 20.1 MB

stderr:

con-leche: invalid: recursor Nat.rec declares k := true; the generated recursor of this block is not K-like (--verified)

Test "bugs/nat-rec-rules"

Expected: ✋ reject · Size: 8.1 KB · Lines: 128 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 20.0 M · max rss memory: 20.3 MB

stderr:

con-leche: invalid: recursor False.rec declares k := true; the generated recursor of this block is not K-like (--verified)

Test "bugs/nested-unused-param"

Expected: ✋ reject · Size: 61.1 KB · Lines: 1.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 36.5 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (2 still running, not counted): 0.002s wall, 4 workers + the commit thread, 41 records, busy 0.002s (19.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (71.7%)
con-leche: stats: slowest installs: 0.000s inductive T (#11); 0.000s def Nat.beq (#26); 0.000s inductive HEq (#14); 0.000s inductive PProd (#17); 0.000s inductive P (#36)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid projection: the node names another structure [at inductive E, fold position 40] (--verified) t=0.0s

Test "bugs/orphan-rec"

Expected: ✋ reject · Size: 1.4 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 19.3 M · max rss memory: 17.9 MB

stderr:

con-leche: invalid: recursor rogue declares 0 motives; the block has 1 inductive types (--verified)

Test "bugs/proj-non-structure"

Expected: ✋ reject · Size: 5.0 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 24.3 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (31.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive True (#11); 0.000s inductive Bad (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (28.2%)
con-leche: stats: slowest checks: 0.000s theorem bad (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid projection: not a structure-like type, or no such field [at theorem bad, fold position 13] (--verified) t=0.0s

Test "bugs/proj-of-imax-prop"

Expected: ✋ reject · Size: 19.3 KB · Lines: 321 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 27.2 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 27 records, busy 0.001s (27.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.5%)
con-leche: stats: slowest installs: 0.000s inductive ImaxPropDummy (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive PUnit (#14); 0.000s inductive True (#21)
con-leche: stats: check pool: 0.000s wall, 4 workers, 9 records, busy 0.000s (23.2%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (31.2%)
con-leche: stats: slowest checks: 0.000s definition cond.match_1 (#18); 0.000s definition imaxLeft (#13); 0.000s definition cond (#19); 0.000s definition Bool.casesOn (#16); 0.000s definition Unit.unit (#17)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def imaxProjBool, fold position 20] (--verified) t=0.0s

Test "bugs/proj-of-stuck-prop"

Expected: ✋ reject · Size: 275.7 KB · Lines: 5.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 84.5 M · max rss memory: 31.4 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (1 still running, not counted): 0.003s wall, 4 workers + the commit thread, 108 records, busy 0.004s (29.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (-)
con-leche: stats: slowest installs: 0.000s def Bool.casesOn (#13); 0.000s inductive Nat.le.below (#71); 0.000s inductive Or (#69); 0.000s inductive Acc (#21); 0.000s inductive OfNat (#27)
con-leche: stats: peak RSS 0.03 GiB
con-leche: invalid: direct sum: type former does not reduce to a sort after its parameters and indices [at inductive Native64ResultSortOwner, fold position 112] (--verified) t=0.0s

Test "bugs/proj-of-subst-prop"

Expected: ✋ reject · Size: 254.9 KB · Lines: 4.8 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 135.9 M · max rss memory: 33.6 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.003s wall, 4 workers + the commit thread, 120 records, busy 0.005s (31.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.6%)
con-leche: stats: slowest installs: 0.000s inductive Nat.le.below (#69); 0.000s inductive Or (#67); 0.000s inductive And (#9); 0.000s inductive Nat.le (#24); 0.000s inductive Acc (#21)
con-leche: stats: check pool: 0.002s wall, 4 workers, 89 records, busy 0.006s (76.8%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (30.0%)
con-leche: stats: slowest checks: 0.000s theorem PR14806Subst.run_eq (#113); 0.000s definition _private.Init.Prelude.0.Nat.le_trans.match_1_10 (#85); 0.000s definition _private.Init.Prelude.0.Nat.succ_le_succ.match_1_7 (#77); 0.000s definition Nat.eq_or_lt_of_le._f (#92); 0.000s definition PR14806Subst.step.match_1 (#46)
con-leche: stats: peak RSS 0.03 GiB
con-leche: invalid: application type mismatch [at def PR14806Subst.proposition, fold position 115] (--verified) t=0.0s

Test "bugs/rec-k-lie"

Expected: ✋ reject · Size: 5.3 KB · Lines: 87 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 19.7 M · max rss memory: 20.1 MB

stderr:

con-leche: invalid: recursor MyBool.rec declares k := true; the generated recursor of this block is not K-like (--verified)

Test "bugs/rec-missing-ih"

Expected: ✋ reject · Size: 289.6 KB · Lines: 5.5 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 88.3 M · max rss memory: 35.4 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.004s wall, 4 workers + the commit thread, 17 records, busy 0.001s (7.3%); tail 0.001s after the last start, 1 busy then, 0.000s worker-time in it (0.4%)
con-leche: stats: slowest installs: 0.000s inductive HAdd (#35); 0.000s inductive OfNat (#31); 0.000s def Nat.add (#47); 0.000s quot Quot.lift (#6); 0.000s inductive Eq (#0)
con-leche: stats: peak RSS 0.03 GiB
con-leche: invalid: nested positivity: non valid occurrence of the datatypes being declared [at inductive Native64TwoHashOwner, fold position 111] (--verified) t=0.0s

Test "bugs/rec-of-subst-prop"

Expected: ✋ reject · Size: 269.2 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 139.1 M · max rss memory: 33.4 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 136 records, busy 0.004s (37.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.5%)
con-leche: stats: slowest installs: 0.000s inductive Nat.le.below (#68); 0.000s inductive Acc (#11); 0.000s inductive Or (#66); 0.000s inductive Iff (#129); 0.000s inductive And (#9)
con-leche: stats: check pool: 0.001s wall, 4 workers, 91 records, busy 0.005s (80.1%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (26.9%)
con-leche: stats: slowest checks: 0.000s theorem Issue.gateRun_eq (#111); 0.000s definition _private.Init.Prelude.0.Nat.le_trans.match_1_10 (#83); 0.000s definition Nat.eq_or_lt_of_le._f (#90); 0.000s definition _private.Init.Prelude.0.Nat.succ_le_succ.match_1_7 (#75); 0.000s definition Issue.gateStep.match_1 (#43)
con-leche: stats: peak RSS 0.03 GiB
con-leche: invalid: application type mismatch [at def Issue.proposition, fold position 114] (--verified) t=0.0s

Test "cedar"

Expected: 👍 accept · Size: 832.0 MB · Lines: 15.3 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 3.2 s · instructions: 95.5 G · max rss memory: 870.2 MB

stderr:

con-leche: stats: phases: parse 1.7s, install 1.3s, check not reached
con-leche: stats: install pool (1 still running, not counted): 0.976s wall, 4 workers + the commit thread, 46093 records, busy 3.251s (66.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (-)
con-leche: stats: slowest installs: 0.476s def String.instInhabited (#1254); 0.474s theorem Int.sub_add_cancel (#1344); 0.405s def Nat.xor (#850); 0.371s def Nat.lor (#4614); 0.316s def Nat.land (#373)
con-leche: stats: peak RSS 0.84 GiB
con-leche: not implemented yet: non-standard axiom (_private.Cedar.Thm.SymCC.Data.Ext.0.Cedar.Thm.msPerDay_toInt._native.native_decide.ax_1_1) [at axiom _private.Cedar.Thm.SymCC.Data.Ext.0.Cedar.Thm.msPerDay_toInt._native.native_decide.ax_1_1, fold position 39109] (--verified) t=3.0s

Test "con-leche"

Expected: 👍 accept · Size: 525.9 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.33.0 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19.5 s · instructions: 664.4 G · max rss memory: 674.4 MB

stdout:

con-leche: accepted 26819 declarations (--verified)

stderr:

con-leche: stats: phases: parse 1.0s, install 1.7s, check 16.6s
con-leche: stats: install pool: 1.689s wall, 4 workers + the commit thread, 26820 records, busy 3.728s (44.1%); tail 0.012s after the last start, 4 busy then, 0.001s worker-time in it (2.2%)
con-leche: stats: slowest installs: 0.723s inductive ConLeche.Rules.Red.below (#12934); 0.338s def Nat.xor (#3364); 0.316s def Nat.lor (#966); 0.305s def _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.exists_testBit_ne_of_ne.match_1_1 (#1024); 0.266s inductive ConLeche.Rules.Red (#12922)
con-leche: stats: check pool: 16.663s wall, 4 workers, 26464 records, busy 66.082s (99.1%); tail 0.191s after the last start, 4 busy then, 0.213s worker-time in it (27.7%)
con-leche: stats: slowest checks: 0.380s theorem _private.Init.Data.Array.Extract.0.Array.extract_append._proof_1_1 (#4384); 0.261s theorem ConLeche.Frontend.keyAt_eq (#26124); 0.253s theorem _private.ConLeche.Model.IndBottomNested.0.ConLeche.Model.indBottomNested._proof_1_62 (#19129); 0.244s theorem _private.ConLeche.Model.IndBottomPlain.0.ConLeche.Model.indBottomPlain._proof_1_69 (#18605); 0.233s theorem ConLeche.Model.divMod_install (#17009)
con-leche: stats: peak RSS 0.65 GiB

Test "corner-cases/alg-conv-trans-acc"

Expected: 🤷 either · Size: 66.4 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 53.7 M · max rss memory: 23.3 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 48 records, busy 0.002s (23.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.0%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive HAdd (#21); 0.000s inductive OfNat (#17); 0.000s inductive Nat.le (#14)
con-leche: stats: check pool: 0.000s wall, 4 workers, 27 records, busy 0.002s (59.1%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (30.2%)
con-leche: stats: slowest checks: 0.000s definition step.match_1 (#36); 0.000s theorem trans (#47); 0.000s theorem Nat.lt_succ_self (#42); 0.000s theorem Nat.le_refl (#40); 0.000s definition Nat.brecOn.go (#29)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem trans [at theorem trans, fold position 47] (--verified) t=0.0s

Test "corner-cases/alg-conv-trans-acc-left"

Expected: 🤷 either · Size: 67.4 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 53.8 M · max rss memory: 23.2 MB

stdout:

con-leche: accepted 41 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 49 records, busy 0.002s (23.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.5%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Nat.le (#14); 0.000s inductive HAdd (#21); 0.000s def Nat.add (#34)
con-leche: stats: check pool: 0.000s wall, 4 workers, 28 records, busy 0.001s (49.0%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (11.4%)
con-leche: stats: slowest checks: 0.000s definition step.match_1 (#36); 0.000s theorem Nat.lt_add_one (#41); 0.000s definition step (#43); 0.000s theorem Nat.lt_succ_self (#42); 0.000s definition Nat.brecOn.go (#29)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/alg-conv-trans-acc-right"

Expected: 🤷 either · Size: 67.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 54.6 M · max rss memory: 23.0 MB

stdout:

con-leche: accepted 41 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 49 records, busy 0.002s (24.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.3%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive HAdd (#21); 0.000s inductive Nat.le (#14); 0.000s def Nat.add (#34)
con-leche: stats: check pool: 0.000s wall, 4 workers, 28 records, busy 0.001s (55.8%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (29.3%)
con-leche: stats: slowest checks: 0.000s definition step.match_1 (#36); 0.000s theorem right (#48); 0.000s definition step (#43); 0.000s theorem Nat.lt_add_one (#41); 0.000s definition Nat.brecOn.go (#29)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/alg-conv-trans-quot"

Expected: 🤷 either · Size: 8.5 KB · Lines: 169 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 23.9 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (55.0%)
con-leche: stats: slowest checks: 0.000s theorem trans (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem trans [at theorem trans, fold position 11] (--verified) t=0.0s

Test "corner-cases/alg-conv-trans-quot-left"

Expected: 🤷 either · Size: 8.6 KB · Lines: 173 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 24.0 M · max rss memory: 23.3 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (20.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem left (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (48.8%)
con-leche: stats: slowest checks: 0.000s theorem left (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem left [at theorem left, fold position 11] (--verified) t=0.0s

Test "corner-cases/alg-conv-trans-quot-left-def"

Expected: 🤷 either · Size: 10.5 KB · Lines: 208 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.5 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 8 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (16.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def lift (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (23.7%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (41.9%)
con-leche: stats: slowest checks: 0.000s theorem left' (#13); 0.000s definition lift (#11); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/alg-conv-trans-quot-right"

Expected: 🤷 either · Size: 9.0 KB · Lines: 180 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.1 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive False (#3); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (37.0%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (56.2%)
con-leche: stats: slowest checks: 0.000s theorem right (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/eta-ctor"

Expected: 🤷 either · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 24.7 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (18.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (8.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive T (#12); 0.000s inductive True (#11); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (32.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (49.3%)
con-leche: stats: slowest checks: 0.000s definition etaCtor (#14); 0.000s definition T.val (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition etaCtor [at def etaCtor, fold position 14] (--verified) t=0.0s

Test "corner-cases/eta-rec-struct"

Expected: 🤷 either · Size: 9.5 KB · Lines: 174 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 24.9 M · max rss memory: 23.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (31.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (27.5%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem etaRecStruct (#12); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (76.6%)
con-leche: stats: slowest checks: 0.000s theorem etaRecStruct (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem etaRecStruct [at theorem etaRecStruct, fold position 12] (--verified) t=0.0s

Test "corner-cases/eta-rule-k"

Expected: 🤷 either · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 23.4 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (35.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (34.8%)
con-leche: stats: slowest installs: 0.000s def etaRuleK (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot.lift (#6)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (51.7%)
con-leche: stats: slowest checks: 0.000s definition etaRuleK (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition etaRuleK [at def etaRuleK, fold position 11] (--verified) t=0.0s

Test "corner-cases/eta-struct-major-and"

Expected: 🤷 either · Size: 9.4 KB · Lines: 175 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.4 M · max rss memory: 21.4 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (30.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (19.2%)
con-leche: stats: slowest installs: 0.000s theorem And.left (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot.lift (#6); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (21.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (29.7%)
con-leche: stats: slowest checks: 0.000s theorem andMajorEta (#13); 0.000s theorem And.left (#11); 0.000s theorem And.right (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/eta-struct-major-and-no-whnf"

Expected: 🤷 either · Size: 24.0 KB · Lines: 421 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 29.0 M · max rss memory: 22.8 MB

stdout:

con-leche: accepted 18 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 26 records, busy 0.001s (32.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive True (#11); 0.000s inductive Bool (#10); 0.000s inductive OfNat (#12); 0.000s inductive Iff (#20)
con-leche: stats: check pool: 0.000s wall, 4 workers, 11 records, busy 0.000s (37.2%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (46.1%)
con-leche: stats: slowest checks: 0.000s definition delta (#18); 0.000s theorem andMajorNoWhnf (#25); 0.000s definition andConst (#15); 0.000s definition cast (#19); 0.000s definition OfNat.ofNat (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/eta-struct-major-no-whnf"

Expected: 🤷 either · Size: 32.2 KB · Lines: 582 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 33.8 M · max rss memory: 23.1 MB

stdout:

con-leche: accepted 22 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 30 records, busy 0.001s (26.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.9%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Acc (#16); 0.000s inductive Iff (#21); 0.000s inductive OfNat (#12)
con-leche: stats: check pool: 0.000s wall, 4 workers, 14 records, busy 0.000s (38.6%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (40.5%)
con-leche: stats: slowest checks: 0.000s definition instOfNatNat (#14); 0.000s definition OfNat.ofNat (#13); 0.000s theorem prodMajorNoWhnf (#29); 0.000s definition prodConst (#15); 0.000s theorem tautext (#23)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/eta-unit-like-nested"

Expected: 🤷 either · Size: 16.0 KB · Lines: 256 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 27.1 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 17 records, busy 0.001s (27.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.7%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive Mixed (#14); 0.000s inductive Bool (#10); 0.000s inductive UnitField (#15)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (21.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (41.8%)
con-leche: stats: slowest checks: 0.000s theorem unitLikeNested (#16); 0.000s definition Unit (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem unitLikeNested [at theorem unitLikeNested, fold position 16] (--verified) t=0.0s

Test "corner-cases/eta-unit-like-pi"

Expected: 🤷 either · Size: 5.6 KB · Lines: 101 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 23.8 M · max rss memory: 21.3 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (23.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (11.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (16.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (45.3%)
con-leche: stats: slowest checks: 0.000s theorem unitLikePi (#13); 0.000s definition Unit (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem unitLikePi [at theorem unitLikePi, fold position 13] (--verified) t=0.0s

Test "corner-cases/eta-unit-like-proof-field"

Expected: 🤷 either · Size: 6.5 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 24.2 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (24.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (15.6%)
con-leche: stats: slowest installs: 0.000s inductive True (#11); 0.000s inductive And (#9); 0.000s inductive ProofField (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (54.5%)
con-leche: stats: slowest checks: 0.000s theorem unitLikeProofField (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem unitLikeProofField [at theorem unitLikeProofField, fold position 13] (--verified) t=0.0s

Test "corner-cases/eta-unit-like-struct"

Expected: 🤷 either · Size: 6.7 KB · Lines: 115 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 24.3 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (28.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive UnitField (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (28.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (42.2%)
con-leche: stats: slowest checks: 0.000s theorem unitLikeStruct (#14); 0.000s definition Unit (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem unitLikeStruct [at theorem unitLikeStruct, fold position 14] (--verified) t=0.0s

Test "corner-cases/imax-right-successor"

Expected: 🤷 either · Size: 806 B · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 22.7 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def imaxRightOne (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (5.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.3%)
con-leche: stats: slowest checks: 0.000s definition imaxRightOne (#11); 0.000s definition imaxRightSucc (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/let-value-type-mismatch"

Expected: 🤷 either · Size: 601 B · Lines: 13 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

def EcosystemCase : Sort 2 := let u : Sort 1 := Sort 1; u

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 22.7 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (26.5%)
con-leche: stats: slowest checks: 0.000s definition EcosystemCase (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: let value type mismatch [at def EcosystemCase, fold position 11] (--verified) t=0.0s

Test "corner-cases/nested-nonuniform-param"

Expected: 🤷 either · Size: 9.2 KB · Lines: 142 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 24.9 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 3 records, busy 0.000s (0.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid occurrence of a datatype being declared in the type of E.mk: it must be applied to the parameters and universe levels of the mutual declaration [at inductive E, fold position 13] (--verified) t=0.0s

Test "corner-cases/positivity-whnf"

Expected: 🤷 either · Size: 4.7 KB · Lines: 81 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

def Ignore (A B : Type) : Type := A

inductive T : Type where
  | mk (f : Ignore Unit T -> T) : T

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 23.7 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 6 records, busy 0.000s (1.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s quot Quot.ind (#7); 0.000s axiom Quot.sound (#8); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: nested positivity: non positive occurrence of the datatypes being declared [at inductive LALReduciblePositivity, fold position 14] (--verified) t=0.0s

Test "corner-cases/proj-maybe-prop"

Expected: 🤷 either · Size: 8.1 KB · Lines: 131 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 25.1 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (17.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive MaybeProp (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive PUnit (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (25.2%)
con-leche: stats: slowest checks: 0.000s definition projMaybeProp (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/proj-maybe-prop-past"

Expected: 🤷 either · Size: 8.1 KB · Lines: 131 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 25.1 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.000s wall, 4 workers + the commit thread, 10 records, busy 0.000s (12.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (22.4%)
con-leche: stats: slowest checks: 0.000s definition projMaybePropPast (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/proof-param-ok"

Expected: 👍 accept · Size: 2.9 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.7 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 10 records, busy 0.000s (13.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (13.6%)
con-leche: stats: slowest installs: 0.000s inductive LALProofParameterSwap (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 0 records, busy 0.000s (0.0%)
con-leche: stats: slowest checks: 
con-leche: stats: peak RSS 0.02 GiB

Test "corner-cases/proof-param-swap"

Expected: 🤷 either · Size: 2.9 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 22.8 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 0 records, busy 0.000s (0.0%)
con-leche: stats: slowest installs: 
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: direct sum: invalid constructor return type [at inductive LALProofParameterSwap, fold position 11] (--verified) t=0.0s

Test "corner-cases/subject-reduction-redex"

Expected: 🤷 either · Size: 66.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 14 ms · instructions: 55.1 M · max rss memory: 22.7 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 51 records, busy 0.002s (22.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.3%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive HAdd (#21); 0.000s inductive LT (#12); 0.000s inductive Nat.le (#14)
con-leche: stats: check pool: 0.000s wall, 4 workers, 30 records, busy 0.002s (61.3%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (43.8%)
con-leche: stats: slowest checks: 0.000s definition step.match_1 (#36); 0.000s definition step (#43); 0.000s theorem Nat.lt_add_one (#41); 0.000s definition redex (#50); 0.000s definition Nat.brecOn.go (#29)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: application type mismatch [at def redex, fold position 50] (--verified) t=0.0s

Test "corner-cases/subject-reduction-reduct"

Expected: 🤷 either · Size: 65.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 54.3 M · max rss memory: 23.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 50 records, busy 0.002s (23.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.0%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Nat.le (#14); 0.000s inductive HAdd (#21); 0.000s def Nat.add (#34)
con-leche: stats: check pool: 0.000s wall, 4 workers, 29 records, busy 0.002s (63.0%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (66.8%)
con-leche: stats: slowest checks: 0.000s definition step.match_1 (#36); 0.000s theorem Nat.lt_add_one (#41); 0.000s theorem Nat.lt_succ_self (#42); 0.000s definition step (#43); 0.000s definition Nat.brecOn.go (#29)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: application type mismatch [at def reduct, fold position 49] (--verified) t=0.0s

Test "cslib"

Expected: 👍 accept · Size: 2.3 GB · Lines: 42.7 M · lean4export: 3.1.0 · Lean: 4.34.0 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 1.1 m · instructions: 2.5 T · max rss memory: 2.0 GB

stdout:

con-leche: accepted 383976 declarations (--verified)

stderr:

con-leche: 2 declarations hoisted ahead of the pinned Nat operations they ground: Nat.mul._f, Nat.mul
con-leche: stats: phases: parse 6.3s, install 4.3s, check 56.7s
con-leche: stats: install pool: 3.056s wall, 4 workers + the commit thread, 383976 records, busy 12.179s (79.7%); tail 0.019s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.453s def Nat.xor (#9301); 0.426s inductive Lean.Name (#1475); 0.425s def String.instInhabited (#1453); 0.418s theorem Lean.Omega.Constraint.addInequality_sat (#1536); 0.379s def Nat.lor (#7971)
con-leche: stats: check pool: 56.616s wall, 4 workers, 379926 records, busy 226.081s (99.8%); tail 0.088s after the last start, 4 busy then, 0.085s worker-time in it (24.2%)
con-leche: stats: slowest checks: 0.447s theorem _private.Init.Data.Array.Extract.0.Array.extract_append._proof_1_1 (#14232); 0.341s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_append._proof_1 (#288510); 0.319s theorem _private.Cslib.Computability.Automata.NA.Loop.0.Cslib.Automata.NA.loop_fin_run_exists._proof_1_179 (#110807); 0.298s theorem Algebra.TensorProduct.tensorTensorTensorComm._proof_2 (#280503); 0.267s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_extract._proof_1 (#169266)
con-leche: stats: peak RSS 1.98 GiB

Test "init"

Expected: 👍 accept · Size: 331.5 MB · Lines: 6.5 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12.0 s · instructions: 431.1 G · max rss memory: 533.4 MB

stdout:

con-leche: accepted 58170 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.5s, install 1.0s, check 10.3s
con-leche: stats: install pool: 0.937s wall, 4 workers + the commit thread, 58170 records, busy 3.238s (69.0%); tail 0.034s after the last start, 4 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.482s def Nat.xor (#5984); 0.431s def Nat.lor (#2479); 0.315s def Nat.land (#591); 0.307s def List.get!Internal._f (#1363); 0.289s def Ordering.isLE._sparseCasesOn_1 (#2290)
con-leche: stats: check pool: 10.368s wall, 4 workers, 57527 records, busy 41.241s (99.4%); tail 0.071s after the last start, 4 busy then, 0.070s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.403s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_append._proof_1 (#42191); 0.384s theorem _private.Init.Data.Array.Extract.0.Array.extract_append._proof_1_1 (#4399); 0.259s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_extract._proof_1 (#49769); 0.219s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_append_extract._proof_1 (#35884); 0.209s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_1 (#3985)
con-leche: stats: peak RSS 0.52 GiB

Test "init-prelude"

Expected: 👍 accept · Size: 3.6 MB · Lines: 64.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 132 ms · instructions: 2.4 G · max rss memory: 45.4 MB

stdout:

con-leche: accepted 1824 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.081s wall, 4 workers + the commit thread, 1824 records, busy 0.330s (81.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.8%)
con-leche: stats: slowest installs: 0.076s def Lean.Name.hasMacroScopes._f (#680); 0.076s def SMul.ctorIdx (#834); 0.069s def _private.Init.Prelude.0.Lean.MacroScopesView.review.match_1 (#705); 0.035s def Nat.mod (#219); 0.020s def Nat.div (#270)
con-leche: stats: check pool: 0.024s wall, 4 workers, 1682 records, busy 0.096s (97.2%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (32.8%)
con-leche: stats: slowest checks: 0.002s definition Lean.ParserDescr.noConfusion (#971); 0.001s definition Lean.ParserDescr.ctorElim (#467); 0.001s definition Trans.noConfusion (#617); 0.001s theorem Nat.modCore_lt (#244); 0.000s theorem Lean.ParserDescr.brecOn.eq (#1790)
con-leche: stats: peak RSS 0.04 GiB

Test "mathlib"

Expected: 👍 accept · Size: 5.8 GB · Lines: 109.8 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 3.7 m · instructions: 7.9 T · max rss memory: 5.1 GB

stdout:

con-leche: accepted 702040 declarations (--verified)

stderr:

con-leche: 2 declarations hoisted ahead of the pinned Nat operations they ground: Nat.mul._f, Nat.mul
con-leche: stats: phases: parse 17.7s, install 10.8s, check 195.3s
con-leche: stats: install pool: 7.129s wall, 4 workers + the commit thread, 702040 records, busy 28.867s (80.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.7%)
con-leche: stats: slowest installs: 0.634s inductive Lean.Name (#1475); 0.633s def String.instInhabited (#1453); 0.624s theorem Lean.Omega.Constraint.addInequality_sat (#1536); 0.508s def Nat.land (#636); 0.435s def Nat.xor (#10984)
con-leche: stats: check pool: 194.957s wall, 4 workers, 695214 records, busy 779.293s (99.9%); tail 0.079s after the last start, 4 busy then, 0.072s worker-time in it (22.7%)
con-leche: stats: slowest checks: 6.431s theorem _private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.Affine.Point.sym2x_add_sub_eq_addSubMap_sym2x._proof_1_8 (#440037); 1.470s theorem _private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.edgeDensity_star_not_uniform._proof_1_10 (#215811); 1.185s definition QuadraticModuleCat.instMonoidalCategoryStruct (#276667); 1.155s theorem QuadraticModuleCat.hom_hom_associator (#276668); 1.070s theorem QuadraticModuleCat.hom_inv_associator (#277682)
con-leche: stats: peak RSS 5.09 GiB

Test "navier-stokes-euler"

Expected: 👍 accept · Size: 1.5 GB · Lines: 28.6 M · lean4export: 3.1.0 · Lean: 4.34.0-rc2 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 1.7 m · instructions: 2.8 T · max rss memory: 1.4 GB

stdout:

con-leche: accepted 126468 declarations (--verified)

stderr:

con-leche: stats: phases: parse 4.1s, install 3.5s, check 92.1s
con-leche: stats: install pool: 2.837s wall, 4 workers + the commit thread, 126468 records, busy 11.987s (84.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (2.4%)
con-leche: stats: slowest installs: 0.381s def Nat.land (#1659); 0.202s inductive EulerMeanVariationalInverse.StrongMeanEvolution (#95851); 0.171s inductive EulerPacketMovingFrame.PhysicalGeometryData (#104023); 0.171s inductive EulerTransversePacketJoin.Budget (#104861); 0.168s inductive EulerMeanPacketProvider.Data (#95680)
con-leche: stats: check pool: 92.116s wall, 4 workers, 124834 records, busy 368.336s (99.9%); tail 0.009s after the last start, 4 busy then, 0.012s worker-time in it (34.4%)
con-leche: stats: slowest checks: 1.145s theorem NavierStokes.FiveProfileMoments.quadraticBilin._proof_6 (#50132); 0.762s theorem NavierStokes.FiveProfileMoments.quadraticBilin._proof_9 (#50135); 0.529s theorem NavierStokes.TerminalCompensation.quadraticBilin._proof_6 (#57739); 0.432s theorem _private.Mathlib.Analysis.ODE.ExistUnique.0.ODE_solution_unique_univ._proof_1_2 (#110301); 0.386s theorem EulerTransversePacketJoin.derivative_match (#103261)
con-leche: stats: peak RSS 1.40 GiB

Test "other/extra-rec"

Expected: ✋ reject · Size: 1.4 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 19.3 M · max rss memory: 18.1 MB

stderr:

con-leche: invalid: recursor rogue declares 0 motives; the block has 1 inductive types (--verified)

Test "other/level-index-out-of-order"

Expected: 👍 accept · Size: 328 B · Lines: 6 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: 🚫 declined · exit code 2 · wall time: 26 ms · instructions: 22.5 M · max rss memory: 20.5 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.001s wall, 4 workers + the commit thread, 5 records, busy 0.000s (2.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive False (#3); 0.000s quot Quot.lift (#6); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (foo) [at axiom foo, fold position 11] (--verified) t=0.0s

Test "other/nat-lit-add"

Expected: 👍 accept · Size: 26.0 KB · Lines: 478 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 24 ms · instructions: 31.6 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 16 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 25 records, busy 0.002s (25.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.2%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s def Nat.add (#19); 0.000s inductive PProd (#12); 0.000s inductive OfNat (#20)
con-leche: stats: check pool: 0.000s wall, 4 workers, 10 records, busy 0.000s (35.2%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (26.3%)
con-leche: stats: slowest checks: 0.000s definition Nat.brecOn.go (#14); 0.000s theorem natAddLit (#24); 0.000s definition Nat.casesOn (#16); 0.000s definition Nat.below (#13); 0.000s definition Nat.add._f (#18)
con-leche: stats: peak RSS 0.02 GiB

Test "other/nat-lit-add-bad"

Expected: ✋ reject · Size: 25.3 KB · Lines: 465 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

natAddLitBad : Nat.add 123456789 987654321 = 1111111111
  := Eq.refl (Nat.add 123456789 987654321)

Test result: ✋ rejected · exit code 1 · wall time: 27 ms · instructions: 31.4 M · max rss memory: 22.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 24 records, busy 0.003s (26.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (8.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s def Nat.add (#19); 0.000s inductive PProd (#12); 0.000s inductive OfNat (#20)
con-leche: stats: check pool: 0.001s wall, 4 workers, 9 records, busy 0.001s (32.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.1%)
con-leche: stats: slowest checks: 0.000s definition Nat.brecOn.go (#14); 0.000s theorem natAddLitBad (#23); 0.000s definition Nat.below (#13); 0.000s definition Nat.add._f (#18); 0.000s definition Nat.add.match_1 (#17)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem natAddLitBad [at theorem natAddLitBad, fold position 23] (--verified) t=0.0s

Test "other/nat-lit-ble"

Expected: 👍 accept · Size: 28.8 KB · Lines: 520 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 26 ms · instructions: 32.2 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 17 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 25 records, busy 0.003s (24.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.4%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s def Nat.ble (#19); 0.000s inductive OfNat (#20); 0.000s inductive PProd (#12)
con-leche: stats: check pool: 0.000s wall, 4 workers, 10 records, busy 0.001s (35.6%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (41.5%)
con-leche: stats: slowest checks: 0.000s definition Nat.brecOn.go (#14); 0.000s definition Nat.casesOn (#16); 0.000s definition Nat.below (#13); 0.000s definition Nat.ble._f (#18); 0.000s definition Nat.brecOn (#15)
con-leche: stats: peak RSS 0.02 GiB

Test "other/nat-lit-sub"

Expected: 👍 accept · Size: 30.0 KB · Lines: 561 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 29 ms · instructions: 33.2 M · max rss memory: 23.1 MB

stdout:

con-leche: accepted 20 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 29 records, busy 0.002s (25.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.6%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive PProd (#12); 0.000s def Nat.pred (#24); 0.000s def Nat.sub (#26)
con-leche: stats: check pool: 0.001s wall, 4 workers, 13 records, busy 0.002s (51.3%); tail 0.000s after the last start, 4 busy then, 0.001s worker-time in it (55.9%)
con-leche: stats: slowest checks: 0.000s definition Nat.mul.match_1 (#20); 0.000s definition Nat.pow.match_1 (#23); 0.000s definition Nat.brecOn.go (#14); 0.000s definition Nat.brecOn (#15); 0.000s definition Nat.sub._f (#25)
con-leche: stats: peak RSS 0.02 GiB

Test "other/orphan-ctor"

Expected: ✋ reject · Size: 1.4 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: ✋ rejected · exit code 1 · wall time: 17 ms · instructions: 19.3 M · max rss memory: 18.0 MB

stderr:

con-leche: invalid: the inductive block lists 0 constructors and carries 1 constructor records (--verified)

Test "other/proj-of-prop"

Expected: ✋ reject · Size: 3.9 KB · Lines: 56 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

badFalse : False := (Wrapper.mk True.intro).p

Test result: ✋ rejected · exit code 1 · wall time: 26 ms · instructions: 23.8 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 14 records, busy 0.002s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.1%)
con-leche: stats: slowest installs: 0.001s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Wrapper (#11); 0.000s inductive Eq (#0); 0.000s inductive True (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (41.3%)
con-leche: stats: slowest checks: 0.000s theorem badFalse (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: application type mismatch [at theorem badFalse, fold position 13] (--verified) t=0.0s

Test "other/sparse-name-index"

Expected: 👍 accept · Size: 292 B · Lines: 4 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Test result: 🚫 declined · exit code 2 · wall time: 28 ms · instructions: 22.5 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 10 records, busy 0.001s (18.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s axiom foo (#11); 0.000s inductive False (#3)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (foo) [at axiom foo, fold position 11] (--verified) t=0.0s

Test "perf/app-lam"

Expected: 👍 accept · Size: 1.2 MB · Lines: 28.6 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 5.1 s · instructions: 24.4 G · max rss memory: 1.2 GB

stdout:

con-leche: accepted 22 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 5.0s
con-leche: stats: install pool: 0.013s wall, 4 workers + the commit thread, 32 records, busy 0.014s (21.7%); tail 0.010s after the last start, 1 busy then, 0.010s worker-time in it (19.8%)
con-leche: stats: slowest installs: 0.010s def dag_app_binder (#31); 0.001s inductive HAdd (#12); 0.001s inductive And (#9); 0.000s def Nat.add (#25); 0.000s inductive OfNat (#27)
con-leche: stats: check pool: 5.026s wall, 4 workers, 15 records, busy 5.026s (25.0%); tail 5.025s after the last start, 4 busy then, 5.025s worker-time in it (24.9%)
con-leche: stats: slowest checks: 5.025s definition dag_app_binder (#31); 0.000s definition Nat.add._f (#24); 0.000s definition Nat.brecOn.go (#20); 0.000s definition instHAdd (#16); 0.000s definition HAdd.hAdd (#13)
con-leche: stats: peak RSS 1.22 GiB

Test "perf/args-before-unfold"

Expected: 👍 accept · Size: 44.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

count #n      and      count (N.add #(n-1) #1)

Test result: 👍 accepted · exit code 0 · wall time: 32 ms · instructions: 85.9 M · max rss memory: 24.2 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.001s (33.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (37.5%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s theorem kernel_args_before_unfold (#14); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.008s wall, 3 workers, 3 records, busy 0.008s (32.8%); tail 0.008s after the last start, 3 busy then, 0.008s worker-time in it (33.2%)
con-leche: stats: slowest checks: 0.008s theorem kernel_args_before_unfold (#14); 0.000s definition N.add (#12); 0.000s definition count (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/beta-ladder"

Expected: 👍 accept · Size: 450.6 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(fun x₁ => … (fun xₙ => x₁ + (x₂ + (… + (xₙ + 0)))) 0 …) 0

Test result: 👍 accepted · exit code 0 · wall time: 701 ms · instructions: 5.4 G · max rss memory: 393.9 MB

stdout:

con-leche: accepted 12 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.6s
con-leche: stats: install pool: 0.004s wall, 4 workers + the commit thread, 21 records, busy 0.005s (24.1%); tail 0.002s after the last start, 1 busy then, 0.002s worker-time in it (19.5%)
con-leche: stats: slowest installs: 0.002s theorem beta_ladder (#20); 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s def Nat.add (#19); 0.000s inductive PProd (#12)
con-leche: stats: check pool: 0.659s wall, 4 workers, 7 records, busy 0.660s (25.0%); tail 0.659s after the last start, 4 busy then, 0.659s worker-time in it (25.0%)
con-leche: stats: slowest checks: 0.658s theorem beta_ladder (#20); 0.000s definition Nat.brecOn.go (#14); 0.000s definition Nat.below (#13); 0.000s definition Nat.brecOn (#15); 0.000s definition Nat.add._f (#18)
con-leche: stats: peak RSS 0.38 GiB

Test "perf/church-numerals"

Expected: 👍 accept · Size: 9.6 KB · Lines: 227 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

cmul (cnum n) (cnum (n+1))      and      cmul (cnum (n+1)) (cnum n)

Test result: 👍 accepted · exit code 0 · wall time: 116 ms · instructions: 319.7 M · max rss memory: 46.1 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.001s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s def CNat (#11)
con-leche: stats: check pool: 0.087s wall, 3 workers, 3 records, busy 0.086s (33.1%); tail 0.086s after the last start, 3 busy then, 0.086s worker-time in it (33.2%)
con-leche: stats: slowest checks: 0.086s theorem kernel_church_numerals (#13); 0.000s definition cmul (#12); 0.000s definition CNat (#11)
con-leche: stats: peak RSS 0.04 GiB

Test "perf/discarded-argument"

Expected: 👍 accept · Size: 15.9 KB · Lines: 367 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

dropArg (count #n)      and      dropArg (count #(n+1))

Test result: 👍 accepted · exit code 0 · wall time: 49 ms · instructions: 79.0 M · max rss memory: 25.1 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 16 records, busy 0.001s (29.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (22.8%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s theorem kernel_discarded_argument (#15)
con-leche: stats: check pool: 0.008s wall, 4 workers, 4 records, busy 0.008s (24.4%); tail 0.008s after the last start, 3 busy then, 0.008s worker-time in it (25.0%)
con-leche: stats: slowest checks: 0.007s theorem kernel_discarded_argument (#15); 0.000s definition count (#14); 0.000s definition N.add (#13); 0.000s definition dropArg (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/discarded-argument-match"

Expected: 👍 accept · Size: 29.2 KB · Lines: 606 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

dropArg (count #n)      and      dropArg (count #(n+1))

Test result: 👍 accepted · exit code 0 · wall time: 64 ms · instructions: 224.9 M · max rss memory: 25.3 MB

stdout:

con-leche: accepted 17 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 27 records, busy 0.002s (29.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.7%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive PProd (#14); 0.000s inductive Bool (#10); 0.000s inductive PUnit (#13)
con-leche: stats: check pool: 0.037s wall, 4 workers, 13 records, busy 0.037s (25.3%); tail 0.036s after the last start, 4 busy then, 0.036s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.036s theorem kernel_discarded_argument_match (#26); 0.000s definition N.brecOn.go (#16); 0.000s definition N.add.match_1 (#21); 0.000s definition N.add._f (#22); 0.000s definition N.below (#15)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/folded-constant-first"

Expected: 👍 accept · Size: 52.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

tagged (count #n)      and      (false, count #n)

Test result: 👍 accepted · exit code 0 · wall time: 46 ms · instructions: 118.1 M · max rss memory: 24.4 MB

stdout:

con-leche: accepted 9 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.003s wall, 4 workers + the commit thread, 18 records, busy 0.003s (21.3%); tail 0.001s after the last start, 1 busy then, 0.001s worker-time in it (19.5%)
con-leche: stats: slowest installs: 0.001s theorem kernel_folded_constant_first (#17); 0.001s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.020s wall, 4 workers, 5 records, busy 0.020s (24.5%); tail 0.019s after the last start, 4 busy then, 0.019s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.019s theorem kernel_folded_constant_first (#17); 0.000s definition isZero (#13); 0.000s definition count (#16); 0.000s definition tagged (#14); 0.000s definition N.add (#15)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/folded-constant-last"

Expected: 👍 accept · Size: 51.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

tagged (count #n)      and      (count #n, false)

Test result: 👍 accepted · exit code 0 · wall time: 49 ms · instructions: 117.8 M · max rss memory: 24.6 MB

stdout:

con-leche: accepted 9 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 18 records, busy 0.001s (17.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s theorem kernel_folded_constant_last (#17); 0.000s inductive Prod (#11); 0.000s inductive Bool (#10); 0.000s inductive N (#12)
con-leche: stats: check pool: 0.019s wall, 4 workers, 5 records, busy 0.019s (25.0%); tail 0.018s after the last start, 3 busy then, 0.018s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.018s theorem kernel_folded_constant_last (#17); 0.000s definition tagged (#14); 0.000s definition isZero (#13); 0.000s definition N.add (#15); 0.000s definition count (#16)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/fueled-chain"

Expected: 👍 accept · Size: 848.6 KB · Lines: 17.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 77 ms · instructions: 422.6 M · max rss memory: 45.5 MB

stdout:

con-leche: accepted 143 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.006s wall, 4 workers + the commit thread, 145 records, busy 0.012s (36.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (6.6%)
con-leche: stats: slowest installs: 0.001s def Bool.casesOn (#67); 0.001s inductive Iff (#128); 0.001s inductive Except (#11); 0.000s inductive And (#9); 0.000s inductive MonadExceptOf (#26)
con-leche: stats: check pool: 0.022s wall, 4 workers, 109 records, busy 0.056s (61.3%); tail 0.019s after the last start, 4 busy then, 0.043s worker-time in it (56.7%)
con-leche: stats: slowest checks: 0.018s theorem chain12_datF (#144); 0.013s theorem chain6_datF (#140); 0.012s theorem chain9_datF (#142); 0.000s definition Except.map.match_1 (#90); 0.000s theorem lift_atF (#124)
con-leche: stats: peak RSS 0.04 GiB

Test "perf/grind-ring-5"

Expected: 👍 accept · Size: 9.8 MB · Lines: 200.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 6.1 s · instructions: 26.0 G · max rss memory: 179.5 MB

stdout:

con-leche: accepted 2273 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.9s, check 5.0s
con-leche: stats: install pool: 0.928s wall, 4 workers + the commit thread, 2274 records, busy 1.487s (32.0%); tail 0.002s after the last start, 4 busy then, 0.000s worker-time in it (0.3%)
con-leche: stats: slowest installs: 0.766s def Nat.land (#795); 0.155s def Lean.Grind.Semiring.ofNat_succ._autoParam (#309); 0.150s def Lean.Grind.Ring.zsmul_natCast_eq_nsmul._autoParam (#334); 0.104s def Classical.propDecidable.match_1 (#386); 0.089s def Nat.mod (#216)
con-leche: stats: check pool: 5.046s wall, 4 workers, 2149 records, busy 5.696s (28.2%); tail 4.830s after the last start, 4 busy then, 4.836s worker-time in it (25.0%)
con-leche: stats: slowest checks: 4.830s theorem _private.Test.0.thm._proof_1_1 (#2272); 0.035s theorem _private.Init.Grind.Ring.Basic.0.Lean.Grind.Ring.intCast_nat_sub._proof_1_2 (#1492); 0.024s theorem _private.Init.Data.Nat.Div.Lemmas.0.Nat.div_le_iff_le_mul._proof_1_1 (#1634); 0.018s theorem _private.Init.Data.Nat.Div.Lemmas.0.Nat.lt_of_div_eq_zero._proof_1_1 (#1625); 0.018s theorem _private.Init.Grind.Ring.Basic.0.Lean.Grind.Ring.intCast_nat_sub._proof_1_3 (#1495)
con-leche: stats: peak RSS 0.17 GiB

Test "perf/identical-nesting"

Expected: 👍 accept · Size: 8.7 KB · Lines: 172 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

f4 (f4 (... (f4 N.O) ...))      and      f4 (f4 (... (f4 N.O) ...))

Test result: 👍 accepted · exit code 0 · wall time: 31 ms · instructions: 24.9 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 8 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 18 records, busy 0.002s (18.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.1%)
con-leche: stats: slowest installs: 0.001s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive N (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 4 workers, 6 records, busy 0.000s (10.8%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (11.6%)
con-leche: stats: slowest checks: 0.000s definition f1 (#13); 0.000s theorem kernel_identical_nesting (#17); 0.000s definition f3 (#15); 0.000s definition f0 (#12); 0.000s definition f2 (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/irrelevance-before-evaluation"

Expected: 👍 accept · Size: 17.5 KB · Lines: 388 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

slowTriv (count #n) = True.intro

Test result: 👍 accepted · exit code 0 · wall time: 31 ms · instructions: 28.1 M · max rss memory: 21.4 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 17 records, busy 0.001s (24.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.2%)
con-leche: stats: slowest installs: 0.000s inductive True (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 4 workers, 4 records, busy 0.000s (22.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (30.7%)
con-leche: stats: slowest checks: 0.000s theorem kernel_irrelevance_before_evaluation (#16); 0.000s definition count (#15); 0.000s definition slowTriv (#13); 0.000s definition N.add (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/irrelevance-refutes"

Expected: 👍 accept · Size: 13.1 KB · Lines: 244 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

f 100000 (slowRefl 100000) = f 100001 (slowRefl 100001)

Test result: 👍 accepted · exit code 0 · wall time: 30 ms · instructions: 25.8 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 9 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 18 records, busy 0.001s (18.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive OfNat (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def OfNat.ofNat (#12)
con-leche: stats: check pool: 0.001s wall, 4 workers, 6 records, busy 0.000s (16.5%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (35.2%)
con-leche: stats: slowest checks: 0.000s theorem irrelevance_refutes (#17); 0.000s definition f (#14); 0.000s definition slowRefl (#16); 0.000s definition OfNat.ofNat (#12); 0.000s definition instOfNatNat (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/let-fold"

Expected: 👍 accept · Size: 316.9 KB · Lines: 6.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

let d := bits #n 0; (rfl : d + 0 = Nat.add d 0)

Test result: 👍 accepted · exit code 0 · wall time: 5.5 s · instructions: 15.2 G · max rss memory: 351.4 MB

stdout:

con-leche: accepted 156 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 5.3s
con-leche: stats: install pool: 0.087s wall, 4 workers + the commit thread, 162 records, busy 0.093s (21.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (2.4%)
con-leche: stats: slowest installs: 0.082s def Nat.mod (#149); 0.000s inductive Mul (#153); 0.000s inductive HMul (#151); 0.000s inductive And (#9); 0.000s inductive LT (#98)
con-leche: stats: check pool: 5.398s wall, 4 workers, 126 records, busy 5.408s (25.0%); tail 5.394s after the last start, 4 busy then, 5.394s worker-time in it (24.9%)
con-leche: stats: slowest checks: 5.393s theorem kernel_let_fold (#161); 0.000s definition _private.Init.Prelude.0.Nat.le_trans.match_1_10 (#117); 0.000s definition _private.Init.Prelude.0.Nat.succ_le_succ.match_1_7 (#83); 0.000s definition _private.Init.Prelude.0.Nat.ble_eq_true_of_le.match_1_7 (#88); 0.000s theorem Nat.succ_sub_succ_eq_sub (#139)
con-leche: stats: peak RSS 0.34 GiB

Test "perf/let-ladder"

Expected: 👍 accept · Size: 457.6 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

let x₃ := 0; x₃ + (let x₂ := 0; x₂ + (let x₁ := 0; x₁ + (x₃ + (x₂ + (x₁ + 0)))))

Test result: 👍 accepted · exit code 0 · wall time: 485 ms · instructions: 2.9 G · max rss memory: 225.7 MB

stdout:

con-leche: accepted 14 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.4s
con-leche: stats: install pool: 0.007s wall, 4 workers + the commit thread, 24 records, busy 0.006s (18.2%); tail 0.003s after the last start, 1 busy then, 0.003s worker-time in it (18.9%)
con-leche: stats: slowest installs: 0.003s def kernel_quadratic_let_ladder (#23); 0.001s inductive And (#9); 0.000s def Nat.add (#22); 0.000s inductive Bool (#10); 0.000s inductive OfNat (#11)
con-leche: stats: check pool: 0.432s wall, 4 workers, 9 records, busy 0.432s (24.9%); tail 0.431s after the last start, 3 busy then, 0.431s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.431s definition kernel_quadratic_let_ladder (#23); 0.000s definition Nat.add.match_1 (#20); 0.000s definition Nat.brecOn.go (#17); 0.000s definition Nat.add._f (#21); 0.000s definition OfNat.ofNat (#12)
con-leche: stats: peak RSS 0.22 GiB

Test "perf/magma-list-deep-n21"

Expected: 👍 accept · Size: 1.1 MB · Lines: 21.8 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10.1 s · instructions: 24.3 G · max rss memory: 596.3 MB

stdout:

con-leche: accepted 514 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 1.1s, check 8.9s
con-leche: stats: install pool: 1.133s wall, 4 workers + the commit thread, 520 records, busy 2.355s (41.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.7%)
con-leche: stats: slowest installs: 1.002s def Nat.land (#345); 0.996s def List.get!Internal._f (#474); 0.134s def String.instInhabited (#461); 0.120s def Nat.mod (#166); 0.056s def Nat.div (#214)
con-leche: stats: check pool: 8.946s wall, 4 workers, 451 records, busy 8.985s (25.1%); tail 8.932s after the last start, 4 busy then, 8.932s worker-time in it (24.9%)
con-leche: stats: slowest checks: 8.932s definition countermodel (#519); 0.001s definition _private.Init.Data.Nat.Div.Basic.0.Nat.div.go.fuel_congr._f (#260); 0.001s theorem Nat.modCore_lt (#419); 0.001s theorem Nat.div_eq_ite (#262); 0.000s theorem Nat.le_trans (#135)
con-leche: stats: peak RSS 0.58 GiB

Test "perf/magma-list-deep-n36"

Expected: 👍 accept · Size: 1.2 MB · Lines: 23.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 1.9 m · instructions: 282.0 G · max rss memory: 7.3 GB

stdout:

con-leche: accepted 514 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 1.1s, check 112.3s
con-leche: stats: install pool: 1.125s wall, 4 workers + the commit thread, 520 records, busy 2.338s (41.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.2%)
con-leche: stats: slowest installs: 0.972s def Nat.land (#345); 0.966s def List.get!Internal._f (#474); 0.155s def String.instInhabited (#461); 0.142s def Nat.mod (#166); 0.060s def Nat.div (#214)
con-leche: stats: check pool: 112.330s wall, 4 workers, 451 records, busy 112.366s (25.0%); tail 112.317s after the last start, 4 busy then, 112.317s worker-time in it (25.0%)
con-leche: stats: slowest checks: 112.317s definition countermodel (#519); 0.001s theorem Nat.modCore_lt (#419); 0.001s definition _private.Init.Data.Nat.Div.Basic.0.Nat.div.go.fuel_congr._f (#260); 0.001s theorem Nat.div_eq_ite (#262); 0.000s definition Nat.decidableBallLT._f (#508)
con-leche: stats: peak RSS 7.34 GiB

Test "perf/magma-list-pair-n21"

Expected: 👍 accept · Size: 583.1 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 38.7 s · instructions: 186.8 G · max rss memory: 5.1 GB

stdout:

con-leche: accepted 276 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 38.5s
con-leche: stats: install pool: 0.036s wall, 4 workers + the commit thread, 282 records, busy 0.042s (23.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.1%)
con-leche: stats: slowest installs: 0.033s def Nat.mod (#151); 0.000s inductive Exists (#11); 0.000s inductive Nat.le.below (#73); 0.000s inductive Mod (#157); 0.000s inductive And (#9)
con-leche: stats: check pool: 38.579s wall, 4 workers, 240 records, busy 38.592s (25.0%); tail 38.575s after the last start, 4 busy then, 38.575s worker-time in it (25.0%)
con-leche: stats: slowest checks: 38.575s definition countermodel (#281); 0.000s theorem Nat.modCore_lt (#186); 0.000s theorem Nat.modCoreGo_lt (#185); 0.000s definition _private.Init.Prelude.0.Nat.ble_eq_true_of_le.match_1_7 (#94); 0.000s theorem Nat.succ_sub_succ_eq_sub (#141)
con-leche: stats: peak RSS 5.11 GiB

Test "perf/magma-list-pair-n7"

Expected: 👍 accept · Size: 583.6 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 2.8 s · instructions: 17.0 G · max rss memory: 475.8 MB

stdout:

con-leche: accepted 276 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 2.7s
con-leche: stats: install pool: 0.040s wall, 4 workers + the commit thread, 282 records, busy 0.045s (22.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.9%)
con-leche: stats: slowest installs: 0.036s def Nat.mod (#151); 0.000s inductive Exists (#11); 0.000s inductive Nat.le.below (#73); 0.000s inductive Mod (#157); 0.000s inductive NeZero (#257)
con-leche: stats: check pool: 2.724s wall, 4 workers, 240 records, busy 2.738s (25.1%); tail 2.720s after the last start, 4 busy then, 2.720s worker-time in it (25.0%)
con-leche: stats: slowest checks: 2.720s definition countermodel (#281); 0.000s theorem Nat.modCore_lt (#186); 0.000s definition _private.Init.Prelude.0.Nat.le_trans.match_1_10 (#119); 0.000s definition _private.Init.Prelude.0.Nat.succ_le_succ.match_1_7 (#79); 0.000s theorem Nat.succ_sub_succ_eq_sub (#141)
con-leche: stats: peak RSS 0.46 GiB

Test "perf/magma-string-n4"

Expected: 👍 accept · Size: 16.5 MB · Lines: 344.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 1.2 s · instructions: 31.0 G · max rss memory: 138.0 MB

stdout:

con-leche: accepted 3268 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.4s, check 0.7s
con-leche: stats: install pool: 0.467s wall, 4 workers + the commit thread, 3269 records, busy 1.687s (72.2%); tail 0.001s after the last start, 1 busy then, 0.000s worker-time in it (0.3%)
con-leche: stats: slowest installs: 0.461s def Nat.lor (#961); 0.320s def Nat.land (#492); 0.311s theorem Nat.exists_testBit_ne_of_ne (#1035); 0.293s def List.get?Internal._sparseCasesOn_1 (#1667); 0.087s def ByteArray.get._auto_1 (#936)
con-leche: stats: check pool: 0.727s wall, 4 workers, 3135 records, busy 2.389s (82.1%); tail 0.177s after the last start, 4 busy then, 0.192s worker-time in it (27.1%)
con-leche: stats: slowest checks: 0.230s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_1 (#2694); 0.181s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_3 (#2701); 0.177s definition countermodel (#3268); 0.076s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_2 (#2702); 0.058s theorem _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.two_pow_succ_sub_succ_div_two._proof_1_1 (#2026)
con-leche: stats: peak RSS 0.13 GiB

Test "perf/magma-string-pair-n9"

Expected: 👍 accept · Size: 16.6 MB · Lines: 344.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 7.8 s · instructions: 72.7 G · max rss memory: 968.2 MB

stdout:

con-leche: accepted 3268 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.4s, check 7.3s
con-leche: stats: install pool: 0.443s wall, 4 workers + the commit thread, 3269 records, busy 1.627s (73.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.5%)
con-leche: stats: slowest installs: 0.438s def Nat.lor (#961); 0.310s def Nat.land (#492); 0.302s theorem Nat.exists_testBit_ne_of_ne (#1035); 0.285s def List.get?Internal._sparseCasesOn_1 (#1667); 0.082s def ByteArray.get._auto_1 (#936)
con-leche: stats: check pool: 7.327s wall, 4 workers, 3135 records, busy 8.912s (30.4%); tail 6.804s after the last start, 4 busy then, 6.820s worker-time in it (25.0%)
con-leche: stats: slowest checks: 6.803s definition countermodel (#3268); 0.232s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_1 (#2694); 0.175s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_3 (#2701); 0.076s theorem _private.Init.Data.Array.Extract.0.Array.extract_append_extract._proof_1_2 (#2702); 0.042s theorem _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.two_pow_succ_sub_succ_div_two._proof_1_1 (#2026)
con-leche: stats: peak RSS 0.94 GiB

Test "perf/proj-cheap-struct"

Expected: 👍 accept · Size: 85.9 KB · Lines: 1.5 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(S u).re      and      (S ()).re

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 57.5 M · max rss memory: 23.1 MB

stdout:

con-leche: accepted 57 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.003s wall, 4 workers + the commit thread, 66 records, busy 0.005s (26.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.3%)
con-leche: stats: slowest installs: 0.000s def List.below (#17); 0.000s inductive HPow (#46); 0.000s inductive List (#15); 0.000s inductive PProd (#16); 0.000s inductive HAdd (#26)
con-leche: stats: check pool: 0.000s wall, 4 workers, 42 records, busy 0.001s (57.8%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (27.5%)
con-leche: stats: slowest checks: 0.000s definition List.brecOn.go (#18); 0.000s definition List.foldr._f (#23); 0.000s definition Nat.brecOn.go (#32); 0.000s definition List.below (#17); 0.000s definition List.casesOn (#20)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/proj-lazy-struct"

Expected: 👍 accept · Size: 44.9 KB · Lines: 808 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(P (slow 100000)).1      and      (Q (slow 100001)).1

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 39.6 M · max rss memory: 23.1 MB

stdout:

con-leche: accepted 31 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 40 records, busy 0.002s (23.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.0%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s def Nat.add (#32); 0.000s inductive HAdd (#25); 0.000s inductive Add (#27)
con-leche: stats: check pool: 0.000s wall, 4 workers, 22 records, busy 0.001s (51.8%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (31.2%)
con-leche: stats: slowest checks: 0.000s definition Nat.brecOn.go (#20); 0.000s definition Prod.fst (#12); 0.000s definition instOfNatNat (#15); 0.000s definition P (#16); 0.000s definition OfNat.ofNat (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/proj-stuck-struct"

Expected: 👍 accept · Size: 50.1 KB · Lines: 916 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 41.4 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 34 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 43 records, busy 0.001s (25.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.7%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive HAdd (#24); 0.000s def Nat.add (#31); 0.000s inductive Bool (#10)
con-leche: stats: check pool: 0.000s wall, 4 workers, 25 records, busy 0.001s (51.8%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (30.3%)
con-leche: stats: slowest checks: 0.000s definition step._f (#36); 0.000s definition Nat.brecOn.go (#16); 0.000s definition Nat.casesOn (#21); 0.000s definition step.match_3 (#22); 0.000s definition step.match_1 (#35)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/refute-cheap-first"

Expected: ✋ reject · Size: 20.7 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(false, count #n) = (true, count #(n+1))

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 29.2 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 16 records, busy 0.001s (34.0%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (31.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Prod (#11); 0.000s inductive Bool (#10); 0.000s inductive N (#12); 0.000s theorem kernel_refute_cheap_first (#15)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (29.9%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (46.8%)
con-leche: stats: slowest checks: 0.000s theorem kernel_refute_cheap_first (#15); 0.000s definition N.add (#13); 0.000s definition count (#14)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem kernel_refute_cheap_first [at theorem kernel_refute_cheap_first, fold position 15] (--verified) t=0.0s

Test "perf/refute-cheap-last"

Expected: ✋ reject · Size: 20.5 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

(count #n, false) = (count #(n+1), true)

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 98.6 M · max rss memory: 23.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 16 records, busy 0.001s (27.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.0%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Bool (#10); 0.000s theorem kernel_refute_cheap_last (#15)
con-leche: stats: check pool: 0.005s wall, 3 workers, 3 records, busy 0.004s (32.5%); tail 0.004s after the last start, 2 busy then, 0.004s worker-time in it (33.2%)
con-leche: stats: slowest checks: 0.004s theorem kernel_refute_cheap_last (#15); 0.000s definition N.add (#13); 0.000s definition count (#14)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem kernel_refute_cheap_last [at theorem kernel_refute_cheap_last, fold position 15] (--verified) t=0.0s

Test "perf/repeated-subproblem"

Expected: 👍 accept · Size: 11.4 KB · Lines: 214 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

perfect #n leaf      and      perfect #(n-1) (node leaf leaf)

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 26.9 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (15.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Tr (#11); 0.000s inductive Bool (#10); 0.000s inductive N (#12); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (49.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (62.6%)
con-leche: stats: slowest checks: 0.000s theorem kernel_repeated_subproblem (#14); 0.000s definition perfect (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/shared-subterm"

Expected: 👍 accept · Size: 50.1 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

ldepth (perfect #n leaf)      and      ldepth2 (perfect #n leaf)

Test result: 👍 accepted · exit code 0 · wall time: 30 ms · instructions: 235.1 M · max rss memory: 28.8 MB

stdout:

con-leche: accepted 8 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 18 records, busy 0.001s (25.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.7%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive Tr (#12); 0.000s theorem kernel_shared_subterm (#17); 0.000s inductive Bool (#10)
con-leche: stats: check pool: 0.017s wall, 4 workers, 5 records, busy 0.017s (24.8%); tail 0.017s after the last start, 4 busy then, 0.017s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.017s theorem kernel_shared_subterm (#17); 0.000s definition ldepth (#13); 0.000s definition N.add (#15); 0.000s definition perfect (#14); 0.000s definition ldepth2 (#16)
con-leche: stats: peak RSS 0.02 GiB

Test "perf/shift-cascade"

Expected: 👍 accept · Size: 256.3 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 19 ms · instructions: 76.4 M · max rss memory: 33.2 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.001s (29.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (26.2%)
con-leche: stats: slowest installs: 0.000s inductive OfNat (#11); 0.000s inductive And (#9); 0.000s def shift_cascade (#14); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.002s wall, 3 workers, 3 records, busy 0.002s (31.9%); tail 0.002s after the last start, 3 busy then, 0.002s worker-time in it (33.7%)
con-leche: stats: slowest checks: 0.002s definition shift_cascade (#14); 0.000s definition instOfNatNat (#13); 0.000s definition OfNat.ofNat (#12)
con-leche: stats: peak RSS 0.03 GiB

Test "perf/unroll-versus-evaluate"

Expected: 👍 accept · Size: 44.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

count #(n+1)      and      N.add (count #n) #1

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 44.6 M · max rss memory: 23.7 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.001s (30.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (27.6%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s theorem kernel_unroll_versus_evaluate (#14); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.001s (34.7%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (38.3%)
con-leche: stats: slowest checks: 0.000s theorem kernel_unroll_versus_evaluate (#14); 0.000s definition N.add (#12); 0.000s definition count (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "std"

Expected: 👍 accept · Size: 569.0 MB · Lines: 10.8 M · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 20.8 s · instructions: 674.9 G · max rss memory: 696.8 MB

stdout:

con-leche: accepted 101286 declarations (--verified)

stderr:

con-leche: stats: phases: parse 1.2s, install 1.5s, check 17.9s
con-leche: stats: install pool: 1.341s wall, 4 workers + the commit thread, 101286 records, busy 6.139s (91.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.4%)
con-leche: stats: slowest installs: 0.824s def String.instInhabited (#1254); 0.821s theorem Int.ofNat_mul_negOfNat (#1410); 0.821s theorem List.zipWith.eq_2 (#1280); 0.820s theorem Int.sub_add_cancel (#1344); 0.429s def Nat.xor (#850)
con-leche: stats: check pool: 17.930s wall, 4 workers, 100201 records, busy 71.476s (99.6%); tail 0.070s after the last start, 4 busy then, 0.070s worker-time in it (24.9%)
con-leche: stats: slowest checks: 0.431s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_append._proof_1 (#89871); 0.410s theorem _private.Init.Data.Array.Extract.0.Array.extract_append._proof_1_1 (#7447); 0.368s theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache._mutual.eq_def (#21861); 0.298s theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual (#22986); 0.284s theorem _private.Init.Data.Vector.Extract.0.Vector.extract_extract._proof_1 (#68804)
con-leche: stats: peak RSS 0.68 GiB

Test "tutorial/001_basicDef"

Expected: 👍 accept · Size: 367 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.6 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (18.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (32.6%)
con-leche: stats: slowest checks: 0.000s definition basicDef (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/002_badDef"

Expected: ✋ reject · Size: 365 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 18 ms · instructions: 22.6 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (16.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (3.6%)
con-leche: stats: slowest checks: 0.000s definition badDef (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition badDef [at def badDef, fold position 11] (--verified) t=0.0s

Test "tutorial/003_arrowType"

Expected: 👍 accept · Size: 622 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 22.7 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s def arrowType (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (31.1%)
con-leche: stats: slowest checks: 0.000s definition arrowType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/004_dependentType"

Expected: 👍 accept · Size: 460 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.7 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (16.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def dependentType (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (14.5%)
con-leche: stats: slowest checks: 0.000s definition dependentType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/005_constType"

Expected: 👍 accept · Size: 897 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 22.7 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (12.3%)
con-leche: stats: slowest checks: 0.000s definition constType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/006_betaReduction"

Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 22.8 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (21.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (36.4%)
con-leche: stats: slowest checks: 0.000s definition betaReduction (#12); 0.000s definition constType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/007_betaReduction2"

Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.8 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (8.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (26.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (43.7%)
con-leche: stats: slowest checks: 0.000s definition betaReduction2 (#12); 0.000s definition constType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/008_forallSortWhnf"

Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.9 M · max rss memory: 20.7 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def id (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (27.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (54.5%)
con-leche: stats: slowest checks: 0.000s definition forallSortWhnf (#12); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/009_forallSortBad"

Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 22.9 M · max rss memory: 20.6 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (17.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (15.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (42.7%)
con-leche: stats: slowest checks: 0.000s definition forallSortBad (#12); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at def forallSortBad, fold position 12] (--verified) t=0.0s

Test "tutorial/010_nonTypeType"

Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 22.8 M · max rss memory: 23.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s def constType (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (14.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (56.9%)
con-leche: stats: slowest checks: 0.000s definition constType (#11); 0.000s definition nonTypeType (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at def nonTypeType, fold position 12] (--verified) t=0.0s

Test "tutorial/011_nonTypeAxiom"

Expected: ✋ reject · Size: 1.0 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 20.7 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 9 records, busy 0.000s (1.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s axiom Quot.sound (#8)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at axiom nonTypeAxiom, fold position 12] (--verified) t=0.0s

Test "tutorial/012_nonPropThm"

Expected: ✋ reject · Size: 424 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (15.1%)
con-leche: stats: slowest checks: 0.000s theorem nonPropThm (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type of theorem nonPropThm is not a proposition [at theorem nonPropThm, fold position 11] (--verified) t=0.0s

Test "tutorial/013_thmProof"

Expected: 👍 accept · Size: 1.3 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 22.9 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s theorem pImpliesP (#11); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (24.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (45.6%)
con-leche: stats: slowest checks: 0.000s theorem thmProof (#12); 0.000s theorem pImpliesP (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/014_selfProof"

Expected: ✋ reject · Size: 459 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 22.6 M · max rss memory: 20.7 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (26.1%)
con-leche: stats: slowest checks: 0.000s theorem selfProof (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: unknown constant in value of selfProof [at theorem selfProof, fold position 11] (--verified) t=0.0s

Test "tutorial/015_levelComp1"

Expected: 👍 accept · Size: 391 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.6 M · max rss memory: 20.7 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (18.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s def levelComp1 (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (31.7%)
con-leche: stats: slowest checks: 0.000s definition levelComp1 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/016_levelComp2"

Expected: 👍 accept · Size: 409 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 22.6 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (24.2%)
con-leche: stats: slowest checks: 0.000s definition levelComp2 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/017_levelComp3"

Expected: 👍 accept · Size: 427 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.7 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (17.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s def levelComp3 (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (27.7%)
con-leche: stats: slowest checks: 0.000s definition levelComp3 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/018_levelParams"

Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.9 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def levelParamF (#11); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (20.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (43.3%)
con-leche: stats: slowest checks: 0.000s definition levelParams (#12); 0.000s definition levelParamF (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/019_tut06_bad01"

Expected: ✋ reject · Size: 427 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 22.5 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 10 records, busy 0.000s (8.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate universe parameters in tut06_bad01 [at def tut06_bad01, fold position 11] (--verified) t=0.0s

Test "tutorial/020_levelComp4"

Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.6 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (19.8%)
con-leche: stats: slowest checks: 0.000s definition levelComp4 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/021_levelComp5"

Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (18.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.2%)
con-leche: stats: slowest checks: 0.000s definition levelComp5 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/022_imax1"

Expected: 👍 accept · Size: 809 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.7 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (18.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s def imax1 (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (22.6%)
con-leche: stats: slowest checks: 0.000s definition imax1 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/023_imax2"

Expected: 👍 accept · Size: 828 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.7 M · max rss memory: 20.6 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s def imax2 (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (31.5%)
con-leche: stats: slowest checks: 0.000s definition imax2 (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/024_levelMaxComm"

Expected: 👍 accept · Size: 524 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 20.7 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (32.3%)
con-leche: stats: slowest checks: 0.000s definition levelMaxComm (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/025_levelMaxAssoc"

Expected: 👍 accept · Size: 623 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (21.5%)
con-leche: stats: slowest checks: 0.000s definition levelMaxAssoc (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/026_levelMaxIdem"

Expected: 👍 accept · Size: 447 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.7 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (24.4%)
con-leche: stats: slowest checks: 0.000s definition levelMaxIdem (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/027_levelMaxAbsorb"

Expected: 👍 accept · Size: 526 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 34 ms · instructions: 22.7 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def levelMaxAbsorb (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (33.0%)
con-leche: stats: slowest checks: 0.000s definition levelMaxAbsorb (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/028_inferVar"

Expected: 👍 accept · Size: 713 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.7 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def inferVar (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (22.6%)
con-leche: stats: slowest checks: 0.000s definition inferVar (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/029_defEqLambda"

Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 22.8 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (16.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (27.4%)
con-leche: stats: slowest checks: 0.000s definition defEqLambda (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/030_peano1"

Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.7 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 18 records, busy 0.000s (17.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 4 workers, 7 records, busy 0.000s (23.4%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (22.8%)
con-leche: stats: slowest checks: 0.000s definition PN.succ (#12); 0.000s definition PN (#11); 0.000s definition PN.zero (#13); 0.000s theorem peano1 (#17); 0.000s definition PN.lit0 (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/031_peano2"

Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 24.2 M · max rss memory: 23.1 MB

stdout:

con-leche: accepted 8 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 19 records, busy 0.000s (18.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 4 workers, 8 records, busy 0.000s (29.7%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (41.6%)
con-leche: stats: slowest checks: 0.000s theorem peano2 (#18); 0.000s definition PN.zero (#13); 0.000s definition PN.succ (#12); 0.000s definition PN (#11); 0.000s definition PN.lit2 (#16)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/032_peano3"

Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 24.7 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 10 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 21 records, busy 0.000s (18.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def PN (#11); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 4 workers, 10 records, busy 0.000s (26.4%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (27.9%)
con-leche: stats: slowest checks: 0.000s theorem peano3 (#20); 0.000s definition PN.succ (#12); 0.000s definition PN (#11); 0.000s definition PN.zero (#13); 0.000s definition PN.mul (#19)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/033_letType"

Expected: 👍 accept · Size: 489 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (18.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def letType (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (15.2%)
con-leche: stats: slowest checks: 0.000s definition letType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/034_letTypeDep"

Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 12 ms · instructions: 22.7 M · max rss memory: 20.5 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 10 records, busy 0.000s (3.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s axiom aDepProp (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s axiom mkADepProp (#12); 0.000s quot Quot (#4)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aDepProp) [at axiom aDepProp, fold position 11] (--verified) t=0.0s

Test "tutorial/035_letRed"

Expected: 👍 accept · Size: 627 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 11 ms · instructions: 22.6 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 2 records, busy 0.000s (0.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.2%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s quot Quot.lift (#6)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aProp) [at axiom aProp, fold position 11] (--verified) t=0.0s

Test "tutorial/036_empty"

Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.7 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (20.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def empty (#11); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (9.3%)
con-leche: stats: slowest checks: 0.000s definition empty (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/037_boolType"

Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 22.8 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 10 records, busy 0.000s (18.6%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (20.3%)
con-leche: stats: slowest installs: 0.000s def boolType (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s quot Quot.ind (#7); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.7%)
con-leche: stats: slowest checks: 0.000s definition boolType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/038_twoBool"

Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.6 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (30.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.8%)
con-leche: stats: slowest installs: 0.000s inductive TwoBool (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.9%)
con-leche: stats: slowest checks: 0.000s definition twoBool (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/039_andType"

Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 22.9 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (29.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s def andType (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (21.2%)
con-leche: stats: slowest checks: 0.000s definition andType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/040_prodType"

Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.2 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (16.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s quot Quot.lift (#6)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (35.1%)
con-leche: stats: slowest checks: 0.000s definition prodType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/041_pprodType"

Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.1 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (29.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.8%)
con-leche: stats: slowest installs: 0.000s inductive PProd (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (30.5%)
con-leche: stats: slowest checks: 0.000s definition pprodType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/042_pUnitType"

Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.1 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (25.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (21.1%)
con-leche: stats: slowest checks: 0.000s definition pUnitType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/043_eqType"

Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 22.9 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (18.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def eqType (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (26.4%)
con-leche: stats: slowest checks: 0.000s definition eqType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/044_natDef"

Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 23.8 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (27.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.7%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (11.7%)
con-leche: stats: slowest checks: 0.000s definition natDef (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/045_rbTreeDef"

Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 32.9 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (3 still running, not counted): 0.001s wall, 4 workers + the commit thread, 11 records, busy 0.001s (19.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.4%)
con-leche: stats: slowest installs: 0.000s inductive RBTree (#13); 0.000s inductive Color (#11); 0.000s inductive N (#12); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (26.0%)
con-leche: stats: slowest checks: 0.000s definition rbTreeDef (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/046_inductBadNonSort"

Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 15 ms · instructions: 22.7 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (2 still running, not counted): 0.000s wall, 4 workers + the commit thread, 10 records, busy 0.000s (6.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.8%)
con-leche: stats: slowest installs: 0.000s inductive Nat (#1); 0.000s inductive inductBadNonSort (#12); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s def constType (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at inductive inductBadNonSort, fold position 12] (--verified) t=0.0s

Test "tutorial/047_inductBadNonSort2"

Expected: ✋ reject · Size: 598 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 7 records, busy 0.000s (3.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s axiom aType (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive False (#3); 0.000s inductive inductBadNonSort2 (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aType) [at axiom aType, fold position 11] (--verified) t=0.0s

Test "tutorial/048_inductLevelParam"

Expected: ✋ reject · Size: 515 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 22.6 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 3 records, busy 0.000s (1.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate universe parameters in inductLevelParam [at inductive inductLevelParam, fold position 11] (--verified) t=0.0s

Test "tutorial/049_inductTooFewParams"

Expected: ✋ reject · Size: 548 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 22.6 M · max rss memory: 20.9 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 2 records, busy 0.000s (1.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.2%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: number of parameters mismatch [at inductive inductTooFewParams, fold position 11] (--verified) t=0.0s

Test "tutorial/050_inductWrongCtorParams"

Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 19.3 M · max rss memory: 19.8 MB

stderr:

con-leche: invalid: recursor inductWrongCtorParams.rec declares 0 parameters; the block declares 1 (--verified)

Test "tutorial/051_inductWrongCtorResParams"

Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 19.3 M · max rss memory: 20.1 MB

stderr:

con-leche: invalid: recursor inductWrongCtorResParams.rec declares 0 parameters; the block declares 2 (--verified)

Test "tutorial/052_inductWrongCtorResLevel"

Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 19.4 M · max rss memory: 20.1 MB

stderr:

con-leche: invalid: recursor inductWrongCtorResLevel.rec declares 0 parameters; the block declares 2 (--verified)

Test "tutorial/053_inductInIndex"

Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 19.3 M · max rss memory: 18.0 MB

stderr:

con-leche: invalid: recursor inductInIndex.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/054_indNeg"

Expected: ✋ reject · Size: 996 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 19.3 M · max rss memory: 18.1 MB

stderr:

con-leche: invalid: recursor indNeg.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/055_reduceCtorParam.mk"

Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.2 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (18.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive reduceCtorParam (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (13.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.8%)
con-leche: stats: slowest checks: 0.000s definition id (#11); 0.000s definition constType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/056_reduceCtorType.mk"

Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 19.4 M · max rss memory: 17.9 MB

stderr:

con-leche: invalid: recursor reduceCtorType.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/057_indNegReducible"

Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 19.3 M · max rss memory: 18.2 MB

stderr:

con-leche: invalid: recursor indNegReducible.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/058_predWithTypeField"

Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 23.2 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (25.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PredWithTypeField (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.9%)
con-leche: stats: slowest checks: 0.000s definition predWithTypeField (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/059_typeWithTypeField"

Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.3 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (29.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive TypeWithTypeField (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (23.8%)
con-leche: stats: slowest checks: 0.000s definition typeWithTypeField (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/060_typeWithTypeFieldPoly"

Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.3 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (11.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive TypeWithTypeFieldPoly (#11); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (14.8%)
con-leche: stats: slowest checks: 0.000s definition typeWithTypeFieldPoly (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/061_typeWithTooHighTypeField.mk"

Expected: ✋ reject · Size: 943 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 19.3 M · max rss memory: 20.0 MB

stderr:

con-leche: invalid: recursor typeWithTooHighTypeField.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/062_emptyRec"

Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 22.7 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def emptyRec (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.0%)
con-leche: stats: slowest checks: 0.000s definition emptyRec (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/063_boolRec"

Expected: 👍 accept · Size: 3.0 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 22.9 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (35.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (35.6%)
con-leche: stats: slowest installs: 0.000s def boolRec (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (41.0%)
con-leche: stats: slowest checks: 0.000s definition boolRec (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/064_twoBoolRec"

Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 23.8 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (27.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.3%)
con-leche: stats: slowest installs: 0.000s inductive TwoBool (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (49.8%)
con-leche: stats: slowest checks: 0.000s definition twoBoolRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/065_andRec"

Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.0 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (33.0%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (19.2%)
con-leche: stats: slowest installs: 0.000s def andRec (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (39.5%)
con-leche: stats: slowest checks: 0.000s definition andRec (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/066_prodRec"

Expected: 👍 accept · Size: 4.0 KB · Lines: 79 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.3 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (26.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.1%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (41.4%)
con-leche: stats: slowest checks: 0.000s definition prodRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/067_pprodRec"

Expected: 👍 accept · Size: 4.0 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.3 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (30.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (21.0%)
con-leche: stats: slowest installs: 0.000s inductive PProd (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def pprodRec (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (40.7%)
con-leche: stats: slowest checks: 0.000s definition pprodRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/068_punitRec"

Expected: 👍 accept · Size: 2.2 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.3 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (24.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (47.9%)
con-leche: stats: slowest checks: 0.000s definition punitRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/069_eqRec"

Expected: 👍 accept · Size: 3.3 KB · Lines: 63 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 23.1 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (16.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def eqRec (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (55.2%)
con-leche: stats: slowest checks: 0.000s definition eqRec (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/070_nRec"

Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.9 M · max rss memory: 20.8 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (26.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.1%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def nRec (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (4.5%)
con-leche: stats: slowest checks: 0.000s definition nRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/071_rbTreeRef"

Expected: 👍 accept · Size: 16.2 KB · Lines: 303 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 33.7 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.001s (25.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.7%)
con-leche: stats: slowest installs: 0.000s inductive RBTree (#13); 0.000s inductive Color (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Bool (#10)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (61.6%)
con-leche: stats: slowest checks: 0.000s definition rbTreeRef (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/072_boolPropRec"

Expected: 👍 accept · Size: 2.3 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.4 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (27.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.9%)
con-leche: stats: slowest installs: 0.000s inductive BoolProp (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.9%)
con-leche: stats: slowest checks: 0.000s definition boolPropRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/073_BogusRecursor"

Expected: ✋ reject · Size: 1.8 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

inductive BogusRecursor : Type where
  | mk : BogusRecursor

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 19.4 M · max rss memory: 17.9 MB

stderr:

con-leche: invalid: recursor BogusRecursor.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/074_existsRec"

Expected: 👍 accept · Size: 3.6 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 24.4 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (32.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s inductive Exists (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (38.0%)
con-leche: stats: slowest checks: 0.000s definition existsRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/075_typeSingletonRecReduction"

Expected: 👍 accept · Size: 7.9 KB · Lines: 138 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.0 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (26.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (34.2%)
con-leche: stats: slowest installs: 0.000s inductive NewSingleton (#11); 0.000s inductive And (#9); 0.000s def typeSingletonRecReduction (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (35.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (53.4%)
con-leche: stats: slowest checks: 0.000s definition typeSingletonRecReduction (#13); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/076_sortElimPropRec"

Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.5 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (30.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.9%)
con-leche: stats: slowest installs: 0.000s inductive SortElimProp (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive False (#3); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (39.2%)
con-leche: stats: slowest checks: 0.000s definition sortElimPropRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/077_sortElimProp2Rec"

Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.9 M · max rss memory: 20.7 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (28.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.3%)
con-leche: stats: slowest installs: 0.000s inductive SortElimProp2 (#12); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (30.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (42.3%)
con-leche: stats: slowest checks: 0.000s definition sortElimProp2Rec (#13); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/078_boolRecEqns"

Expected: 👍 accept · Size: 10.8 KB · Lines: 199 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.1 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (33.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (37.5%)
con-leche: stats: slowest installs: 0.000s theorem boolRecEqns (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (74.1%)
con-leche: stats: slowest checks: 0.000s theorem boolRecEqns (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/079_prodRecEqns"

Expected: 👍 accept · Size: 10.1 KB · Lines: 205 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 25.3 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (29.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (22.2%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (66.3%)
con-leche: stats: slowest checks: 0.000s theorem prodRecEqns (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/080_nRecReduction"

Expected: 👍 accept · Size: 12.7 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 25.7 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (29.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.9%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (27.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (39.7%)
con-leche: stats: slowest checks: 0.000s theorem nRecReduction (#14); 0.000s definition N.add (#12); 0.000s definition id (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/081_listRecReduction"

Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 27.8 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 16 records, busy 0.001s (34.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.8%)
con-leche: stats: slowest installs: 0.000s def List.recOn (#12); 0.000s inductive And (#9); 0.000s inductive List (#11); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 4 workers, 4 records, busy 0.000s (25.7%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (30.0%)
con-leche: stats: slowest checks: 0.000s theorem listRecReduction (#15); 0.000s definition myListApped (#13); 0.000s definition List.recOn (#12); 0.000s definition id (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/082_RBTree.id_spec"

Expected: 👍 accept · Size: 47.9 KB · Lines: 1.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 43.2 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 17 records, busy 0.001s (25.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.5%)
con-leche: stats: slowest installs: 0.000s inductive RBTree (#13); 0.000s inductive Color (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Bool (#10)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (34.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (39.0%)
con-leche: stats: slowest checks: 0.000s theorem RBTree.id_spec (#16); 0.000s definition RBTree.id (#14); 0.000s definition id (#15)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/083_And.right"

Expected: 👍 accept · Size: 4.3 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 36 ms · instructions: 23.1 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (32.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (18.3%)
con-leche: stats: slowest installs: 0.000s theorem And.left (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (38.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (57.8%)
con-leche: stats: slowest checks: 0.000s theorem And.left (#11); 0.000s theorem And.right (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/084_Prod.snd"

Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.4 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (28.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (34.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (59.3%)
con-leche: stats: slowest checks: 0.000s definition Prod.snd (#13); 0.000s definition Prod.fst (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/085_PProd.snd"

Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.4 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (29.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (17.7%)
con-leche: stats: slowest installs: 0.000s inductive PProd (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot.ind (#7)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (24.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (39.8%)
con-leche: stats: slowest checks: 0.000s definition PProd.snd (#13); 0.000s definition PProd.fst (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/086_PSigma.snd"

Expected: 👍 accept · Size: 5.1 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.9 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (30.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (16.8%)
con-leche: stats: slowest installs: 0.000s inductive PSigma (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def PSigma.fst (#12)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (33.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (55.8%)
con-leche: stats: slowest checks: 0.000s definition PSigma.snd (#13); 0.000s definition PSigma.fst (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/087_projOutOfRange"

Expected: ✋ reject · Size: 3.8 KB · Lines: 67 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 22.9 M · max rss memory: 21.4 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (31.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.9%)
con-leche: stats: slowest installs: 0.000s def projOutOfRange (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (52.6%)
con-leche: stats: slowest checks: 0.000s definition projOutOfRange (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection index out of range [at def projOutOfRange, fold position 11] (--verified) t=0.0s

Test "tutorial/088_projNotStruct"

Expected: ✋ reject · Size: 3.5 KB · Lines: 64 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 23.8 M · max rss memory: 23.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (30.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (18.7%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (32.0%)
con-leche: stats: slowest checks: 0.000s definition projNotStruct (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid projection: not a structure-like type, or no such field [at def projNotStruct, fold position 12] (--verified) t=0.0s

Test "tutorial/089_projProp1"

Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 25.2 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (17.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (8.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive PUnit (#11); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (39.7%)
con-leche: stats: slowest checks: 0.000s definition projProp1 (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/090_projProp2"

Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 25.2 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (28.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.8%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (16.9%)
con-leche: stats: slowest checks: 0.000s definition projProp2 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp2, fold position 13] (--verified) t=0.0s

Test "tutorial/091_projProp3"

Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 25.3 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (28.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.0%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (30.3%)
con-leche: stats: slowest checks: 0.000s definition projProp3 (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/092_projProp4"

Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 25.3 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (30.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (17.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (30.3%)
con-leche: stats: slowest checks: 0.000s definition projProp4 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp4, fold position 13] (--verified) t=0.0s

Test "tutorial/093_projProp5"

Expected: ✋ reject · Size: 8.4 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 25.3 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (32.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (11.2%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (37.9%)
con-leche: stats: slowest checks: 0.000s definition projProp5 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp5, fold position 13] (--verified) t=0.0s

Test "tutorial/094_projProp6"

Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 25.3 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (32.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (13.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (24.6%)
con-leche: stats: slowest checks: 0.000s definition projProp6 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp6, fold position 13] (--verified) t=0.0s

Test "tutorial/095_projDataIndexRec"

Expected: 👍 accept · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 25.3 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.001s (31.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.3%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive ProjDataIndex (#13); 0.000s inductive Bool (#10); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (43.7%)
con-leche: stats: slowest checks: 0.000s definition projDataIndexRec (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/096_projIndexData"

Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 27.8 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (9.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (26.7%)
con-leche: stats: slowest checks: 0.000s definition projIndexData (#16)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid projection: the node names another structure [at def projIndexData, fold position 16] (--verified) t=0.0s

Test "tutorial/097_projIndexData2"

Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 27.7 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 17 records, busy 0.001s (25.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.9%)
con-leche: stats: slowest installs: 0.000s inductive PropStructure (#15); 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive PUnit (#14); 0.000s inductive ProjDataIndex (#13)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (29.6%)
con-leche: stats: slowest checks: 0.000s definition projIndexData2 (#16)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection index out of range [at def projIndexData2, fold position 16] (--verified) t=0.0s

Test "tutorial/098_projRed"

Expected: 👍 accept · Size: 9.9 KB · Lines: 177 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 25.1 M · max rss memory: 23.3 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.001s (33.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (37.9%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def projRed (#14); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (25.1%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (31.5%)
con-leche: stats: slowest checks: 0.000s definition projRed (#14); 0.000s definition Prod.snd (#12); 0.000s definition rfl (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/099_ruleK"

Expected: 👍 accept · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 23.4 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.001s (34.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (33.9%)
con-leche: stats: slowest installs: 0.000s theorem ruleK (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (70.7%)
con-leche: stats: slowest checks: 0.000s theorem ruleK (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/100_ruleKbad"

Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 23.4 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (14.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (12.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (59.4%)
con-leche: stats: slowest checks: 0.000s theorem ruleKbad (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem ruleKbad [at theorem ruleKbad, fold position 11] (--verified) t=0.0s

Test "tutorial/101_ruleKAcc"

Expected: ✋ reject · Size: 12.5 KB · Lines: 229 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 26.9 M · max rss memory: 21.3 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (32.0%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (17.4%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (70.8%)
con-leche: stats: slowest checks: 0.000s theorem ruleKAcc (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem ruleKAcc [at theorem ruleKAcc, fold position 12] (--verified) t=0.0s

Test "tutorial/102_aNatLit"

Expected: 👍 accept · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 22.9 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.000s wall, 4 workers + the commit thread, 10 records, busy 0.000s (4.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (0.2%)
con-leche: stats: slowest installs: 0.000s def aNatLit (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (21.3%)
con-leche: stats: slowest checks: 0.000s definition aNatLit (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/103_natLitEq"

Expected: 👍 accept · Size: 6.1 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.2 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (20.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem natLitEq (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (36.9%)
con-leche: stats: slowest checks: 0.000s theorem natLitEq (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/104_proofIrrelevance"

Expected: 👍 accept · Size: 5.0 KB · Lines: 100 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 23.3 M · max rss memory: 21.3 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def rfl (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (44.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (63.1%)
con-leche: stats: slowest checks: 0.000s definition proofIrrelevance (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/105_proofIrrelevanceBad"

Expected: ✋ reject · Size: 4.7 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 23.3 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (20.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def rfl (#11); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (32.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (56.3%)
con-leche: stats: slowest checks: 0.000s definition proofIrrelevanceBad (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition proofIrrelevanceBad [at def proofIrrelevanceBad, fold position 12] (--verified) t=0.0s

Test "tutorial/106_proofIrrelevanceWhnf"

Expected: 👍 accept · Size: 5.6 KB · Lines: 112 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.5 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (26.9%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (41.6%)
con-leche: stats: slowest checks: 0.000s definition proofIrrelevanceWhnf (#13); 0.000s definition rfl (#12); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/107_proofIrrelevanceUnderBinder"

Expected: 👍 accept · Size: 1.9 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 10 ms · instructions: 22.8 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (2 still running, not counted): 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (19.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (26.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s axiom aPropFamily (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aType) [at axiom aType, fold position 11] (--verified) t=0.0s

Test "tutorial/108_unitEta1"

Expected: 👍 accept · Size: 6.2 KB · Lines: 116 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.8 M · max rss memory: 20.9 MB

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (18.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive PUnit (#11); 0.000s def rfl (#13)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (24.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (43.2%)
con-leche: stats: slowest checks: 0.000s definition unitEta1 (#14); 0.000s definition rfl (#13); 0.000s definition Unit (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/109_unitEta2"

Expected: 👍 accept · Size: 5.9 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 23.8 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (27.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def rfl (#12)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (23.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (40.1%)
con-leche: stats: slowest checks: 0.000s definition unitEta2 (#13); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/110_unitEta3"

Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.7 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.000s (23.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def rfl (#12)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (29.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (41.3%)
con-leche: stats: slowest checks: 0.000s definition unitEta3 (#13); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/111_indexedUnitEta"

Expected: ✋ reject · Size: 7.2 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 23.9 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (31.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.4%)
con-leche: stats: slowest installs: 0.000s inductive IndexedUnit (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (58.4%)
con-leche: stats: slowest checks: 0.000s definition indexedUnitEta (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition indexedUnitEta [at def indexedUnitEta, fold position 12] (--verified) t=0.0s

Test "tutorial/112_structEta"

Expected: 👍 accept · Size: 12.5 KB · Lines: 230 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 25.8 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 16 records, busy 0.000s (17.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Prod (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def Prod.fst (#12)
con-leche: stats: check pool: 0.000s wall, 4 workers, 4 records, busy 0.000s (25.2%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (36.2%)
con-leche: stats: slowest checks: 0.000s definition structEta (#15); 0.000s definition Prod.snd (#13); 0.000s definition Prod.fst (#12); 0.000s definition rfl (#14)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/113_indexedStructEta"

Expected: ✋ reject · Size: 8.5 KB · Lines: 138 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 33 ms · instructions: 24.6 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (28.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.3%)
con-leche: stats: slowest installs: 0.000s inductive IndexedSingleton (#12); 0.000s inductive And (#9); 0.000s inductive True (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (50.8%)
con-leche: stats: slowest checks: 0.000s definition indexedStructEta (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition indexedStructEta [at def indexedStructEta, fold position 13] (--verified) t=0.0s

Test "tutorial/114_funEta"

Expected: 👍 accept · Size: 5.2 KB · Lines: 104 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 23.4 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def rfl (#11); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (26.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (61.8%)
con-leche: stats: slowest checks: 0.000s theorem funEta (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/115_funEtaDep"

Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.4 M · max rss memory: 23.2 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (16.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s def rfl (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (35.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (44.3%)
con-leche: stats: slowest checks: 0.000s theorem funEtaDep (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/116_funEtaBad"

Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 23.3 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s theorem funEtaBad (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (67.5%)
con-leche: stats: slowest checks: 0.000s theorem funEtaBad (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem funEtaBad [at theorem funEtaBad, fold position 11] (--verified) t=0.0s

Test "tutorial/117_reflOccLeft"

Expected: ✋ reject · Size: 3.7 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 19.7 M · max rss memory: 20.1 MB

stderr:

con-leche: invalid: recursor reflOccLeft.rec declares 0 motives; the block has 1 inductive types (--verified)

Test "tutorial/118_reflOccInIndex"

Expected: ✋ reject · Size: 3.9 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 19.7 M · max rss memory: 19.9 MB

stderr:

con-leche: invalid: constructor reflOccInIndex.mk declares 1 fields at 0 parameters; its type has 2 binders (--verified)

Test "tutorial/119_reduceCtorParamRefl.mk"

Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 24.6 M · max rss memory: 23.3 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (30.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (29.9%)
con-leche: stats: slowest installs: 0.000s inductive reduceCtorParamRefl (#13); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (12.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.7%)
con-leche: stats: slowest checks: 0.000s definition id (#11); 0.000s definition constType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/120_reduceCtorParamRefl2.mk"

Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 24.5 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (30.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (20.0%)
con-leche: stats: slowest installs: 0.000s inductive reduceCtorParamRefl2 (#13); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (6.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.0%)
con-leche: stats: slowest checks: 0.000s definition id (#11); 0.000s definition constType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/121_rTreeRec"

Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 24.4 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (29.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.5%)
con-leche: stats: slowest installs: 0.000s inductive RTree (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (37.9%)
con-leche: stats: slowest checks: 0.000s definition rTreeRec (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/122_rtreeRecReduction"

Expected: 👍 accept · Size: 10.7 KB · Lines: 191 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 25.3 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.001s (29.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.4%)
con-leche: stats: slowest installs: 0.000s inductive RTree (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (30.8%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (46.1%)
con-leche: stats: slowest checks: 0.000s theorem rtreeRecReduction (#14); 0.000s definition RTree.left (#12); 0.000s definition rfl (#13)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/123_accRecType"

Expected: 👍 accept · Size: 7.5 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 26.2 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (12.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Acc (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def accRecType (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (54.7%)
con-leche: stats: slowest checks: 0.000s definition accRecType (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/124_accRecReduction"

Expected: 👍 accept · Size: 13.0 KB · Lines: 243 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 27.2 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (34.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (33.5%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem accRecReduction (#12); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (60.3%)
con-leche: stats: slowest checks: 0.000s theorem accRecReduction (#12)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/125_accRecNoEta"

Expected: ✋ reject · Size: 12.7 KB · Lines: 235 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 26.9 M · max rss memory: 21.3 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (31.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (27.9%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem accRecNoEta (#12); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (60.9%)
con-leche: stats: slowest checks: 0.000s theorem accRecNoEta (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem accRecNoEta [at theorem accRecNoEta, fold position 12] (--verified) t=0.0s

Test "tutorial/126_quotMkType"

Expected: 👍 accept · Size: 6.3 KB · Lines: 123 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.2 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (21.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def quotMkType (#11); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (27.0%)
con-leche: stats: slowest checks: 0.000s definition quotMkType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/127_quotIndType"

Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.2 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def quotIndType (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (40.3%)
con-leche: stats: slowest checks: 0.000s definition quotIndType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/128_quotLiftType"

Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 11 ms · instructions: 23.3 M · max rss memory: 21.2 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (20.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def quotLiftType (#11); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (57.3%)
con-leche: stats: slowest checks: 0.000s definition quotLiftType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/129_quotSoundType"

Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 23.3 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def quotSoundType (#11); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (54.6%)
con-leche: stats: slowest checks: 0.000s definition quotSoundType (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/130_quotLiftReduction"

Expected: 👍 accept · Size: 7.8 KB · Lines: 153 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 23.9 M · max rss memory: 21.0 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (20.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem quotLiftReduction (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (67.7%)
con-leche: stats: slowest checks: 0.000s theorem quotLiftReduction (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/131_quotIndReduction"

Expected: 👍 accept · Size: 7.6 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 23.8 M · max rss memory: 21.1 MB

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (21.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s theorem quotIndReduction (#11); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (67.0%)
con-leche: stats: slowest checks: 0.000s theorem quotIndReduction (#11)
con-leche: stats: peak RSS 0.02 GiB

Test "tutorial/132_dup_defs"

Expected: ✋ reject · Size: 475 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 22.6 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 3 records, busy 0.000s (1.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_defs [at def dup_defs, fold position 12] (--verified) t=0.0s

Test "tutorial/133_dup_ind_def"

Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 11 ms · instructions: 22.7 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 7 records, busy 0.000s (3.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot.lift (#6); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_ind_def [at inductive dup_ind_def, fold position 12] (--verified) t=0.0s

Test "tutorial/134_dup_ctor_def"

Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 22.7 M · max rss memory: 21.2 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 7 records, busy 0.000s (1.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Empty (#2); 0.000s inductive False (#3)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_ctor_def.mk [at inductive dup_ctor_def, fold position 12] (--verified) t=0.0s

Test "tutorial/135_dup_rec_def"

Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 22.8 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 7 records, busy 0.000s (1.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Empty (#2); 0.000s axiom Quot.sound (#8)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_rec_def.rec [at inductive dup_rec_def, fold position 12] (--verified) t=0.0s

Test "tutorial/136_misnamed_rec_user"

Expected: ✋ reject · Size: 2.0 KB · Lines: 33 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 10 ms · instructions: 22.9 M · max rss memory: 21.0 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 7 records, busy 0.000s (2.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s axiom Quot.sound (#8)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: target rec: the block's recursor names are not the generated ones (one T.rec per member) [at inductive misnamed_rec, fold position 11] (--verified) t=0.0s

Test "tutorial/137_dup_rec_def2"

Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 22.8 M · max rss memory: 20.8 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 4 records, busy 0.000s (1.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: target rec: the block's recursor names are not the generated ones (one T.rec per member) [at inductive dup_rec_def2, fold position 12] (--verified) t=0.0s

Test "tutorial/138_dup_ctor_rec"

Expected: ✋ reject · Size: 1.5 KB · Lines: 24 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 22.8 M · max rss memory: 21.1 MB

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.000s wall, 4 workers + the commit thread, 3 records, busy 0.000s (1.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive False (#3); 0.000s quot Quot.ind (#7)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_ctor_rec.rec [at inductive dup_ctor_rec, fold position 11] (--verified) t=0.0s

Test "tutorial/139_DupConCon"

Expected: ✋ reject · Size: 2.2 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: ✋ rejected · exit code 1 · wall time: 9 ms · instructions: 19.4 M · max rss memory: 18.1 MB

stderr:

con-leche: invalid: duplicate constructor name in an inductive type's ctors (--verified)

Test "tutorial/140_falseFromUnsafe"

Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 9 ms · instructions: 19.3 M · max rss memory: 20.2 MB

stderr:

con-leche: declined: definition with safety 'unsafe' (--verified)

Test "tutorial/141_falseFromPartial"

Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Test result: 🚫 declined · exit code 2 · wall time: 31 ms · instructions: 19.3 M · max rss memory: 18.2 MB

stderr:

con-leche: declined: definition with safety 'partial' (--verified)