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 <[email protected]>

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