also display loading of constants

leanprover-community · Nov 28, 2023 · a57a5af · a57a5af
1 parent 946a7fa
commit a57a5af
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 3 deletions.
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
@@ -458,7 +458,13 @@ export function TypewriterInterface({props}) {
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
-    setLoadingProgress(params.counter)
+    if (params.kind == "loadConstants") {
+      setLoadingProgress(params.counter/100*50)
+    } else if (params.kind == "finalizeExtensions") {
+      setLoadingProgress(50 + params.counter/150*50)
+    } else {
+      console.error(`Unknown loading kind: ${params.kind}`)
+    }
   })
 
   return <div className="typewriter-interface">
@@ -527,7 +533,7 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress variant="determinate" value={loadingProgress/1.5 + 30} />
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
         }
       </div>
     </div>

diff --git a/server/GameServer/ImportModules.lean b/server/GameServer/ImportModules.lean
@@ -4,8 +4,12 @@ import Lean.Data.Lsp.Communication
 
 open Lean
 
+inductive LoadingKind := | finalizeExtensions | loadConstants
+  deriving ToJson
+
 structure LoadingParams : Type where
   counter : Nat
+  kind : LoadingKind
   deriving ToJson
 
 -- Code adapted from `Lean/Environment.lean`
@@ -33,7 +37,9 @@ private partial def finalizePersistentExtensions' (env : Environment) (mods : Ar
   loop 0 env
 where
   loop (i : Nat) (env : Environment) : IO Environment := do
-    (← IO.getStdout).writeLspNotification { method := "$/game/loading", param := {counter := i : LoadingParams} }
+    (← IO.getStdout).writeLspNotification {
+      method := "$/game/loading",
+      param := {counter := i, kind := .finalizeExtensions : LoadingParams} }
     -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions.
     let pExtDescrs ← persistentEnvExtensionsRef.get
     if i < pExtDescrs.size then
@@ -61,6 +67,11 @@ def finalizeImport' (s : ImportState) (imports : Array Import) (opts : Options)
   let mut const2ModIdx : HashMap Name ModuleIdx := mkHashMap (capacity := numConsts)
   let mut constantMap : HashMap Name ConstantInfo := mkHashMap (capacity := numConsts)
   for h:modIdx in [0:s.moduleData.size] do
+    if modIdx % 100 = 0 then
+      let percentage := modIdx * 100 / s.moduleData.size
+      (← IO.getStdout).writeLspNotification {
+        method := "$/game/loading",
+        param := {counter := percentage, kind := .loadConstants : LoadingParams} }
     let mod := s.moduleData[modIdx]'h.upper
     for cname in mod.constNames, cinfo in mod.constants do
       match constantMap.insert' cname cinfo with