From 54dd11a2d8e8fa71f2a8badfb9d6af332a66c55c Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 26 Feb 2026 06:51:51 +0000 Subject: [PATCH 1/3] Add test case for #10577 --- tests/constlevels.ndjson | 283 +++++++++++++++++++++++++++++++++++++++ tests/constlevels.yaml | 4 + 2 files changed, 287 insertions(+) create mode 100644 tests/constlevels.ndjson create mode 100644 tests/constlevels.yaml diff --git a/tests/constlevels.ndjson b/tests/constlevels.ndjson new file mode 100644 index 0000000..67d23f3 --- /dev/null +++ b/tests/constlevels.ndjson @@ -0,0 +1,283 @@ +{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"format":{"version":"3.1.0"},"lean":{"githash":"83e54b65b65d1d3ce31d99d820a7bd5f3e219295","version":"4.29.0-rc2"}}} +{"in":1,"str":{"pre":0,"str":"Nat"}} +{"il":1,"succ":0} +{"ie":0,"sort":1} +{"in":2,"str":{"pre":1,"str":"zero"}} +{"in":3,"str":{"pre":1,"str":"succ"}} +{"const":{"name":1,"us":[]},"ie":1} +{"in":4,"str":{"pre":0,"str":"n"}} +{"forallE":{"binderInfo":"default","body":1,"name":4,"type":1},"ie":2} +{"in":5,"str":{"pre":1,"str":"rec"}} +{"in":6,"str":{"pre":0,"str":"u"}} +{"il":2,"param":6} +{"in":7,"str":{"pre":0,"str":"motive"}} +{"in":8,"str":{"pre":0,"str":"t"}} +{"ie":3,"sort":2} +{"forallE":{"binderInfo":"default","body":3,"name":8,"type":1},"ie":4} +{"in":9,"str":{"pre":0,"str":"zero"}} +{"bvar":0,"ie":5} +{"const":{"name":2,"us":[]},"ie":6} +{"app":{"arg":6,"fn":5},"ie":7} +{"in":10,"str":{"pre":0,"str":"succ"}} +{"in":11,"str":{"pre":0,"str":"n_ih"}} +{"bvar":2,"ie":8} +{"app":{"arg":5,"fn":8},"ie":9} +{"bvar":3,"ie":10} +{"const":{"name":3,"us":[]},"ie":11} +{"bvar":1,"ie":12} +{"app":{"arg":12,"fn":11},"ie":13} +{"app":{"arg":13,"fn":10},"ie":14} +{"forallE":{"binderInfo":"default","body":14,"name":11,"type":9},"ie":15} +{"forallE":{"binderInfo":"default","body":15,"name":4,"type":1},"ie":16} +{"app":{"arg":5,"fn":10},"ie":17} +{"forallE":{"binderInfo":"default","body":17,"name":8,"type":1},"ie":18} +{"forallE":{"binderInfo":"default","body":18,"name":10,"type":16},"ie":19} +{"forallE":{"binderInfo":"default","body":19,"name":9,"type":7},"ie":20} +{"forallE":{"binderInfo":"implicit","body":20,"name":7,"type":4},"ie":21} +{"ie":22,"lam":{"binderInfo":"default","body":12,"name":10,"type":16}} +{"ie":23,"lam":{"binderInfo":"default","body":22,"name":9,"type":7}} +{"ie":24,"lam":{"binderInfo":"default","body":23,"name":7,"type":4}} +{"app":{"arg":5,"fn":12},"ie":25} +{"const":{"name":5,"us":[2]},"ie":26} +{"app":{"arg":10,"fn":26},"ie":27} +{"app":{"arg":8,"fn":27},"ie":28} +{"app":{"arg":12,"fn":28},"ie":29} +{"app":{"arg":5,"fn":29},"ie":30} +{"app":{"arg":30,"fn":25},"ie":31} +{"ie":32,"lam":{"binderInfo":"default","body":31,"name":4,"type":1}} +{"ie":33,"lam":{"binderInfo":"default","body":32,"name":10,"type":16}} +{"ie":34,"lam":{"binderInfo":"default","body":33,"name":9,"type":7}} +{"ie":35,"lam":{"binderInfo":"default","body":34,"name":7,"type":4}} +{"inductive":{"ctors":[{"cidx":0,"induct":1,"isUnsafe":false,"levelParams":[],"name":2,"numFields":0,"numParams":0,"type":1},{"cidx":1,"induct":1,"isUnsafe":false,"levelParams":[],"name":3,"numFields":1,"numParams":0,"type":2}],"recs":[{"all":[1],"isUnsafe":false,"k":false,"levelParams":[6],"name":5,"numIndices":0,"numMinors":2,"numMotives":1,"numParams":0,"rules":[{"ctor":2,"nfields":0,"rhs":24},{"ctor":3,"nfields":1,"rhs":35}],"type":21}],"types":[{"all":[1],"ctors":[2,3],"isRec":true,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":1,"numIndices":0,"numNested":0,"numParams":0,"type":0}]}} +{"in":12,"str":{"pre":0,"str":"Eq"}} +{"in":13,"str":{"pre":0,"str":"u_1"}} +{"il":3,"param":13} +{"in":14,"str":{"pre":0,"str":"α"}} +{"ie":36,"sort":3} +{"in":15,"str":{"pre":0,"str":"a"}} +{"in":16,"str":{"pre":15,"str":"_@"}} +{"in":17,"str":{"pre":16,"str":"_internal"}} +{"in":18,"str":{"pre":17,"str":"_hyg"}} +{"in":19,"num":{"i":0,"pre":18}} +{"ie":37,"sort":0} +{"forallE":{"binderInfo":"default","body":37,"name":19,"type":12},"ie":38} +{"forallE":{"binderInfo":"default","body":38,"name":19,"type":5},"ie":39} +{"forallE":{"binderInfo":"implicit","body":39,"name":14,"type":36},"ie":40} +{"in":20,"str":{"pre":12,"str":"refl"}} +{"const":{"name":12,"us":[3]},"ie":41} +{"app":{"arg":12,"fn":41},"ie":42} +{"app":{"arg":5,"fn":42},"ie":43} +{"app":{"arg":5,"fn":43},"ie":44} +{"forallE":{"binderInfo":"default","body":44,"name":15,"type":5},"ie":45} +{"forallE":{"binderInfo":"implicit","body":45,"name":14,"type":36},"ie":46} +{"in":21,"str":{"pre":12,"str":"rec"}} +{"app":{"arg":8,"fn":41},"ie":47} +{"app":{"arg":12,"fn":47},"ie":48} +{"app":{"arg":5,"fn":48},"ie":49} +{"forallE":{"binderInfo":"default","body":3,"name":8,"type":49},"ie":50} +{"forallE":{"binderInfo":"default","body":50,"name":19,"type":12},"ie":51} +{"in":22,"str":{"pre":0,"str":"refl"}} +{"app":{"arg":12,"fn":5},"ie":52} +{"const":{"name":20,"us":[3]},"ie":53} +{"app":{"arg":8,"fn":53},"ie":54} +{"app":{"arg":12,"fn":54},"ie":55} +{"app":{"arg":55,"fn":52},"ie":56} +{"bvar":4,"ie":57} +{"app":{"arg":57,"fn":41},"ie":58} +{"app":{"arg":10,"fn":58},"ie":59} +{"app":{"arg":5,"fn":59},"ie":60} +{"app":{"arg":12,"fn":10},"ie":61} +{"app":{"arg":5,"fn":61},"ie":62} +{"forallE":{"binderInfo":"default","body":62,"name":8,"type":60},"ie":63} +{"forallE":{"binderInfo":"implicit","body":63,"name":19,"type":10},"ie":64} +{"forallE":{"binderInfo":"default","body":64,"name":22,"type":56},"ie":65} +{"forallE":{"binderInfo":"implicit","body":65,"name":7,"type":51},"ie":66} +{"forallE":{"binderInfo":"implicit","body":66,"name":19,"type":5},"ie":67} +{"forallE":{"binderInfo":"implicit","body":67,"name":14,"type":36},"ie":68} +{"ie":69,"lam":{"binderInfo":"default","body":5,"name":22,"type":56}} +{"ie":70,"lam":{"binderInfo":"default","body":69,"name":7,"type":51}} +{"ie":71,"lam":{"binderInfo":"default","body":70,"name":19,"type":5}} +{"ie":72,"lam":{"binderInfo":"implicit","body":71,"name":14,"type":36}} +{"inductive":{"ctors":[{"cidx":0,"induct":12,"isUnsafe":false,"levelParams":[13],"name":20,"numFields":0,"numParams":2,"type":46}],"recs":[{"all":[12],"isUnsafe":false,"k":true,"levelParams":[6,13],"name":21,"numIndices":1,"numMinors":1,"numMotives":1,"numParams":2,"rules":[{"ctor":20,"nfields":0,"rhs":72}],"type":68}],"types":[{"all":[12],"ctors":[20],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[13],"name":12,"numIndices":1,"numNested":0,"numParams":2,"type":40}]}} +{"in":23,"str":{"pre":0,"str":"False"}} +{"in":24,"str":{"pre":23,"str":"rec"}} +{"const":{"name":23,"us":[]},"ie":73} +{"forallE":{"binderInfo":"default","body":3,"name":8,"type":73},"ie":74} +{"forallE":{"binderInfo":"default","body":25,"name":8,"type":73},"ie":75} +{"forallE":{"binderInfo":"default","body":75,"name":7,"type":74},"ie":76} +{"inductive":{"ctors":[],"recs":[{"all":[23],"isUnsafe":false,"k":false,"levelParams":[6],"name":24,"numIndices":0,"numMinors":0,"numMotives":1,"numParams":0,"rules":[],"type":76}],"types":[{"all":[23],"ctors":[],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":23,"numIndices":0,"numNested":0,"numParams":0,"type":37}]}} +{"in":25,"str":{"pre":0,"str":"Not"}} +{"forallE":{"binderInfo":"default","body":37,"name":15,"type":37},"ie":77} +{"forallE":{"binderInfo":"default","body":73,"name":19,"type":5},"ie":78} +{"ie":79,"lam":{"binderInfo":"default","body":78,"name":15,"type":37}} +{"def":{"all":[25],"hints":{"regular":1},"levelParams":[],"name":25,"safety":"safe","type":77,"value":79}} +{"in":26,"str":{"pre":0,"str":"Ne"}} +{"forallE":{"binderInfo":"implicit","body":39,"name":14,"type":3},"ie":80} +{"in":27,"str":{"pre":0,"str":"b"}} +{"const":{"name":25,"us":[]},"ie":81} +{"const":{"name":12,"us":[2]},"ie":82} +{"app":{"arg":8,"fn":82},"ie":83} +{"app":{"arg":12,"fn":83},"ie":84} +{"app":{"arg":5,"fn":84},"ie":85} +{"app":{"arg":85,"fn":81},"ie":86} +{"ie":87,"lam":{"binderInfo":"default","body":86,"name":27,"type":12}} +{"ie":88,"lam":{"binderInfo":"default","body":87,"name":15,"type":5}} +{"ie":89,"lam":{"binderInfo":"implicit","body":88,"name":14,"type":3}} +{"def":{"all":[26],"hints":{"regular":2},"levelParams":[6],"name":26,"safety":"safe","type":80,"value":89}} +{"in":28,"str":{"pre":0,"str":"True"}} +{"in":29,"str":{"pre":28,"str":"intro"}} +{"const":{"name":28,"us":[]},"ie":90} +{"in":30,"str":{"pre":28,"str":"rec"}} +{"forallE":{"binderInfo":"default","body":3,"name":8,"type":90},"ie":91} +{"in":31,"str":{"pre":0,"str":"intro"}} +{"const":{"name":29,"us":[]},"ie":92} +{"app":{"arg":92,"fn":5},"ie":93} +{"forallE":{"binderInfo":"default","body":9,"name":8,"type":90},"ie":94} +{"forallE":{"binderInfo":"default","body":94,"name":31,"type":93},"ie":95} +{"forallE":{"binderInfo":"implicit","body":95,"name":7,"type":91},"ie":96} +{"ie":97,"lam":{"binderInfo":"default","body":5,"name":31,"type":93}} +{"ie":98,"lam":{"binderInfo":"default","body":97,"name":7,"type":91}} +{"inductive":{"ctors":[{"cidx":0,"induct":28,"isUnsafe":false,"levelParams":[],"name":29,"numFields":0,"numParams":0,"type":90}],"recs":[{"all":[28],"isUnsafe":false,"k":true,"levelParams":[6],"name":30,"numIndices":0,"numMinors":1,"numMotives":1,"numParams":0,"rules":[{"ctor":29,"nfields":0,"rhs":98}],"type":96}],"types":[{"all":[28],"ctors":[29],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":28,"numIndices":0,"numNested":0,"numParams":0,"type":37}]}} +{"in":32,"str":{"pre":0,"str":"trivial"}} +{"thm":{"all":[32],"levelParams":[],"name":32,"type":90,"value":92}} +{"in":33,"str":{"pre":0,"str":"rfl"}} +{"app":{"arg":12,"fn":82},"ie":99} +{"app":{"arg":5,"fn":99},"ie":100} +{"app":{"arg":5,"fn":100},"ie":101} +{"forallE":{"binderInfo":"implicit","body":101,"name":15,"type":5},"ie":102} +{"forallE":{"binderInfo":"implicit","body":102,"name":14,"type":3},"ie":103} +{"const":{"name":20,"us":[2]},"ie":104} +{"app":{"arg":12,"fn":104},"ie":105} +{"app":{"arg":5,"fn":105},"ie":106} +{"ie":107,"lam":{"binderInfo":"implicit","body":106,"name":15,"type":5}} +{"ie":108,"lam":{"binderInfo":"implicit","body":107,"name":14,"type":3}} +{"def":{"all":[33],"hints":{"regular":1},"levelParams":[6],"name":33,"safety":"safe","type":103,"value":108}} +{"in":34,"str":{"pre":12,"str":"symm"}} +{"in":35,"str":{"pre":0,"str":"h"}} +{"app":{"arg":10,"fn":82},"ie":109} +{"app":{"arg":12,"fn":109},"ie":110} +{"app":{"arg":8,"fn":110},"ie":111} +{"forallE":{"binderInfo":"default","body":111,"name":35,"type":85},"ie":112} +{"forallE":{"binderInfo":"implicit","body":112,"name":27,"type":12},"ie":113} +{"forallE":{"binderInfo":"implicit","body":113,"name":15,"type":5},"ie":114} +{"forallE":{"binderInfo":"implicit","body":114,"name":14,"type":3},"ie":115} +{"const":{"name":21,"us":[0,2]},"ie":116} +{"app":{"arg":10,"fn":116},"ie":117} +{"app":{"arg":8,"fn":117},"ie":118} +{"in":36,"str":{"pre":0,"str":"x"}} +{"in":37,"str":{"pre":36,"str":"_@"}} +{"in":38,"str":{"pre":37,"str":"Init"}} +{"in":39,"str":{"pre":38,"str":"Prelude"}} +{"in":40,"num":{"i":2345006592,"pre":39}} +{"in":41,"str":{"pre":40,"str":"_hygCtx"}} +{"in":42,"str":{"pre":41,"str":"_hyg"}} +{"in":43,"num":{"i":14,"pre":42}} +{"in":44,"str":{"pre":35,"str":"_@"}} +{"in":45,"str":{"pre":44,"str":"Init"}} +{"in":46,"str":{"pre":45,"str":"Prelude"}} +{"in":47,"num":{"i":2345006592,"pre":46}} +{"in":48,"str":{"pre":47,"str":"_hygCtx"}} +{"in":49,"str":{"pre":48,"str":"_hyg"}} +{"in":50,"num":{"i":15,"pre":49}} +{"app":{"arg":57,"fn":82},"ie":119} +{"app":{"arg":10,"fn":119},"ie":120} +{"app":{"arg":5,"fn":120},"ie":121} +{"bvar":5,"ie":122} +{"app":{"arg":122,"fn":82},"ie":123} +{"app":{"arg":12,"fn":123},"ie":124} +{"app":{"arg":57,"fn":124},"ie":125} +{"ie":126,"lam":{"binderInfo":"default","body":125,"name":50,"type":121}} +{"ie":127,"lam":{"binderInfo":"default","body":126,"name":43,"type":10}} +{"app":{"arg":127,"fn":118},"ie":128} +{"const":{"name":33,"us":[2]},"ie":129} +{"app":{"arg":10,"fn":129},"ie":130} +{"app":{"arg":8,"fn":130},"ie":131} +{"app":{"arg":131,"fn":128},"ie":132} +{"app":{"arg":12,"fn":132},"ie":133} +{"app":{"arg":5,"fn":133},"ie":134} +{"ie":135,"lam":{"binderInfo":"default","body":134,"name":35,"type":85}} +{"ie":136,"lam":{"binderInfo":"implicit","body":135,"name":27,"type":12}} +{"ie":137,"lam":{"binderInfo":"implicit","body":136,"name":15,"type":5}} +{"ie":138,"lam":{"binderInfo":"implicit","body":137,"name":14,"type":3}} +{"thm":{"all":[34],"levelParams":[6],"name":34,"type":115,"value":138}} +{"in":51,"str":{"pre":0,"str":"false_ne_true"}} +{"const":{"name":26,"us":[1]},"ie":139} +{"app":{"arg":37,"fn":139},"ie":140} +{"app":{"arg":73,"fn":140},"ie":141} +{"app":{"arg":90,"fn":141},"ie":142} +{"const":{"name":12,"us":[1]},"ie":143} +{"app":{"arg":37,"fn":143},"ie":144} +{"app":{"arg":73,"fn":144},"ie":145} +{"app":{"arg":90,"fn":145},"ie":146} +{"const":{"name":21,"us":[0,1]},"ie":147} +{"app":{"arg":37,"fn":147},"ie":148} +{"app":{"arg":90,"fn":148},"ie":149} +{"in":52,"str":{"pre":38,"str":"Core"}} +{"in":53,"num":{"i":789336685,"pre":52}} +{"in":54,"str":{"pre":53,"str":"_hygCtx"}} +{"in":55,"str":{"pre":54,"str":"_hyg"}} +{"in":56,"num":{"i":17,"pre":55}} +{"in":57,"str":{"pre":45,"str":"Core"}} +{"in":58,"num":{"i":789336685,"pre":57}} +{"in":59,"str":{"pre":58,"str":"_hygCtx"}} +{"in":60,"str":{"pre":59,"str":"_hyg"}} +{"in":61,"num":{"i":18,"pre":60}} +{"app":{"arg":90,"fn":144},"ie":150} +{"app":{"arg":5,"fn":150},"ie":151} +{"ie":152,"lam":{"binderInfo":"default","body":12,"name":61,"type":151}} +{"ie":153,"lam":{"binderInfo":"default","body":152,"name":56,"type":37}} +{"app":{"arg":153,"fn":149},"ie":154} +{"const":{"name":32,"us":[]},"ie":155} +{"app":{"arg":155,"fn":154},"ie":156} +{"app":{"arg":73,"fn":156},"ie":157} +{"const":{"name":34,"us":[1]},"ie":158} +{"app":{"arg":37,"fn":158},"ie":159} +{"app":{"arg":73,"fn":159},"ie":160} +{"app":{"arg":90,"fn":160},"ie":161} +{"app":{"arg":5,"fn":161},"ie":162} +{"app":{"arg":162,"fn":157},"ie":163} +{"ie":164,"lam":{"binderInfo":"default","body":163,"name":35,"type":146}} +{"thm":{"all":[51],"levelParams":[],"name":51,"type":142,"value":164}} +{"in":62,"str":{"pre":12,"str":"casesOn"}} +{"app":{"arg":10,"fn":41},"ie":165} +{"app":{"arg":8,"fn":165},"ie":166} +{"app":{"arg":5,"fn":166},"ie":167} +{"app":{"arg":10,"fn":8},"ie":168} +{"app":{"arg":57,"fn":53},"ie":169} +{"app":{"arg":10,"fn":169},"ie":170} +{"app":{"arg":170,"fn":168},"ie":171} +{"app":{"arg":8,"fn":10},"ie":172} +{"app":{"arg":12,"fn":172},"ie":173} +{"forallE":{"binderInfo":"default","body":173,"name":22,"type":171},"ie":174} +{"forallE":{"binderInfo":"default","body":174,"name":8,"type":167},"ie":175} +{"forallE":{"binderInfo":"implicit","body":175,"name":19,"type":8},"ie":176} +{"forallE":{"binderInfo":"implicit","body":176,"name":7,"type":51},"ie":177} +{"forallE":{"binderInfo":"implicit","body":177,"name":19,"type":5},"ie":178} +{"forallE":{"binderInfo":"implicit","body":178,"name":14,"type":36},"ie":179} +{"const":{"name":21,"us":[2,3]},"ie":180} +{"app":{"arg":122,"fn":180},"ie":181} +{"app":{"arg":57,"fn":181},"ie":182} +{"app":{"arg":10,"fn":182},"ie":183} +{"app":{"arg":5,"fn":183},"ie":184} +{"app":{"arg":8,"fn":184},"ie":185} +{"app":{"arg":12,"fn":185},"ie":186} +{"ie":187,"lam":{"binderInfo":"default","body":186,"name":22,"type":171}} +{"ie":188,"lam":{"binderInfo":"default","body":187,"name":8,"type":167}} +{"ie":189,"lam":{"binderInfo":"implicit","body":188,"name":19,"type":8}} +{"ie":190,"lam":{"binderInfo":"implicit","body":189,"name":7,"type":51}} +{"ie":191,"lam":{"binderInfo":"implicit","body":190,"name":19,"type":5}} +{"ie":192,"lam":{"binderInfo":"implicit","body":191,"name":14,"type":36}} +{"def":{"all":[62],"hints":"abbrev","levelParams":[6,13],"name":62,"safety":"safe","type":179,"value":192}} +{"in":63,"str":{"pre":0,"str":"_test"}} +{"app":{"arg":1,"fn":5},"ie":193} +{"ie":194,"letE":{"body":5,"name":36,"nondep":false,"type":193,"value":143}} +{"app":{"arg":143,"fn":194},"ie":195} +{"app":{"arg":193,"fn":195},"ie":196} +{"const":{"name":51,"us":[]},"ie":197} +{"app":{"arg":194,"fn":197},"ie":198} +{"const":{"name":62,"us":[]},"ie":199} +{"ie":200,"letE":{"body":193,"name":36,"nondep":false,"type":198,"value":199}} +{"ie":201,"letE":{"body":200,"name":36,"nondep":false,"type":143,"value":196}} +{"ie":202,"letE":{"body":201,"name":36,"nondep":false,"type":143,"value":201}} +{"ie":203,"letE":{"body":202,"name":36,"nondep":false,"type":1,"value":1}} +{"thm":{"all":[63],"levelParams":[],"name":63,"type":203,"value":37}} diff --git a/tests/constlevels.yaml b/tests/constlevels.yaml new file mode 100644 index 0000000..935b037 --- /dev/null +++ b/tests/constlevels.yaml @@ -0,0 +1,4 @@ +description: | + Incorrect number of level variables for constant +file: tests/constlevels.ndjson +outcome: reject From b8bc0d2b043ff28574d217fdbe348350b935e2af Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 26 Feb 2026 06:52:09 +0000 Subject: [PATCH 2/3] Claude-produced fix for the problem that file tests are not discovered --- lka.py | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/lka.py b/lka.py index f423bf4..5fa89f4 100755 --- a/lka.py +++ b/lka.py @@ -827,6 +827,38 @@ def create_test(test: dict, output_dir: Path) -> bool: shutil.copy(source_file, tmp_file) tmp_file.rename(output_file) print(f" Copied {source_file} to {output_file}") + + # Gather stats about the copied file + file_size = output_file.stat().st_size + with open(output_file, "r") as f: + line_count = sum(1 for _ in f) + + test_metadata = extract_ndjson_metadata(output_file) + size_str = format_memory(file_size) + lines_str = format_unitless(line_count) + print(f" {size_str}, {lines_str} lines") + + stats_file = output_dir / f"{name}.stats.json" + stats = { + "name": name, + "size": file_size, + "size_str": size_str, + "lines": line_count, + "lines_str": lines_str, + "yaml_file": f"tests/{name}.yaml", + "outcome": test.get("outcome"), + } + stats.update(test_metadata) + if test.get("description"): + stats["description"] = test["description"] + if test.get("large"): + stats["large"] = test["large"] + build_info = get_build_metadata() + source_links = generate_source_links(test, "tests", build_info.get("git_revision")) + stats.update(source_links) + with open(stats_file, "w") as f: + json.dump(stats, f, indent=2) + return True # These test types require lean4export From 1023caecfbf0432e67809485c935725f71dc7ac2 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 26 Feb 2026 07:12:31 +0000 Subject: [PATCH 3/3] Improve description --- tests/constlevels.yaml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/tests/constlevels.yaml b/tests/constlevels.yaml index 935b037..f90cd99 100644 --- a/tests/constlevels.yaml +++ b/tests/constlevels.yaml @@ -1,4 +1,13 @@ description: | - Incorrect number of level variables for constant + Regression test for undefined behavior in `lazy_delta_reduction_step` in the official kernel + + In the function `lazy_delta_reduction_step`, the official kernel expects `unfold_definition` + to always succeed. However, if the constant has an incorrect number of level parameters, it + actually fails, which leads to memory corruption in `lazy_delta_reduction_step`. + + This test is to check that the official kernel and also other kernels that closely follow the + logic of the official kernel correctly handle this unfolding failure. + + The issue in the official kernel was originally reported as https://github.com/leanprover/lean4/issues/10577. file: tests/constlevels.ndjson outcome: reject