Lean Kernel Arena / lean4cobol

Checker "lean4cobol"

Version: d2e7b79 · 📄 Declaration · 🔗 Source

A GnuCOBOL 3.2 port of lean4lean's executable kernel. Checks NDJSON exports with no wall-clock timeout. Resource limits return decline.

Soundness (rightfully rejected tests)

80 ✅ 0 ❌ 0 🚫

Completeness (rightfully accepted tests)

133 ✅ 0 ❌ 5 🚫

Corner cases (no outcome prescribed)

28 ✅ 2 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 👍 31.8 min (×13) 969.8 MB (-30%)
con-leche 👍 ⌛ 0 ms 0 B
cslib 👍 ⌛ 0 ms 0 B
init 👍 👍 15.2 min (×14) 487.8 MB (-14%)
init-prelude 👍 👍 3.33 s (×9.2) 21.5 MB (÷3.4)
mathlib 👍 🚫 0 ms 0 B
navier-stokes-euler 👍 🚫 20.3 min 1.7 GB
reachability 👍 👍 6.68 min (×17) 2.1 GB (+27%)
std 👍 ⌛ 0 ms 0 B
26 1.09 s 14.7 MB
closure-level-subst ✋ ✋ 2.76 ms 13.4 MB
constlevels ✋ ✋ 9.65 ms 13.8 MB
ctor-num-fields ✋ ✋ 20.3 ms 13.6 MB
eta-ctor-alias ✋ ✋ 4.54 ms 13.8 MB
forged-quot-ind ✋ ✋ 6.35 ms 13.5 MB
k-rec-conv ✋ ✋ 8.27 ms 13.6 MB
large-elim-param ✋ ✋ 3.41 ms 13.5 MB
large-elim-prop-bool ✋ ✋ 12.8 ms 13.8 MB
level-imax-leq ✋ ✋ 3.13 ms 13.6 MB
level-imax-normalization ✋ ✋ 3.18 ms 13.5 MB
loose-bvar-value ✋ ✋ 1.99 ms 13.2 MB
nat-rec-k-lie ✋ ✋ 3.87 ms 13.6 MB
nat-rec-rules ✋ ✋ 4.31 ms 13.7 MB
nested-name-capture ✋ ✋ 15.2 ms 13.8 MB
nested-rec-rule-nfields ✋ ✋ 25.7 ms 13.8 MB
nested-unused-param ✋ ✋ 42.2 ms 13.8 MB
orphan-rec ✋ ✋ 1.66 ms 13.7 MB
pi-closure-context ✋ ✋ 1.81 ms 13.7 MB
proj-non-structure ✋ ✋ 3.14 ms 13.6 MB
proj-of-imax-prop ✋ ✋ 9.59 ms 13.5 MB
proj-of-stuck-prop ✋ ✋ 219 ms 14.7 MB
proj-of-subst-prop ✋ ✋ 221 ms 14.1 MB
rec-k-lie ✋ ✋ 3.37 ms 13.6 MB
rec-missing-ih ✋ ✋ 225 ms 14.7 MB
rec-of-subst-prop ✋ ✋ 233 ms 14.3 MB
unit-rec-rule ✋ ✋ 2.48 ms 13.8 MB
1 1.21 s 14.1 MB
alg-conv-trans-acc 🤷 ✋ 52.7 ms 13.9 MB
alg-conv-trans-acc-left 🤷 👍 52.8 ms 14.1 MB
alg-conv-trans-acc-right 🤷 👍 54.9 ms 14.0 MB
alg-conv-trans-quot 🤷 ✋ 6.38 ms 13.7 MB
alg-conv-trans-quot-left 🤷 ✋ 6.52 ms 13.7 MB
alg-conv-trans-quot-left-def 🤷 👍 7.64 ms 13.8 MB
alg-conv-trans-quot-right 🤷 👍 6.69 ms 13.7 MB
eta-ctor 🤷 ✋ 5.31 ms 13.8 MB
eta-rec-struct 🤷 ✋ 6.21 ms 13.8 MB
eta-rule-k 🤷 ✋ 4.52 ms 13.7 MB
eta-struct-major-and 🤷 ✋ 6.92 ms 13.8 MB
eta-struct-major-and-no-whnf 🤷 🚫 396 ms 13.5 MB
eta-struct-major-no-whnf 🤷 🚫 401 ms 13.8 MB
eta-unit-like-nested 🤷 ✋ 8.80 ms 13.7 MB
eta-unit-like-pi 🤷 ✋ 4.00 ms 13.7 MB
eta-unit-like-proof-field 🤷 ✋ 4.25 ms 13.6 MB
eta-unit-like-struct 🤷 ✋ 4.36 ms 13.5 MB
imax-nested-absorption 🤷 ✋ 1.44 ms 13.3 MB
imax-right-successor 🤷 ✋ 1.48 ms 13.2 MB
large-elim-maybe-prop 🤷 ✋ 2.58 ms 13.5 MB
let-value-type-mismatch 🤷 ✋ 1.37 ms 13.4 MB
nested-nonuniform-param 🤷 👍 6.23 ms 13.4 MB
nested-redex-aux 🤷 👍 35.2 ms 14.0 MB
positivity-whnf 🤷 ✋ 2.96 ms 13.4 MB
proj-maybe-prop 🤷 ✋ 5.01 ms 13.5 MB
proj-maybe-prop-past 🤷 ✋ 5.01 ms 13.7 MB
proof-param-ok 👍 👍 2.70 ms 13.5 MB
proof-param-swap 🤷 ✋ 2.35 ms 13.3 MB
subject-reduction-redex 🤷 👍 55.1 ms 13.9 MB
subject-reduction-reduct 🤷 ✋ 52.8 ms 14.0 MB
vanishing-occurrence 🤷 👍 4.20 ms 13.5 MB
10 88.7 ms 13.9 MB
extra-rec ✋ ✋ 1.66 ms 13.5 MB
inductive-undeclared-universe ✋ ✋ 1.96 ms 13.7 MB
level-index-out-of-order 👍 👍 1.25 ms 13.2 MB
nat-lit-add 👍 👍 18.2 ms 13.8 MB
nat-lit-add-bad ✋ ✋ 17.9 ms 13.7 MB
nat-lit-ble 👍 👍 20.7 ms 13.8 MB
nat-lit-sub 👍 👍 21.4 ms 13.9 MB
orphan-ctor ✋ ✋ 1.67 ms 13.4 MB
proj-of-prop ✋ ✋ 2.70 ms 13.5 MB
sparse-name-index 👍 👍 1.23 ms 13.4 MB
31 23.0 min (×17) 8.1 GB
app-lam 👍 👍 1.73 min (×21) 3.0 GB (×2.2)
args-before-unfold 👍 👍 118 ms (×3.3) 21.1 MB (÷3.1)
beta-ladder 👍 👍 30.9 s (×18) 796.9 MB (+59%)
church-numerals 👍 👍 428 ms (×9.1) 113.6 MB (+45%)
discarded-argument 👍 👍 3.80 s (×23) 16.6 MB (÷4.0)
discarded-argument-match 👍 👍 14.5 s (×102) 18.1 MB (÷3.7)
folded-constant-first 👍 👍 182 ms (×4.5) 27.9 MB (÷2.5)
folded-constant-last 👍 👍 182 ms (×4.5) 27.6 MB (÷2.5)
fueled-chain 👍 👍 1.02 s (×8.1) 19.6 MB (÷3.9)
grind-ring-5 👍 👍 31.1 s (×14) 194.1 MB (-15%)
identical-nesting 👍 👍 5.41 ms (÷5.2) 13.5 MB (÷4.9)
irrelevance-before-evaluation 👍 👍 9.94 ms (÷2.9) 14.2 MB (÷4.6)
irrelevance-refutes 👍 👍 8.30 ms (÷3.4) 13.7 MB (÷4.9)
let-fold 👍 👍 317 ms (×5.5) 14.7 MB (÷4.5)
let-ladder 👍 👍 17.1 s (×17) 420.8 MB (+32%)
magma-list-deep-n21 👍 👍 45.7 s (×17) 364.2 MB (-45%)
magma-list-deep-n36 👍 👍 10.1 min (×17) 5.5 GB (-31%)
magma-list-pair-n21 👍 👍 5.35 min (×17) 8.1 GB (×2.0)
magma-list-pair-n7 👍 👍 29.2 s (×17) 536.1 MB (+26%)
magma-string-n4 👍 👍 49.5 s (×14) 92.6 MB (-24%)
magma-string-pair-n9 👍 👍 2.07 min (×15) 1.1 GB (+8%)
proj-cheap-struct 👍 👍 61.1 ms (+76%) 14.2 MB (÷4.6)
proj-lazy-struct 👍 👍 30.1 ms (-4%) 13.8 MB (÷4.8)
proj-stuck-struct 👍 👍 34.0 ms (+7%) 13.9 MB (÷4.7)
prop-struct-projections 👍 👍 1.74 s (×18) 21.0 MB (÷3.3)
refute-cheap-first ✋ ✋ 11.8 ms (÷3.6) 14.4 MB (÷4.8)
refute-cheap-last ✋ ✋ 3.89 s (×22) 16.6 MB (÷4.2)
repeated-subproblem 👍 👍 9.65 ms (÷3.0) 13.9 MB (÷4.7)
shared-subterm 👍 👍 454 ms (×7.9) 30.9 MB (÷2.4)
shift-cascade 👍 👍 143 ms (×3.1) 16.9 MB (÷4.0)
unroll-versus-evaluate 👍 👍 24.6 ms (-21%) 17.2 MB (÷3.9)
141 519 ms 14.1 MB
001_basicDef 👍 👍 1.27 ms 13.3 MB
002_badDef ✋ ✋ 1.27 ms 13.4 MB
003_arrowType 👍 👍 1.38 ms 13.3 MB
004_dependentType 👍 👍 1.31 ms 13.4 MB
005_constType 👍 👍 1.48 ms 13.5 MB
006_betaReduction 👍 👍 1.71 ms 13.6 MB
007_betaReduction2 👍 👍 1.75 ms 13.6 MB
008_forallSortWhnf 👍 👍 1.69 ms 13.3 MB
009_forallSortBad ✋ ✋ 1.70 ms 13.6 MB
010_nonTypeType ✋ ✋ 1.56 ms 13.3 MB
011_nonTypeAxiom ✋ ✋ 1.55 ms 13.2 MB
012_nonPropThm ✋ ✋ 1.29 ms 13.3 MB
013_thmProof 👍 👍 1.73 ms 13.5 MB
014_selfProof ✋ ✋ 1.31 ms 13.4 MB
015_levelComp1 👍 👍 1.29 ms 13.1 MB
016_levelComp2 👍 👍 1.30 ms 13.2 MB
017_levelComp3 👍 👍 1.31 ms 13.3 MB
018_levelParams 👍 👍 1.77 ms 13.5 MB
019_tut06_bad01 ✋ ✋ 1.29 ms 13.3 MB
020_levelComp4 👍 👍 1.30 ms 13.1 MB
021_levelComp5 👍 👍 1.30 ms 13.3 MB
022_imax1 👍 👍 1.46 ms 13.4 MB
023_imax2 👍 👍 1.47 ms 13.3 MB
024_levelMaxComm 👍 👍 1.37 ms 13.4 MB
025_levelMaxAssoc 👍 👍 1.43 ms 13.2 MB
026_levelMaxIdem 👍 👍 1.32 ms 13.2 MB
027_levelMaxAbsorb 👍 👍 1.37 ms 13.2 MB
028_inferVar 👍 👍 1.42 ms 13.4 MB
029_defEqLambda 👍 👍 1.75 ms 13.5 MB
030_peano1 👍 👍 3.01 ms 13.7 MB
031_peano2 👍 👍 3.99 ms 13.4 MB
032_peano3 👍 👍 4.57 ms 13.4 MB
033_letType 👍 👍 1.33 ms 13.6 MB
034_letTypeDep 👍 👍 1.68 ms 13.5 MB
035_letRed 👍 👍 1.40 ms 13.6 MB
036_empty 👍 👍 1.61 ms 13.5 MB
037_boolType 👍 👍 2.08 ms 13.6 MB
038_twoBool 👍 👍 2.84 ms 13.5 MB
039_andType 👍 👍 2.83 ms 13.4 MB
040_prodType 👍 👍 3.14 ms 13.7 MB
041_pprodType 👍 👍 3.12 ms 13.4 MB
042_pUnitType 👍 👍 1.89 ms 13.7 MB
043_eqType 👍 👍 2.85 ms 13.5 MB
044_natDef 👍 👍 2.61 ms 13.7 MB
045_rbTreeDef 👍 👍 12.1 ms 13.7 MB
046_inductBadNonSort ✋ ✋ 1.61 ms 13.6 MB
047_inductBadNonSort2 ✋ ✋ 1.37 ms 13.7 MB
048_inductLevelParam ✋ ✋ 1.31 ms 13.3 MB
049_inductTooFewParams ✋ ✋ 1.31 ms 13.3 MB
050_inductWrongCtorParams ✋ ✋ 1.61 ms 13.6 MB
051_inductWrongCtorResParams ✋ ✋ 1.71 ms 13.6 MB
052_inductWrongCtorResLevel ✋ ✋ 1.78 ms 13.6 MB
053_inductInIndex ✋ ✋ 1.57 ms 13.6 MB
054_indNeg ✋ ✋ 1.51 ms 13.3 MB
055_reduceCtorParam.mk 👍 👍 3.21 ms 13.6 MB
056_reduceCtorType.mk ✋ ✋ 1.77 ms 13.5 MB
057_indNegReducible ✋ ✋ 1.90 ms 13.6 MB
058_predWithTypeField 👍 👍 1.96 ms 13.4 MB
059_typeWithTypeField 👍 👍 2.00 ms 13.7 MB
060_typeWithTypeFieldPoly 👍 👍 2.08 ms 13.6 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 1.50 ms 13.7 MB
062_emptyRec 👍 👍 1.68 ms 13.6 MB
063_boolRec 👍 👍 2.55 ms 13.7 MB
064_twoBoolRec 👍 👍 3.29 ms 13.4 MB
065_andRec 👍 👍 3.03 ms 13.5 MB
066_prodRec 👍 👍 3.48 ms 13.6 MB
067_pprodRec 👍 👍 3.47 ms 13.6 MB
068_punitRec 👍 👍 2.12 ms 13.6 MB
069_eqRec 👍 👍 3.12 ms 13.4 MB
070_nRec 👍 👍 2.72 ms 13.8 MB
071_rbTreeRef 👍 👍 13.5 ms 14.0 MB
072_boolPropRec 👍 👍 2.11 ms 13.7 MB
073_BogusRecursor ✋ ✋ 1.90 ms 13.6 MB
074_existsRec 👍 👍 3.43 ms 13.4 MB
075_typeSingletonRecReduction 👍 👍 5.02 ms 13.7 MB
076_sortElimPropRec 👍 👍 4.05 ms 13.4 MB
077_sortElimProp2Rec 👍 👍 4.67 ms 13.8 MB
078_boolRecEqns 👍 👍 7.36 ms 13.5 MB
079_prodRecEqns 👍 👍 7.51 ms 13.9 MB
080_nRecReduction 👍 👍 8.45 ms 13.6 MB
081_listRecReduction 👍 👍 13.5 ms 13.7 MB
082_RBTree.id_spec 👍 👍 42.8 ms 14.1 MB
083_And.right 👍 👍 3.44 ms 13.7 MB
084_Prod.snd 👍 👍 3.76 ms 13.7 MB
085_PProd.snd 👍 👍 3.75 ms 13.4 MB
086_PSigma.snd 👍 👍 4.44 ms 13.7 MB
087_projOutOfRange ✋ ✋ 3.13 ms 13.5 MB
088_projNotStruct ✋ ✋ 2.68 ms 13.5 MB
089_projProp1 👍 👍 5.32 ms 13.6 MB
090_projProp2 ✋ ✋ 5.32 ms 13.4 MB
091_projProp3 👍 👍 5.32 ms 13.5 MB
092_projProp4 ✋ ✋ 5.32 ms 13.4 MB
093_projProp5 ✋ ✋ 5.41 ms 13.5 MB
094_projProp6 ✋ ✋ 5.32 ms 13.6 MB
095_projDataIndexRec 👍 👍 4.16 ms 13.6 MB
096_projIndexData ✋ ✋ 7.73 ms 13.5 MB
097_projIndexData2 ✋ ✋ 7.73 ms 13.5 MB
098_projRed 👍 👍 6.46 ms 13.7 MB
099_ruleK 👍 👍 4.58 ms 13.6 MB
100_ruleKbad ✋ ✋ 4.64 ms 13.8 MB
101_ruleKAcc ✋ ✋ 9.01 ms 13.9 MB
102_aNatLit 👍 👍 2.47 ms 13.6 MB
103_natLitEq 👍 👍 4.24 ms 13.6 MB
104_proofIrrelevance 👍 👍 3.85 ms 13.5 MB
105_proofIrrelevanceBad ✋ ✋ 3.73 ms 13.6 MB
106_proofIrrelevanceWhnf 👍 👍 4.18 ms 13.5 MB
107_proofIrrelevanceUnderBinder 👍 👍 2.01 ms 13.5 MB
108_unitEta1 👍 👍 4.31 ms 13.4 MB
109_unitEta2 👍 👍 4.21 ms 13.6 MB
110_unitEta3 👍 👍 4.21 ms 13.8 MB
111_indexedUnitEta ✋ ✋ 4.55 ms 13.6 MB
112_structEta 👍 👍 9.00 ms 13.9 MB
113_indexedStructEta ✋ ✋ 5.07 ms 13.5 MB
114_funEta 👍 👍 4.03 ms 13.6 MB
115_funEtaDep 👍 👍 4.15 ms 13.6 MB
116_funEtaBad ✋ ✋ 3.84 ms 13.7 MB
117_reflOccLeft ✋ ✋ 2.72 ms 13.7 MB
118_reflOccInIndex ✋ ✋ 2.84 ms 13.6 MB
119_reduceCtorParamRefl.mk 👍 👍 3.46 ms 13.6 MB
120_reduceCtorParamRefl2.mk 👍 👍 3.48 ms 13.6 MB
121_rTreeRec 👍 👍 3.64 ms 13.6 MB
122_rtreeRecReduction 👍 👍 6.70 ms 13.6 MB
123_accRecType 👍 👍 6.21 ms 13.5 MB
124_accRecReduction 👍 👍 10.7 ms 13.9 MB
125_accRecNoEta ✋ ✋ 9.05 ms 13.8 MB
126_quotMkType 👍 👍 4.38 ms 13.7 MB
127_quotIndType 👍 👍 4.55 ms 13.7 MB
128_quotLiftType 👍 👍 4.58 ms 13.7 MB
129_quotSoundType 👍 👍 5.07 ms 13.6 MB
130_quotLiftReduction 👍 👍 6.15 ms 13.8 MB
131_quotIndReduction 👍 👍 5.92 ms 13.7 MB
132_dup_defs ✋ ✋ 1.27 ms 12.9 MB
133_dup_ind_def ✋ ✋ 1.62 ms 13.1 MB
134_dup_ctor_def ✋ ✋ 1.63 ms 13.2 MB
135_dup_rec_def ✋ ✋ 1.64 ms 12.9 MB
136_misnamed_rec_user ✋ ✋ 1.97 ms 13.6 MB
137_dup_rec_def2 ✋ ✋ 1.83 ms 13.6 MB
138_dup_ctor_rec ✋ ✋ 1.59 ms 13.1 MB
139_DupConCon ✋ ✋ 1.79 ms 13.1 MB
140_falseFromUnsafe ✋ ✋ 1.66 ms 13.8 MB
141_falseFromPartial ✋ ✋ 1.66 ms 13.4 MB