Update lean4export to 3.1.0 format

checkers/lean4lean/lean4lean-wrapper.py

@@ -10,11 +10,11 @@
 
 # Map from Lean toolchains to lean4lean git tags
 TOOLCHAIN_TO_TAG = {
-    "4.27.0-rc1": ("arena/v4.27.0-rc1","73fef0c"),
-    "4.28.0-nightly-2026-01-19": ("arena/v4.27.0-rc1","73fef0c"),
-    "4.28.0-nightly-2026-01-20": ("arena/v4.27.0-rc1","73fef0c"),
-    "4.27.0-nightly-2025-12-01": ("arena/v4.26.0","1a2c6b2"),
-    "4.26.0": ("arena/v4.26.0","1a2c6b2"),
+    "4.27.0-rc1": ("arena/v4.27.0-rc1","4bc2066"),
+    "4.28.0-nightly-2026-01-19": ("arena/v4.27.0-rc1","4bc2066"),
+    "4.28.0-nightly-2026-01-20": ("arena/v4.27.0-rc1","4bc2066"),
+    "4.27.0-nightly-2025-12-01": ("arena/v4.26.0","c1429d5"),
+    "4.26.0": ("arena/v4.26.0","c1429d5"),
 }
 
 # Base directory for lean4lean builds

checkers/nanoda.yaml

@@ -16,9 +16,9 @@ description: |
 
   The nanoda integration in the arena does not distinguish between a rejected proof and other forms
   of failure, so they are all repoted as “rejected”.
-url: https://github.com/ammkrn/nanoda_lib/
-ref: json_string
-rev: 2747659518c0d5debe1d05cb02ba9232cafa4897
+url: https://github.com/nomeata/nanoda_lib/
+ref: joachim/pred_of_nat_succ
+rev: 2425d79dd38ada0e863c6268837fe17d4b9d76e6
 build: |
   cargo build --release
   cat > config.json <<__END__
@@ -27,7 +27,7 @@ build: |
      "nat_extension": true,
      "string_extension": true,
      "unpermitted_axiom_hard_error": false,
-     "permitted_axioms": ["propext", "Classical.choice", "Quot.sound", "Lean.trustCompiler"],
+     "unsafe_permit_all_axioms": true,
      "num_threads": 4
    }
   __END__

checkers/official/lake-manifest.json

@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "f8c6ed35d043b6253d66e7f0b4a1368f659ebc8e",
+   "rev": "a31244ec8f800315a96e9e5a74f3b873cf34b6f9",
    "name": "lean4export",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "joachim_parse_fixes",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "kernel",

checkers/official/lakefile.toml

@@ -9,7 +9,7 @@ root = "Main"
 [[require]]
 scope = "leanprover"
 name = "lean4export"
-rev = "joachim_parse_fixes"
+rev = "master"
 
 [[require]]
 scope = "leanprover"

checkers/official/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.28.0-rc1

lka.py

