From c7a83273a4499091858183dfebc3d93ecb7b6e17 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 1 Mar 2024 14:57:52 +0100 Subject: [PATCH] fix: load references asynchronously (#3552) In v4.6.0, there was a significant regression in initial server startup performance because the .ilean files got bigger in #3082 and we load the information stored in all .ilean files synchronously when the server starts up. This PR makes this loading asynchronous. The trade-off is that requests that are issued right after the initial server start when the references are not fully loaded yet may yield incomplete results. Benchmark for this in a separate PR soon after this one. --------- Co-authored-by: Sebastian Ullrich --- src/Lean/Server/Watchdog.lean | 36 ++++++++++++++++++++++------------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 7a496fb73532..13603764d890 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -869,23 +869,33 @@ def findWorkerPath : IO System.FilePath := do workerPath := System.FilePath.mk path return workerPath -def loadReferences : IO References := do - let oleanSearchPath ← Lean.searchPathRef.get - let mut refs := References.empty - for path in ← oleanSearchPath.findAllWithExt "ilean" do - try - refs := refs.addIlean path (← Ilean.load path) - catch _ => - -- could be a race with the build system, for example - -- ilean load errors should not be fatal, but we *should* log them - -- when we add logging to the server - pure () - return refs +/-- +Starts loading .ileans present in the search path asynchronously in an IO task. +This ensures that server startup is not blocked by loading the .ileans. +In return, while the .ileans are being loaded, users will only get incomplete +results in requests that need references. +-/ +def startLoadingReferences (references : IO.Ref References) : IO Unit := do + -- Discard the task; there isn't much we can do about this failing, + -- but we should try to continue server operations regardless + let _ ← IO.asTask do + let oleanSearchPath ← Lean.searchPathRef.get + for path in ← oleanSearchPath.findAllWithExt "ilean" do + try + let ilean ← Ilean.load path + references.modify fun refs => + refs.addIlean path ilean + catch _ => + -- could be a race with the build system, for example + -- ilean load errors should not be fatal, but we *should* log them + -- when we add logging to the server + pure () def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do let workerPath ← findWorkerPath let srcSearchPath ← initSrcSearchPath - let references ← IO.mkRef (← loadReferences) + let references ← IO.mkRef .empty + startLoadingReferences references let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap) let i ← maybeTee "wdIn.txt" false i let o ← maybeTee "wdOut.txt" true o