Lean Kernel Arena / overfull

Checker "overfull"

Version: b275736 · 📄 Declaration · 🔗 Source

A Lean kernel checker in plain TeX. Some inputs overfill it.

Soundness (rightfully rejected tests)

73 ✅ 0 ❌ 7 🚫

Completeness (rightfully accepted tests)

103 ✅ 0 ❌ 35 🚫

Corner cases (no outcome prescribed)

22 ✅ 8 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 ⌛ 0 ms 0 B
con-leche 👍 ⌛ 0 ms 0 B
cslib 👍 ⌛ 0 ms 0 B
init 👍 ⌛ 0 ms 0 B
init-prelude 👍 ⌛ 0 ms 0 B
mathlib 👍 ⌛ 0 ms 0 B
navier-stokes-euler 👍 ⌛ 0 ms 0 B
reachability 👍 ⌛ 0 ms 0 B
std 👍 ⌛ 0 ms 0 B
20 7.93 min 48.7 MB
closure-level-subst ✋ ✋ 7.38 s 45.9 MB
constlevels ✋ ✋ 42.6 s 47.3 MB
ctor-num-fields ✋ ✋ 83.4 s 48.7 MB
eta-ctor-alias ✋ ✋ 15.5 s 46.1 MB
forged-quot-ind ✋ ✋ 25.6 s 46.7 MB
k-rec-conv ✋ ✋ 34.4 s 47.0 MB
large-elim-param ✋ ✋ 9.99 s 46.0 MB
large-elim-prop-bool ✋ ✋ 65.3 s 48.3 MB
level-imax-leq ✋ ✋ 9.62 s 46.0 MB
level-imax-normalization ✋ ✋ 10.7 s 45.9 MB
loose-bvar-value ✋ ✋ 4.66 s 45.7 MB
nat-rec-k-lie ✋ ✋ 11.4 s 46.1 MB
nat-rec-rules ✋ ✋ 14.3 s 46.0 MB
nested-name-capture ✋ ✋ 67.1 s 48.1 MB
nested-rec-rule-nfields ✋ ⌛ 0 ms 0 B
nested-unused-param ✋ ⌛ 0 ms 0 B
orphan-rec ✋ ✋ 2.27 s 45.7 MB
pi-closure-context ✋ ✋ 2.94 s 45.6 MB
proj-non-structure ✋ ✋ 9.31 s 46.1 MB
proj-of-imax-prop ✋ ✋ 45.2 s 47.3 MB
proj-of-stuck-prop ✋ ⌛ 0 ms 0 B
proj-of-subst-prop ✋ ⌛ 0 ms 0 B
rec-k-lie ✋ ✋ 9.13 s 45.7 MB
rec-missing-ih ✋ ⌛ 0 ms 0 B
rec-of-subst-prop ✋ ⌛ 0 ms 0 B
unit-rec-rule ✋ ✋ 5.29 s 45.8 MB
1 6.28 min 47.2 MB
alg-conv-trans-acc 🤷 ⌛ 0 ms 0 B
alg-conv-trans-acc-left 🤷 ⌛ 0 ms 0 B
alg-conv-trans-acc-right 🤷 ⌛ 0 ms 0 B
alg-conv-trans-quot 🤷 ✋ 24.8 s 46.7 MB
alg-conv-trans-quot-left 🤷 ✋ 25.7 s 47.0 MB
alg-conv-trans-quot-left-def 🤷 👍 32.0 s 46.9 MB
alg-conv-trans-quot-right 🤷 👍 26.5 s 46.7 MB
eta-ctor 🤷 ✋ 19.5 s 46.4 MB
eta-rec-struct 🤷 ✋ 23.5 s 46.6 MB
eta-rule-k 🤷 ✋ 15.6 s 46.3 MB
eta-struct-major-and 🤷 ✋ 27.5 s 46.8 MB
eta-struct-major-and-no-whnf 🤷 ⌛ 0 ms 0 B
eta-struct-major-no-whnf 🤷 ⌛ 0 ms 0 B
eta-unit-like-nested 🤷 ✋ 37.7 s 47.2 MB
eta-unit-like-pi 🤷 ✋ 13.0 s 46.1 MB
eta-unit-like-proof-field 🤷 ✋ 14.2 s 46.2 MB
eta-unit-like-struct 🤷 ✋ 14.7 s 46.2 MB
imax-nested-absorption 🤷 👍 1.68 s 45.6 MB
imax-right-successor 🤷 👍 1.81 s 45.5 MB
large-elim-maybe-prop 🤷 ✋ 5.98 s 45.6 MB
let-value-type-mismatch 🤷 ✋ 1.31 s 45.6 MB
nested-nonuniform-param 🤷 👍 21.3 s 46.3 MB
nested-redex-aux 🤷 ⌛ 0 ms 0 B
positivity-whnf 🤷 ✋ 8.79 s 46.0 MB
proj-maybe-prop 🤷 ✋ 17.4 s 46.3 MB
proj-maybe-prop-past 🤷 ✋ 17.4 s 46.4 MB
proof-param-ok 👍 👍 6.25 s 45.8 MB
proof-param-swap 🤷 ✋ 5.53 s 45.8 MB
subject-reduction-redex 🤷 ⌛ 0 ms 0 B
subject-reduction-reduct 🤷 ⌛ 0 ms 0 B
vanishing-occurrence 🤷 👍 14.5 s 46.1 MB
10 6.88 min 50.0 MB
extra-rec ✋ ✋ 2.29 s 45.7 MB
inductive-undeclared-universe ✋ ✋ 4.23 s 45.6 MB
level-index-out-of-order 👍 👍 878 ms 45.7 MB
nat-lit-add 👍 👍 91.4 s 49.3 MB
nat-lit-add-bad ✋ ✋ 89.5 s 49.3 MB
nat-lit-ble 👍 👍 1.77 min 50.0 MB
nat-lit-sub 👍 👍 1.80 min 49.8 MB
orphan-ctor ✋ ✋ 2.28 s 45.6 MB
proj-of-prop ✋ ✋ 7.07 s 45.9 MB
sparse-name-index 👍 👍 824 ms 45.6 MB
5 3.57 min (×1371) 47.9 MB
app-lam 👍 ⌛ 0 ms 0 B
args-before-unfold 👍 ⌛ 0 ms 0 B
beta-ladder 👍 ⌛ 0 ms 0 B
church-numerals 👍 ⌛ 0 ms 0 B
discarded-argument 👍 ⌛ 0 ms 0 B
discarded-argument-match 👍 ⌛ 0 ms 0 B
folded-constant-first 👍 ⌛ 0 ms 0 B
folded-constant-last 👍 ⌛ 0 ms 0 B
fueled-chain 👍 ⌛ 0 ms 0 B
grind-ring-5 👍 ⌛ 0 ms 0 B
identical-nesting 👍 👍 21.0 s (×744) 46.6 MB (-30%)
irrelevance-before-evaluation 👍 👍 51.8 s (×1793) 47.5 MB (-28%)
irrelevance-refutes 👍 👍 36.1 s (×1264) 46.9 MB (-29%)
let-fold 👍 ⌛ 0 ms 0 B
let-ladder 👍 ⌛ 0 ms 0 B
magma-list-deep-n21 👍 ⌛ 0 ms 0 B
magma-list-deep-n36 👍 ⌛ 0 ms 0 B
magma-list-pair-n21 👍 ⌛ 0 ms 0 B
magma-list-pair-n7 👍 ⌛ 0 ms 0 B
magma-string-n4 👍 ⌛ 0 ms 0 B
magma-string-pair-n9 👍 ⌛ 0 ms 0 B
proj-cheap-struct 👍 ⌛ 0 ms 0 B
proj-lazy-struct 👍 ⌛ 0 ms 0 B
proj-stuck-struct 👍 ⌛ 0 ms 0 B
prop-struct-projections 👍 ⌛ 0 ms 0 B
refute-cheap-first ✋ ✋ 63.5 s (×1517) 47.9 MB (-31%)
refute-cheap-last ✋ ⌛ 0 ms 0 B
repeated-subproblem 👍 👍 41.7 s (×1459) 47.3 MB (-28%)
shared-subterm 👍 ⌛ 0 ms 0 B
shift-cascade 👍 ⌛ 0 ms 0 B
unroll-versus-evaluate 👍 ⌛ 0 ms 0 B
140 24.0 min 47.9 MB
001_basicDef 👍 👍 941 ms 45.6 MB
002_badDef ✋ ✋ 967 ms 45.7 MB
003_arrowType 👍 👍 1.29 s 45.8 MB
004_dependentType 👍 👍 1.05 s 45.7 MB
005_constType 👍 👍 1.68 s 45.6 MB
006_betaReduction 👍 👍 2.56 s 45.8 MB
007_betaReduction2 👍 👍 2.73 s 45.8 MB
008_forallSortWhnf 👍 👍 2.52 s 45.9 MB
009_forallSortBad ✋ ✋ 2.64 s 45.7 MB
010_nonTypeType ✋ ✋ 1.96 s 45.5 MB
011_nonTypeAxiom ✋ ✋ 1.87 s 45.6 MB
012_nonPropThm ✋ ✋ 997 ms 45.7 MB
013_thmProof 👍 👍 2.70 s 45.7 MB
014_selfProof ✋ ✋ 1.09 s 45.7 MB
015_levelComp1 👍 👍 1.00 s 45.7 MB
016_levelComp2 👍 👍 1.04 s 45.6 MB
017_levelComp3 👍 👍 1.09 s 45.6 MB
018_levelParams 👍 👍 2.75 s 45.7 MB
019_tut06_bad01 ✋ ✋ 989 ms 45.7 MB
020_levelComp4 👍 👍 1.03 s 45.5 MB
021_levelComp5 👍 👍 1.05 s 45.5 MB
022_imax1 👍 👍 1.59 s 45.7 MB
023_imax2 👍 👍 1.66 s 45.6 MB
024_levelMaxComm 👍 👍 1.27 s 45.7 MB
025_levelMaxAssoc 👍 👍 1.47 s 45.6 MB
026_levelMaxIdem 👍 👍 1.12 s 45.6 MB
027_levelMaxAbsorb 👍 👍 1.27 s 45.5 MB
028_inferVar 👍 👍 1.49 s 45.5 MB
029_defEqLambda 👍 👍 2.77 s 45.6 MB
030_peano1 👍 👍 8.23 s 45.9 MB
031_peano2 👍 👍 12.9 s 46.0 MB
032_peano3 👍 👍 15.7 s 46.1 MB
033_letType 👍 👍 1.13 s 45.6 MB
034_letTypeDep 👍 👍 2.37 s 45.7 MB
035_letRed 👍 👍 1.34 s 45.6 MB
036_empty 👍 👍 2.14 s 45.5 MB
037_boolType 👍 👍 4.16 s 45.7 MB
038_twoBool 👍 👍 7.81 s 46.0 MB
039_andType 👍 👍 6.84 s 45.9 MB
040_prodType 👍 👍 8.45 s 45.9 MB
041_pprodType 👍 👍 8.43 s 46.0 MB
042_pUnitType 👍 👍 3.27 s 45.7 MB
043_eqType 👍 👍 7.24 s 45.8 MB
044_natDef 👍 👍 6.54 s 45.9 MB
045_rbTreeDef 👍 👍 47.5 s 47.1 MB
046_inductBadNonSort ✋ ✋ 2.00 s 45.5 MB
047_inductBadNonSort2 ✋ ✋ 1.18 s 45.6 MB
048_inductLevelParam ✋ ✋ 1.05 s 45.5 MB
049_inductTooFewParams ✋ ✋ 1.12 s 45.7 MB
050_inductWrongCtorParams ✋ ✋ 2.08 s 45.6 MB
051_inductWrongCtorResParams ✋ ✋ 2.34 s 45.6 MB
052_inductWrongCtorResLevel ✋ ✋ 2.58 s 45.8 MB
053_inductInIndex ✋ ✋ 1.89 s 45.5 MB
054_indNeg ✋ ✋ 1.78 s 45.6 MB
055_reduceCtorParam.mk 👍 👍 9.21 s 46.0 MB
056_reduceCtorType.mk ✋ ✋ 2.79 s 45.8 MB
057_indNegReducible ✋ ✋ 3.36 s 45.7 MB
058_predWithTypeField 👍 👍 3.61 s 45.7 MB
059_typeWithTypeField 👍 👍 3.80 s 45.7 MB
060_typeWithTypeFieldPoly 👍 👍 4.04 s 45.7 MB
061_typeWithTooHighTypeField.mk ✋ ✋ 1.65 s 45.6 MB
062_emptyRec 👍 👍 2.40 s 45.5 MB
063_boolRec 👍 👍 6.35 s 45.8 MB
064_twoBoolRec 👍 👍 9.94 s 46.1 MB
065_andRec 👍 👍 7.64 s 46.0 MB
066_prodRec 👍 👍 9.77 s 46.1 MB
067_pprodRec 👍 👍 9.66 s 45.9 MB
068_punitRec 👍 👍 4.24 s 45.8 MB
069_eqRec 👍 👍 8.21 s 45.8 MB
070_nRec 👍 👍 7.03 s 45.8 MB
071_rbTreeRef 👍 👍 52.9 s 47.6 MB
072_boolPropRec 👍 👍 4.24 s 45.7 MB
073_BogusRecursor ✋ ✋ 3.05 s 45.7 MB
074_existsRec 👍 👍 9.05 s 45.9 MB
075_typeSingletonRecReduction 👍 👍 17.9 s 46.3 MB
076_sortElimPropRec 👍 👍 12.9 s 45.9 MB
077_sortElimProp2Rec 👍 👍 16.1 s 46.4 MB
078_boolRecEqns 👍 👍 29.6 s 46.7 MB
079_prodRecEqns 👍 👍 30.9 s 46.9 MB
080_nRecReduction 👍 👍 36.0 s 47.0 MB
081_listRecReduction 👍 👍 63.6 s 47.9 MB
082_RBTree.id_spec 👍 ⌛ 0 ms 0 B
083_And.right 👍 👍 9.69 s 46.2 MB
084_Prod.snd 👍 👍 11.0 s 45.9 MB
085_PProd.snd 👍 👍 11.0 s 46.0 MB
086_PSigma.snd 👍 👍 13.8 s 46.0 MB
087_projOutOfRange ✋ ✋ 8.09 s 46.0 MB
088_projNotStruct ✋ ✋ 6.87 s 45.8 MB
089_projProp1 👍 👍 18.5 s 46.3 MB
090_projProp2 ✋ ✋ 18.6 s 46.4 MB
091_projProp3 👍 👍 18.6 s 46.4 MB
092_projProp4 ✋ ✋ 18.6 s 46.3 MB
093_projProp5 ✋ ✋ 19.2 s 46.4 MB
094_projProp6 ✋ ✋ 18.6 s 46.2 MB
095_projDataIndexRec 👍 👍 14.0 s 46.2 MB
096_projIndexData ✋ ✋ 32.2 s 47.0 MB
097_projIndexData2 ✋ ✋ 32.2 s 46.9 MB
098_projRed 👍 👍 24.8 s 46.4 MB
099_ruleK 👍 👍 15.7 s 46.1 MB
100_ruleKbad ✋ ✋ 15.8 s 46.3 MB
101_ruleKAcc ✋ ✋ 36.1 s 47.2 MB
102_aNatLit 👍 👍 6.04 s 45.9 MB
103_natLitEq 👍 👍 14.1 s 46.0 MB
104_proofIrrelevance 👍 👍 12.0 s 46.2 MB
105_proofIrrelevanceBad ✋ ✋ 11.5 s 46.1 MB
106_proofIrrelevanceWhnf 👍 👍 13.6 s 46.2 MB
107_proofIrrelevanceUnderBinder 👍 👍 3.72 s 45.6 MB
108_unitEta1 👍 👍 14.4 s 46.2 MB
109_unitEta2 👍 👍 13.7 s 46.1 MB
110_unitEta3 👍 👍 13.8 s 46.2 MB
111_indexedUnitEta ✋ ✋ 15.6 s 46.2 MB
112_structEta 👍 👍 36.4 s 47.1 MB
113_indexedStructEta ✋ ✋ 18.2 s 46.3 MB
114_funEta 👍 👍 13.1 s 46.2 MB
115_funEtaDep 👍 👍 13.5 s 46.2 MB
116_funEtaBad ✋ ✋ 12.3 s 46.2 MB
117_reflOccLeft ✋ ✋ 7.27 s 45.8 MB
118_reflOccInIndex ✋ ✋ 7.70 s 45.8 MB
119_reduceCtorParamRefl.mk 👍 👍 10.4 s 46.0 MB
120_reduceCtorParamRefl2.mk 👍 👍 10.4 s 45.8 MB
121_rTreeRec 👍 👍 11.5 s 46.0 MB
122_rtreeRecReduction 👍 👍 26.9 s 46.7 MB
123_accRecType 👍 👍 21.5 s 46.4 MB
124_accRecReduction 👍 👍 44.7 s 47.6 MB
125_accRecNoEta ✋ ✋ 36.7 s 47.1 MB
126_quotMkType 👍 👍 14.4 s 46.3 MB
127_quotIndType 👍 👍 14.9 s 46.2 MB
128_quotLiftType 👍 👍 15.2 s 46.2 MB
129_quotSoundType 👍 👍 17.7 s 46.4 MB
130_quotLiftReduction 👍 👍 23.4 s 46.8 MB
131_quotIndReduction 👍 👍 22.1 s 46.5 MB
132_dup_defs ✋ ✋ 1.02 s 45.5 MB
133_dup_ind_def ✋ ✋ 2.57 s 45.7 MB
134_dup_ctor_def ✋ ✋ 2.61 s 45.8 MB
135_dup_rec_def ✋ ✋ 2.70 s 45.5 MB
136_misnamed_rec_user ✋ ✋ 3.37 s 45.7 MB
137_dup_rec_def2 ✋ ✋ 2.99 s 45.6 MB
138_dup_ctor_rec ✋ ✋ 2.49 s 45.6 MB
139_DupConCon ✋ ✋ 3.38 s 45.8 MB
140_falseFromUnsafe ✋ ✋ 2.29 s 45.5 MB
141_falseFromPartial ✋ ✋ 2.30 s 45.5 MB