@@ -419,6 +419,12 @@ def run_cmd(
             status = "ok" if result.returncode == 0 else f"FAILED (exit {result.returncode})"
             print(f"      -> {status} in {format_duration(elapsed)}")
 
+    if VERBOSE:
+        if result.stdout:
+            print(f"      stdout: {result.stdout.replace('\n', '\n               ')}")
+        if result.stderr:
+            print(f"      stderr: {result.stderr.replace('\n', '\n               ')}")
+
     return result
 
 
@@ -498,7 +504,7 @@ def setup_lean4export(toolchain: str) -> Path | None:
 
         lean4export_tmp_dir.mkdir(parents=True, exist_ok=True)
 
-        clone_cmd = ["git", "clone", "--branch", "arena_json_output",
+        clone_cmd = ["git", "clone", "--branch", "master",
                     "https://github.com/leanprover/lean4export",
                     str(lean4export_tmp_dir)]
         result = run_cmd(clone_cmd)
@@ -858,7 +864,11 @@ def create_test(test: dict, output_dir: Path) -> bool:
 
         result = run_cmd(run_cmd_str, cwd=work_dir, shell=True, env=env)
         if result.returncode != 0:
-            print(f"  Script failed: {result.stderr}")
+            print(f"  Script failed")
+            if result.stdout:
+                print(f"  stdout: {result.stdout.replace('\n', '\n          ')}")
+            if result.stderr:
+                print(f"  stderr: {result.stderr.replace('\n', '\n          ')}")
             return False
 
     if multiple:
@@ -1136,6 +1146,7 @@ def run_checker_on_test(checker: dict, test: dict, build_dir: Path, tests_dir: P
             "checker": checker_name,
             "test": test_name,
             "status": "error",
+            "correctness": "error",
             "message": f"Test file not found: {test_file}",
             "exit_code": -1,
             "wall_time": 0,
@@ -1179,10 +1190,24 @@ def run_checker_on_test(checker: dict, test: dict, build_dir: Path, tests_dir: P
     else:
         status = "error"
 
+    # Determine correctness based on expected outcome
+    expected_outcome = test.get("outcome")
+    if status == "declined":
+        correctness = "declined"
+    elif status == "error":
+        correctness = "error"
+    elif expected_outcome == "accept" and status == "accepted":
+        correctness = "correct"
+    elif expected_outcome == "reject" and status == "rejected":
+        correctness = "correct"
+    else:
+        correctness = "incorrect"
+
     result_data = {
         "checker": checker_name,
         "test": test_name,
         "status": status,
+        "correctness": correctness,
         "exit_code": exit_code,
         "wall_time": result.wall_time,
         "cpu_time": result.cpu_time,
@@ -1247,29 +1272,60 @@ def cmd_run_checker(args: argparse.Namespace) -> int:
         print("No built tests found.")
         return 0
 
-    # Sort tests by line count for consistent processing order
-    tests = sort_tests_by_line_count(tests)
-
     results = []
     for checker in checkers:
         for test in tests:
             print(f"Running {checker['name']} on {test['name']}...", end="\n" if VERBOSE else " ", flush=True)
             result = run_checker_on_test(checker, test, build_dir, tests_dir, results_dir)
             results.append(result)
-            print(f"[{result['status']}, {format_duration(result['wall_time'])}]", flush=True)
+
+            # Choose emoji based on status
+            status = result.get('status', 'error')
+            if status == 'accepted':
+                status_emoji = '👍'
+            elif status == 'rejected':
+                status_emoji = '👎'
+            elif status == 'declined':
+                status_emoji = '⊘'
+            else:  # error
+                status_emoji = '⚠️'
+
+            # Choose emoji based on correctness
+            correctness = result.get('correctness', 'error')
+            if correctness == 'correct':
+                correctness_emoji = '✅'
+            elif correctness == 'incorrect':
+                correctness_emoji = '❌'
+            elif correctness == 'declined':
+                correctness_emoji = '⊘'
+            else:  # error
+                correctness_emoji = '⚠️'
+
+            print(f"[{status_emoji} {correctness_emoji} {format_duration(result['wall_time'])}]", flush=True)
 
     # Summary
     print("\n" + "=" * 60)
     print("Summary:")
     print("=" * 60)
 
-    status_counts = {"accepted": 0, "rejected": 0, "declined": 0, "error": 0}
+    correctness_counts = {"correct": 0, "incorrect": 0, "declined": 0, "error": 0}
     for r in results:
-        status_counts[r["status"]] = status_counts.get(r["status"], 0) + 1
+        correctness = r.get("correctness", "error")
+        correctness_counts[correctness] = correctness_counts.get(correctness, 0) + 1
 
-    for status, count in status_counts.items():
+    # Print in order: correct, incorrect, declined, error
+    for correctness in ["correct", "incorrect", "declined", "error"]:
+        count = correctness_counts.get(correctness, 0)
         if count > 0:
-            print(f"  {status}: {count}")
+            if correctness == "correct":
+                emoji = "✅"
+            elif correctness == "incorrect":
+                emoji = "❌"
+            elif correctness == "declined":
+                emoji = "⊘"
+            else:  # error
+                emoji = "⚠️"
+            print(f"  {correctness}: {count} {emoji}")
 
     return 0
 
@@ -1329,6 +1385,7 @@ def load_tests() -> list[dict]:
         except Exception as e:
             print(f"Warning: Could not read stats file {stats_file}: {e}")
 
+    tests.sort(key=lambda t: t["name"])
     return tests
 
 

tests/tutorial.yaml

@@ -3,4 +3,4 @@ dir: tutorial
 multiple: true
 run: |
   lake clean
-  lake build Tutorial
+  LEAN_ABORT_ON_PANIC=1 lake build Tutorial

tutorial/Tutorial/Export.lean

@@ -1,35 +1,42 @@
 import Export
 open Lean
 
-/-! This module should not be necessary if lean4export's API were more complete -/
+initialize importedRecursorMap : IO.Ref (NameMap NameSet) ← do
+  IO.mkRef {}
 
-def semver := "3.0.0"
+def addRecInfo (constInfo : ConstantInfo) (recursorMap : NameMap NameSet) : NameMap NameSet :=
+  if let .recInfo recVal := constInfo then
+    recVal.all.foldl (init := recursorMap) fun recursorMap indName =>
+      recursorMap.alter indName <|
+        fun
+        | none => some <| NameSet.empty.insert recVal.name
+        | some recNames => some <| recNames.insert recVal.name
+  else
+    recursorMap
 
-def exportMetadata : Json :=
-  let leanMeta := Json.mkObj [
-    ("version", versionString),
-    ("githash", githash)
-  ]
-  let exporterMeta := Json.mkObj [
-    ("name", "lean4export"),
-    ("version", semver)
-  ]
-
-  Json.mkObj [
-    ("meta", Json.mkObj [
-      ("exporter", exporterMeta),
-      ("lean", leanMeta)
-    ])
-  ]
+/--
+Like initstate, but assumes that the imported entries in `env` are
+always the same and cache them
+-/
+def initStateCached (env : Environment) (cliOptions : List String := []) : M Unit := do
+  let mut recursorMap : NameMap NameSet := (← importedRecursorMap.get)
+  if recursorMap.isEmpty then
+    for (_, constInfo) in env.constants.map₁ do
+      recursorMap := addRecInfo constInfo recursorMap
+    importedRecursorMap.set recursorMap
+  for (_, constInfo) in env.constants.map₂ do
+    recursorMap := addRecInfo constInfo recursorMap
+  modify fun st => { st with
+    exportMData  := cliOptions.any  (· == "--export-mdata")
+    exportUnsafe := cliOptions.any (· == "--export-unsafe")
+    recursorMap
+  }
 
 def exportDeclsFromEnv (env : Lean.Environment) (constants : Array Name) : IO Unit := do
   initSearchPath (← findSysroot)
   M.run env do
-    modify (fun st => { st with
-      exportMData  := false
-      exportUnsafe := false
-    })
-    IO.println exportMetadata.compress
+    initStateCached env
+    dumpMetadata
     for c in constants do
       modify (fun st => { st with noMDataExprs := {} })
       let _ ← dumpConstant c

tutorial/lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "874fdb12dfd5600de03e21303b561d75ef64f111",
+   "rev": "a31244ec8f800315a96e9e5a74f3b873cf34b6f9",
    "name": "Lean4Export",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "arena_json_output",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "tutorial",

tutorial/lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = [ "Tutorial" ]
 [[require]]
 name = "Lean4Export"
 git = "https://github.com/leanprover/lean4export"
-rev = "arena_json_output"
+rev = "master"
 
 [[lean_lib]]
 name = "Tutorial"