[kiranandcode]

Stacked on #15 (codex/lean-4.35-newton). These fix four problems found while driving the kernel bridge from materia, where a translator elaborates generated Lean declarations against a compiled Mathlib project.

(a) Kernel.process dropped Lean's messages and the environment

New @[python "leanpy_kernel_frontend_process_json"] frontendProcessJson (source : String) (inheritEnv : Bool) : IO String, wrapped as:

Kernel.elaborate(source: str, *, inherit_env: bool = False) -> ProcessResult

• ProcessResult has these fields:

  • commands: list[Command], where a Command is (line, constants, messages);
  • header: list[Message];
  • error: str | None. This is set only when nothing could be processed: no environment is loaded, or an imported module isn't loaded.

  It also has the properties messages, errors, constants and ok (no error and no error-severity message).

• A Message has severity ("error", "warning" or "information"), line (1-based), column (0-based), end_line, end_column and text, all relative to the processed source.

• With inherit_env=True, envRef becomes the environment after the source. Later elaborate, process, decl_type, decl_axioms, goal_create and other calls then see the new declarations, so fragments can be elaborated and checked one at a time. If an exception occurs, the environment is unchanged. A declaration that fails to elaborate is still added (with sorryAx) and reported; callers check ok/errors.

Kernel.process keeps its string result, so existing callers and tests are unaffected.

(b) A module/import header gave empty output silently

createContextStateFromFile (env? := some env) started parsing at byte 0, so a header failed to parse as commands, and the error was dropped. Both entry points, and collect_sorrys, now parse the header with Parser.parseHeader:

• If every module it imports is already in the loaded environment, the header is skipped and elaboration starts after it. A module keyword is accepted, and the body is elaborated as ordinary commands.
• Otherwise nothing is elaborated: elaborate returns error naming the missing modules, and process returns <error: …>.

(c) lean_prefix depended on the cwd's lean-toolchain

utils.lean_prefix() resolves the first of these that is set:

1. LEANPY_LEAN_PREFIX;
2. a pinned toolchain, from utils.set_toolchain(name | lean-toolchain file | dir), LEANPY_TOOLCHAIN or ELAN_TOOLCHAIN, resolved by lean --print-prefix with ELAN_TOOLCHAIN set;
3. lean.py's own lean-toolchain, when it runs from a checkout;
4. the old cwd behaviour.

LeanLibrary.from_lake pins the project's lean-toolchain unless the caller already pinned one. _parse.find_lean_header now uses the same resolution instead of its own lean --print-prefix.

The in-process Lean has the same problem: Kernel.init_search calls Lean.findSysroot, which ran lean --print-prefix in the cwd. From a directory without a toolchain it failed with "no default toolchain configured". LeanLibrary now sets LEAN_SYSROOT, if unset, to the resolved prefix when it loads the runtime, and findSysroot reads that first.

(d) Names came back wrapped in «»

process and elaborate constants, all_decls, catalog, search, module_of and decl_axioms now use Name.toString (escape := false). Goal and metavariable names are unchanged, since they are round-tripped into resume and similar calls. The ops that take a declaration name (decl_exists, decl_type, decl_value, decl_axioms, module_of, is_internal_name) accept it unescaped or escaped (parseName), so returned names read back. String.toName alone returns anonymous for a b. A component that itself contains a dot needs the escaped form.

(e) A top-level Float argument or result was boxed

LeanLibrary's wrapper passed a Float parameter through to_lean, which boxes it with lean_box_float. That is right inside an Array Float or a structure, but at the C ABI a top-level Float is a raw double. So any @[python] function taking a Float failed with "argument N: must be real number, not LP_lean_object", and a Float result was unboxed from a double. Both now go by value, the same way the wrapper already unboxes a top-level Bool/enum. tests/lean/TestLib.lean gains py_float_affine (x : Float) (k : Nat) (ys : Array Float) : Float, and test_marshal.py gains a test for it. This was found while exporting a binary64 mirror from materia (BasisResearch/materia#24).

Tests

The new tests/test_kernel_process.py has 14 tests:

• constants per command;
• error and information messages with their positions;
• declarations not persisting without inherit_env, and persisting with it (also after an error);
• a header of loaded imports skipped, a module header skipped, and an unloaded import refused by name;
• unescaped names that read back, both unescaped and escaped;
• init_search from a cwd with no toolchain;
• lean_prefix ignoring a bogus lean-toolchain in the cwd, honouring LEANPY_LEAN_PREFIX, and set_toolchain from a file.

Full suite on Linux x86 (AWS, Lean 4.35.0): 1330 passed, 7 skipped, 3 failed. The 3 failures are the test_packaging bundle and wheel tests, which need patchelf. It isn't installed on this box, and they fail the same way on the base branch. ruff check and ruff format --check are clean. examples/kernel/lean (KernelBridge) and tests/lean build.

🤖 Generated with Claude Code