Lake check/comparator can reuse export files and tune sandboxing (
dc34e5f, a2233a3, 
669e6b4)
lake check and lake comparator gained new modes to load prebuilt export NDJSON directly, avoiding an on-the-fly rebuild/export step. Comparator also now has an expert-only --inadvisably-no-sandbox escape hatch, and --paranoid runs additional bundled checkers alongside Lean's kernel for stronger verification.
Float and Float32 now expose fused multiply-add (
d3a0781)
Float.fma and Float32.fma were added with logical models in the corresponding float model modules, backed by the native fma/fmaf C functions. This gives Lean code access to a more accurate single-rounding x * y + z operation and expands the standard float API.
Parser preserves whitespace for hygieneInfo antiquotations (
9632ea4)
The parser/pretty-printer path was adjusted so hygieneInfo antiquotations no longer drop the trailing space from the preceding token. That fixes reprinting and source reconstruction for syntax that depends on that whitespace.
InfoTree utilities moved into elaboration internals (5e7db96)
InfoTree/SnapshotTree helpers were relocated out of the server namespace into Lean.Elab, with the old server module deprecated. This is a broad internal refactor that cleans up ownership of elaboration-time tree traversal and related LSP helpers.
