From 72fd28deb2a1ee61a895c5448faef696dd78e30c Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 16 Jul 2026 13:50:25 -0400 Subject: [PATCH 1/3] feat: look for ilean.mmap files on watchdog load --- src/Lean/Server/References.lean | 49 +++++++++++++++++++++++++++++++++ src/Lean/Server/Watchdog.lean | 20 +++++++++++++- 2 files changed, 68 insertions(+), 1 deletion(-) diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 02c4ff28d648..3f175b61e313 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -216,6 +216,55 @@ structure Ilean where decls : Lsp.Decls deriving FromJson, ToJson +/-- Extra data stored with an `.ilean` loaded and written to disk for mmapping -/ +structure Milean extends Ilean where + /-- The `.ilean.hash` value, as computed by Lake.fetchFileHash from the `.ilean` JSON. -/ + hash : Option UInt64 + +/-- +Given `.hash`, attempt to read the 64-bit hex value it contains. +Duplicates, and needs to be kept functionally in sync with, `Lake.Hash.load?`. +-/ +private def loadHash (hashFile : System.FilePath) : IO UInt64 := do + let contents ← FS.readBinFile hashFile + if contents.size != 16 then throw (.userError s!"hash file does not have expected form") + + let mut result: UInt64 := 0 + for byte in contents do + result := result.shiftLeft 4 + if '0'.toUInt8 ≤ byte && byte ≤ '9'.toUInt8 then result := result + (byte - '0'.toUInt8).toUInt64 + else if 'a'.toUInt8 ≤ byte && byte ≤ 'f'.toUInt8 then result := result + (byte - 'a'.toUInt8 + 10).toUInt64 + else if 'A'.toUInt8 ≤ byte && byte ≤ 'F'.toUInt8 then result := result + (byte - 'A'.toUInt8 + 10).toUInt64 + else throw (.userError s!"unexpected byte {byte} in hash") + return result + +/-- +The extension for a memory-mapped ilean file +-/ +def Milean.ext := "ilean.mmap" + +/-- +Given a path `.ilean`, attempt to read `.ilean.mmap`. Returns `.none` if the file does +not exist, `.some ilean` if the file hashes match, indicating that `.ilean.mmap` is a +mmapped version of `.ilean`, throws an error otherwise. +-/ +def Milean.load (ileanPath : System.FilePath) : IO (Option Ilean) := do + if ileanPath.extension ≠ .some "ilean" then throw (.userError s!"Milean.load: '{ileanPath}' not an .ilean") + let mileanPath := ileanPath.withExtension Milean.ext + if not (← mileanPath.pathExists) then return .none + + let hashPath := ileanPath.addExtension "hash" + + -- nb: ignoring the region means we can't unmap this ilean later + let (milean, _region) ← unsafe CompactedRegion.read (α := Milean) mileanPath #[] + if let .some memHash := milean.hash then + if not (← hashPath.pathExists) then throw (.userError s!"Milean.load: '{mileanPath}' expected '{hashPath}' to exist, but that file does not exist") + let fsHash ← loadHash hashPath + if memHash ≠ fsHash then throw (.userError s!"Milean.load: '{mileanPath}' expects a .ilean.hash value {String.ofList <| Nat.toDigits 16 memHash.toNat}, but .ilean.hash contains {String.ofList <| Nat.toDigits 16 fsHash.toNat}") + else + if (← hashPath.pathExists) then throw (.userError s!"Milean.load: '{mileanPath}' expected no '{hashPath}' to exist, but that file does exist") + return milean.toIlean + namespace Ilean open Lean.IO diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index dedb28154c48..94b8cd9f6d53 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -15,6 +15,7 @@ public import Lean.Server.Completion.CompletionUtils public import Init.Data.List.Sort public import Std.Sync.Channel public import Lean.Server.Logging +import all Lean.Elab.ErrorUtils public section @@ -1678,9 +1679,24 @@ results in requests that need references. def startLoadingReferences (referenceData : Std.Mutex ReferenceData) : IO Unit := do let task ← ServerTask.IO.asTask do let oleanSearchPath ← Lean.searchPathRef.get + let mut mileanCount := 0 + let mut mileanErrors := 0 for path in ← oleanSearchPath.findAllWithExt "ilean" do + let milean : Option Ilean ← try + let .some milean ← Milean.load path | pure .none + mileanCount := mileanCount + 1 + pure milean + catch _ => + -- milean errors should not be fatal, but we *should* log them + -- individually to help debug the global error message we give on error + mileanErrors := mileanErrors + 1 + mileanCount := mileanCount + 1 -- errors mean there *was* a milean but something went wrong + pure .none + try - let ilean ← Ilean.load path + let ilean ← match milean with + | .none => Ilean.load path + | .some il => pure il referenceData.atomically do let rd ← get let rd ← rd.modifyReferencesM (·.addIlean path ilean) @@ -1690,6 +1706,8 @@ def startLoadingReferences (referenceData : Std.Mutex ReferenceData) : IO Unit : -- ilean load errors should not be fatal, but we *should* log them -- when we add logging to the server pure () + if mileanErrors > 0 then + (← getStderr).putStrLn s!"Attempted to load {mileanCount} .{Milean.ext} {mileanCount.plural "file"}, but failed to load {mileanErrors} of them" referenceData.atomically <| modify fun rd => { rd with loadingTask := task.mapCheap fun _ => () } From dc55434684cd85bd05d7e4098f4c384630f4fa2d Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 17 Jul 2026 08:55:23 -0400 Subject: [PATCH 2/3] Clarify comment --- src/Lean/Server/References.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 3f175b61e313..aadc36bc799c 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -216,9 +216,9 @@ structure Ilean where decls : Lsp.Decls deriving FromJson, ToJson -/-- Extra data stored with an `.ilean` loaded and written to disk for mmapping -/ +/-- Extra metadata data stored with a loaded `.ilean` and written to disk for mmaped load -/ structure Milean extends Ilean where - /-- The `.ilean.hash` value, as computed by Lake.fetchFileHash from the `.ilean` JSON. -/ + /-- The `.ilean.hash` value for the stored `.ilean`, if it existed when the `Milean` was created. -/ hash : Option UInt64 /-- From 085ab16fb4e0052297ec53aa747f3404fb2d1fc1 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sun, 19 Jul 2026 07:35:03 -0400 Subject: [PATCH 3/3] avoid visiting an ilean more than once, because there's a significant penalty to opening the same .ilean.mem file multiple times --- src/Lean/Server/Watchdog.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 94b8cd9f6d53..3dfe04c46719 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -1681,7 +1681,13 @@ def startLoadingReferences (referenceData : Std.Mutex ReferenceData) : IO Unit : let oleanSearchPath ← Lean.searchPathRef.get let mut mileanCount := 0 let mut mileanErrors := 0 + let mut visitedPaths : Std.HashSet String := {} for path in ← oleanSearchPath.findAllWithExt "ilean" do + -- Avoid loading an ilean twice + let realPathString := (← FS.realPath path).toString + if visitedPaths.contains realPathString then continue + visitedPaths := visitedPaths.insert realPathString + let milean : Option Ilean ← try let .some milean ← Milean.load path | pure .none mileanCount := mileanCount + 1