From f6727e5c9f7f638fa05c6ce60d4a11e07682ecdb Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 28 Nov 2023 11:40:00 +0100 Subject: [PATCH] loading progress --- client/src/components/infoview/main.tsx | 8 +- server/GameServer/FileWorker.lean | 3 +- server/GameServer/ImportModules.lean | 97 +++++++++++++++++++++++++ server/lake-manifest.json | 11 ++- server/lakefile.lean | 2 + 5 files changed, 118 insertions(+), 3 deletions(-) create mode 100644 server/GameServer/ImportModules.lean diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index ab670a1..951d3a1 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -347,6 +347,7 @@ export function TypewriterInterface({props}) { const uri = model.uri.toString() const [disableInput, setDisableInput] = React.useState(false) + const [loadingProgress, setLoadingProgress] = React.useState(0) const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) const {mobile} = React.useContext(MobileContext) const { proof } = React.useContext(ProofContext) @@ -455,6 +456,11 @@ export function TypewriterInterface({props}) { let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false + + useServerNotificationEffect("$/game/loading", (params : any) => { + setLoadingProgress(params.counter) + }) + return
@@ -521,7 +527,7 @@ export function TypewriterInterface({props}) { }
} - : + : }
diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 0cca9c1..43abb73 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -1,6 +1,7 @@ /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/ import Lean.Server.FileWorker import GameServer.Game +import GameServer.ImportModules namespace MyModule open Lean @@ -412,7 +413,7 @@ section Initialization -- Set the search path Lean.searchPathRef.set paths - let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0 + let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] -- return (env, paths) -- use empty header diff --git a/server/GameServer/ImportModules.lean b/server/GameServer/ImportModules.lean new file mode 100644 index 0000000..65cbafc --- /dev/null +++ b/server/GameServer/ImportModules.lean @@ -0,0 +1,97 @@ +import Lean.Environment +import Std.Tactic.OpenPrivate +import Lean.Data.Lsp.Communication + +open Lean + +structure LoadingParams : Type where + counter : Nat + deriving ToJson + +-- Code adapted from `Lean/Environment.lean` + +partial def importModulesCore' (imports : Array Import) : ImportStateM Unit := do + for i in imports do + if i.runtimeOnly || (← get).moduleNameSet.contains i.module then + continue + modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module } + let mFile ← findOLean i.module + unless (← mFile.pathExists) do + throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist" + let (mod, region) ← readModuleData mFile + importModulesCore' mod.imports + modify fun s => { s with + moduleData := s.moduleData.push mod + regions := s.regions.push region + moduleNames := s.moduleNames.push i.module + } + +open private mkInitialExtensionStates Environment.mk setImportedEntries finalizePersistentExtensions + ensureExtensionsArraySize from Lean.Environment + +private partial def finalizePersistentExtensions' (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do + loop 0 env +where + loop (i : Nat) (env : Environment) : IO Environment := do + (← IO.getStdout).writeLspNotification { method := "$/game/loading", param := {counter := i : 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 + let extDescr := pExtDescrs[i]! + let s := extDescr.toEnvExtension.getState env + let prevSize := (← persistentEnvExtensionsRef.get).size + let prevAttrSize ← getNumBuiltinAttributes + let newState ← extDescr.addImportedFn s.importedEntries { env := env, opts := opts } + let mut env := extDescr.toEnvExtension.setState env { s with state := newState } + env ← ensureExtensionsArraySize env + if (← persistentEnvExtensionsRef.get).size > prevSize || (← getNumBuiltinAttributes) > prevAttrSize then + -- This branch is executed when `pExtDescrs[i]` is the extension associated with the `init` attribute, and + -- a user-defined persistent extension is imported. + -- Thus, we invoke `setImportedEntries` to update the array `importedEntries` with the entries for the new extensions. + env ← setImportedEntries env mods prevSize + -- See comment at `updateEnvAttributesRef` + env ← updateEnvAttributes env + loop (i + 1) env + else + return env + +def finalizeImport' (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := do + let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod => + numConsts + mod.constants.size + mod.extraConstNames.size + 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 + let mod := s.moduleData[modIdx]'h.upper + for cname in mod.constNames, cinfo in mod.constants do + match constantMap.insert' cname cinfo with + | (constantMap', replaced) => + constantMap := constantMap' + if replaced then + throwAlreadyImported s const2ModIdx modIdx cname + const2ModIdx := const2ModIdx.insert cname modIdx + for cname in mod.extraConstNames do + const2ModIdx := const2ModIdx.insert cname modIdx + let constants : ConstMap := SMap.fromHashMap constantMap false + let exts ← mkInitialExtensionStates + let env : Environment := Environment.mk + (const2ModIdx := const2ModIdx) + (constants := constants) + (extraConstNames := {}) + (extensions := exts) + (header := { + quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module + trustLevel := trustLevel + imports := imports + regions := s.regions + moduleNames := s.moduleNames + moduleData := s.moduleData + }) + + let env ← setImportedEntries env s.moduleData + finalizePersistentExtensions' env s.moduleData opts + +def importModules' (imports : Array Import) : IO Environment := do + withImporting do + let (_, s) ← importModulesCore' imports |>.run + let env ← finalizeImport' s imports {} 0 + return env diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 48f0d7b..9e9b6bb 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -1,5 +1,14 @@ {"version": 7, "packagesDir": ".lake/packages", - "packages": [], + "packages": + [{"url": "https://github.com/leanprover/std4.git", + "type": "git", + "subDir": null, + "rev": "bf8a6ea960d5a99f8e30cbf5597ab05cd233eadf", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}], "name": "GameServer", "lakeDir": ".lake"} diff --git a/server/lakefile.lean b/server/lakefile.lean index 4ffee6f..c11a3db 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -3,6 +3,8 @@ open Lake DSL package GameServer +require std from git "https://github.com/leanprover/std4.git" + lean_lib GameServer @[default_target]