Merge branch 'dev' into world_overviews

2023-12-10 00:18:47 +01:00
parent 4266c090db 527f58e3a4
commit bb214f426b
61 changed files with 3357 additions and 1699 deletions
@@ -46,7 +46,9 @@ elab "Title" t:str : command => do
  match ← getCurLayer with
  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with title := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with
+      title := t.getString
+      tile := {game.tile with title := t.getString}}

 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
@@ -58,10 +60,32 @@ elab "Introduction" t:str : command => do
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
  match ← getCurLayer with
-  | .Level => pure ()
-  | .World => pure ()
+  | .Level =>
+    logError "Can't use `Info` in a level!"
+    pure ()
+  | .World =>
+    logError "Can't use `Info` in a world"
+    pure ()
  | .Game => modifyCurGame  fun game => pure {game with info := t.getString}

+/-- Provide the location of the image for the current game/world/level.
+Paths are relative to the lean project's root. -/
+elab "Image" t:str : command => do
+  let file := t.getString
+  if not <| ← System.FilePath.pathExists file then
+    logWarningAt t s!"Make sure the cover image '{file}' exists."
+  if not <| file.startsWith "images/" then
+    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
+
+  match ← getCurLayer with
+  | .Level =>
+    logWarning "Level-images not implemented yet" -- TODO
+    modifyCurLevel fun level => pure {level with image := file}
+  | .World =>
+    modifyCurWorld  fun world => pure {world with image := file}
+  | .Game =>
+    logWarning "Main image of the game not implemented yet" -- TODO
+    modifyCurGame  fun game => pure {game with image := file}

 /-- Define the conclusion of the current game or current level if some
 building a level. -/
@@ -71,6 +95,38 @@ elab "Conclusion" t:str : command => do
  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}

+/-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
+elab "Prerequisites" t:str* : command => do
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with prerequisites := t.map (·.getString) |>.toList}}
+
+/-- Short caption for the game (1 sentence) -/
+elab "CaptionShort" t:str : command => do
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with short := t.getString}}
+
+/-- More detailed description what the game is about (2-4 sentences). -/
+elab "CaptionLong" t:str : command => do
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with long := t.getString}}
+
+/-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
+NOTE: For the time being, only a single language is supported.
+ -/
+elab "Languages" t:str* : command => do
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with languages := t.map (·.getString) |>.toList}}
+
+/-- The Image of the game (optional). TODO: Not impementeds -/
+elab "CoverImage" t:str : command => do
+  let file := t.getString
+  if not <| ← System.FilePath.pathExists file then
+    logWarningAt t s!"Make sure the cover image '{file}' exists."
+  if not <| file.startsWith "images/" then
+    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
+
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with image := file}}

 /-! # Inventory

@@ -215,7 +271,7 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 * The identifier after `in` is the category to group lemmas by (in the Inventory).
 * The description is a string supporting Markdown.

-Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requries
+Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
 The lemma/definition to have the same fully qualified name as in mathlib.
 -/
 elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
@@ -243,7 +299,7 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The string following `as` is the displayed name (in the Inventory).
 * The description is a string supporting Markdown.

-Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requries
+Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
 The lemma/definition to have the same fully qualified name as in mathlib.
 -/
 elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
@@ -521,7 +577,7 @@ elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(t
  let mut strict := false
  let mut hidden := false

-  -- remove spaces at the beginngng of new lines
+  -- remove spaces at the beginning of new lines
  let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
    match m with
    | Syntax.node info k args =>
@@ -589,7 +645,7 @@ elab (name := GameServer.Tactic.Hole) "Hole" t:tacticSeq : tactic => do

 /--
 Iterate recursively through the Syntax, replace `Hole` with `sorry` and remove all
-`Hint`/`Branch` occurences.
+`Hint`/`Branch` occurrences.
 -/
 def replaceHoles (tacs : Syntax) : Syntax :=
  match tacs with
@@ -603,7 +659,7 @@ where filterArgs (args : List Syntax) : List Syntax :=
    -- replace `Hole` with `sorry`.
    | Syntax.node info `GameServer.Tactic.Hole _ :: r =>
      Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
-    -- delete all `Hint` and `Branch` occurences in the middle.
+    -- delete all `Hint` and `Branch` occurrences in the middle.
    | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
    | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
      filterArgs r
@@ -626,6 +682,27 @@ elab "Template" tacs:tacticSeq : tactic => do
  modifyLevel (←getCurLevelId) fun level => do
    return {level with template := s!"{template}"}

+
+
+open IO.FS System FilePath in
+/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
+def copyImages : IO Unit := do
+  let target : FilePath := ".lake" / "gamedata"
+  if ← FilePath.pathExists "images" then
+    for file in ← walkDir "images" do
+      let outFile := target.join file
+      -- create the directories
+      if ← file.isDir then
+        createDirAll outFile
+      else
+        if let some parent := outFile.parent then
+          createDirAll parent
+        -- copy file
+        let content ← readBinFile file
+        writeBinFile outFile content
+
+
+
 -- TODO: Notes for testing if a declaration has the simp attribute

 -- -- Test: From zulip
@@ -644,6 +721,47 @@ elab "Template" tacs:tacticSeq : tactic => do

 /-! # Make Game -/

+#eval IO.FS.createDirAll ".lake/gamedata/"
+
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
+  let game ← getCurGame
+  let env ← getEnv
+  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+
+  if ← path.isDir then
+    IO.FS.removeDirAll path
+  IO.FS.createDirAll path
+
+  -- copy the images folder
+  copyImages
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    for (levelId, level) in world.levels.toArray do
+      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+
+  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+
+  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
+    for name in allItemsByType.findD inventoryType {} do
+      let some item ← getInventoryItem? name inventoryType
+        | throwError "Expected item to exist: {name}"
+      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := ← getTiles .Lemma
+    tactics := ← getTiles .Tactic
+    definitions := ← getTiles .Definition
+    lemmaTab := none
+  }
+  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
+
+
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
@@ -810,8 +928,12 @@ elab "MakeGame" : command => do
  -- Items that should not be displayed in inventory
  let mut hiddenItems : HashSet Name := {}

+  let allWorlds := game.worlds.nodes.toArray
+  let nrWorlds := allWorlds.size
+  let mut nrLevels := 0
+
  -- Calculate which "items" are used/new in which world
-  for (worldId, world) in game.worlds.nodes.toArray do
+  for (worldId, world) in allWorlds do
    let mut usedItems : HashSet Name := {}
    let mut newItems : HashSet Name := {}
    for inventoryType in #[.Tactic, .Definition, .Lemma] do
@@ -850,9 +972,12 @@ elab "MakeGame" : command => do
    -- logInfo m!"{worldId} uses: {usedItems.toList}"
    -- logInfo m!"{worldId} introduces: {newItems.toList}"

+    -- Moreover, count the number of levels in the game
+    nrLevels := nrLevels + world.levels.toArray.size
+
  /- for each "item" this is a HashSet of `worldId`s that introduce this item -/
  let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
-  for (worldId, _world) in game.worlds.nodes.toArray do
+  for (worldId, _world) in allWorlds do
    for newItem in newItemsInWorld.findD worldId {} do
      worldsWithNewItem := worldsWithNewItem.insert newItem $
        (worldsWithNewItem.findD newItem {}).insert worldId
@@ -864,7 +989,7 @@ elab "MakeGame" : command => do
  let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {}

  -- Calculate world dependency graph `game.worlds`
-  for (dependentWorldId, _dependentWorld) in game.worlds.nodes.toArray do
+  for (dependentWorldId, _dependentWorld) in allWorlds do
    let mut dependsOnWorlds : HashSet Name := {}
    -- Adding manual dependencies that were specified via the `Dependency` command.
    for (sourceId, targetId) in game.worlds.edges do
@@ -915,14 +1040,25 @@ elab "MakeGame" : command => do
        logError m!"{w1} depends on {w2} because of {items.toList}."
  else
    worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
+
+    -- need to delete all existing edges as they are already present in `worldDependsOnWorlds`.
+    modifyCurGame fun game =>
+      pure {game with worlds := {game.worlds with edges := Array.empty}}
+
    for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
      modifyCurGame fun game =>
        pure {game with worlds := {game.worlds with
          edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}}

+  -- Add the number of levels and worlds to the tile for the landing page
+  modifyCurGame fun game => pure {game with tile := {game.tile with
+    levels := nrLevels
+    worlds := nrWorlds }}
+
  -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
  let game ← getCurGame

+  let mut allItemsByType : HashMap InventoryType (HashSet Name) := {}
  -- Compute which inventory items are available in which level:
  for inventoryType in #[.Tactic, .Definition, .Lemma] do

@@ -1052,6 +1188,9 @@ elab "MakeGame" : command => do

        modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
          return level.setComputedInventory inventoryType itemsArray
+    allItemsByType := allItemsByType.insert inventoryType allItems
+
+  saveGameData allItemsByType

 /-! # Debugging tools -/

@@ -67,7 +67,7 @@ structure InventoryTemplate where
  /-- Depends on the type:
  * Tactic: the tactic's name
  * Lemma: fully qualified lemma name
-  * Definition: no restrictions (preferrably the definions fully qualified name)
+  * Definition: no restrictions (preferably the definitions fully qualified name)
  -/
  name: Name
  /-- Only for Lemmas. To sort them into tabs -/
@@ -108,6 +108,12 @@ structure InventoryTile where
  hidden := false
 deriving ToJson, FromJson, Repr, Inhabited

+def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
+      name := item.name,
+      displayName := item.displayName
+      category := item.category
+}
+
 /-- The extension that stores the doc templates. Note that you can only add, but never modify
 entries! -/
 initialize inventoryTemplateExt :
@@ -135,7 +141,12 @@ def getInventoryItem? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
    m (Option InventoryItem) := do
  return (inventoryExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)

-
+structure InventoryOverview where
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  lemmaTab : Option String
+deriving ToJson, FromJson

 /-! ## Environment extensions for game specification -/

@@ -254,7 +265,9 @@ structure GameLevel where
  lemmas: InventoryInfo := default
  /-- A proof template that is printed in an empty editor. -/
  template: Option String := none
-  deriving Inhabited, Repr
+  /-- The image for this level. -/
+  image : String := default
+deriving Inhabited, Repr

 structure WorldOverview where
  world: Name
@@ -263,6 +276,58 @@ structure WorldOverview where
  lemmas: Array InventoryTile := default
  deriving FromJson, ToJson, Inhabited, Repr

+/-- Json-encodable version of `GameLevel`
+Fields:
+- description: Lemma in mathematical language.
+- descriptionGoal: Lemma printed as Lean-Code.
+-/
+structure LevelInfo where
+  index : Nat
+  title : String
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  introduction : String
+  conclusion : String
+  descrText : Option String := none
+  descrFormat : String := ""
+  lemmaTab : Option String
+  displayName : Option String
+  statementName : Option String
+  template : Option String
+  image: Option String
+deriving ToJson, FromJson
+
+def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
+  { index := lvl.index,
+    title := lvl.title,
+    tactics := lvl.tactics.tiles,
+    lemmas := lvl.lemmas.tiles,
+    definitions := lvl.definitions.tiles,
+    descrText := lvl.descrText,
+    descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
+    introduction := lvl.introduction
+    conclusion := lvl.conclusion
+    lemmaTab := match lvl.lemmaTab with
+    | some tab => tab
+    | none =>
+      -- Try to set the lemma tab to the category of the first added lemma
+      match lvl.lemmas.tiles.find? (·.new) with
+      | some tile => tile.category
+      | none => none
+    statementName := lvl.statementName.toString
+    displayName := match lvl.statementName with
+      | .anonymous => none
+      | name => match (inventoryExt.getState env).find?
+          (fun x => x.name == name && x.type == .Lemma) with
+        | some n => n.displayName
+        | none => name.toString
+        -- Note: we could call `.find!` because we check in `Statement` that the
+        -- lemma doc must exist.
+    template := lvl.template
+    image := lvl.image
+  }
+
 /-! ## World -/

 /-- A world is a collection of levels, like a chapter. -/
@@ -277,17 +342,46 @@ structure World where
  conclusion : String := default
  /-- The levels of the world. -/
  levels: HashMap Nat GameLevel := default
+  /-- The introduction image of the world. -/
+  image: String := default
 deriving Inhabited

 instance : ToJson World := ⟨
  fun world => Json.mkObj [
    ("name", toJson world.name),
    ("title", world.title),
-    ("introduction", world.introduction)]
+    ("introduction", world.introduction),
+    ("image", world.image)]
 ⟩

 /-! ## Game -/

+/-- A tile as they are displayed on the servers landing page. -/
+structure GameTile where
+  /-- The title of the game -/
+  title: String
+  /-- One catch phrase about the game -/
+  short: String := default
+  /-- One paragraph description what the game is about -/
+  long: String := default
+  /-- List of languages the game supports
+
+  TODO: What's the expectected format
+  TODO: Must be a list with a single language currently
+   -/
+  languages: List String := default
+  /-- A list of games which this one builds upon -/
+  prerequisites: List String := default
+  /-- Number of worlds in the game -/
+  worlds: Nat := default
+  /-- Number of levels in the game -/
+  levels: Nat := default
+  /-- A cover image of the game
+
+  TODO: What's the format? -/
+  image: String := default
+deriving Inhabited, ToJson
+
 structure Game where
  /-- Internal name of the game. -/
  name : Name
@@ -302,8 +396,19 @@ structure Game where
  /-- TODO: currently unused. -/
  authors : List String := default
  worlds : Graph Name World := default
+  /-- The tile displayed on the server's landing page. -/
+  tile : GameTile := default
+  /-- The path to the background image of the world. -/
+  image : String := default
 deriving Inhabited, ToJson

+def getGameJson (game : «Game») : Json := Id.run do
+  let gameJson : Json := toJson game
+  -- Add world sizes to Json object
+  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
+  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
+  return gameJson
+
 /-! ## Game environment extension -/

 def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :
@@ -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
@@ -292,7 +293,7 @@ where
    -- TODO(MH): check for interrupt with increased precision
    cancelTk.check
    /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while prefering newer versions over old ones. The former is necessary because we do
+      while preferring newer versions over old ones. The former is necessary because we do
      not explicitly clear older diagnostics, while the latter is necessary because we do
      not guarantee that diagnostics are emitted in order. Specifically, it may happen that
      we interrupted this elaboration task right at this point and a newer elaboration task
@@ -300,7 +301,7 @@ where
      the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
      because we cannot guarantee that no further diagnostics are emitted after clearing
      them. -/
-    -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
+    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
    -- because empty diagnostics clear existing error/information squiggles. Therefore we always
    -- want to publish in case there was previously a message at this position.
    publishDiagnostics m snap.diagnostics.toArray ctx.hOut
@@ -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
@@ -496,7 +497,7 @@ section NotificationHandling
      IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
    else if ¬ changes.isEmpty then
      let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩

 end NotificationHandling

@@ -573,7 +574,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
    This is because LSP always refers to characters by (line, column),
    so if we get the line number correct it shouldn't matter that there
    is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
  let e := e.withPrefix s!"[{param.textDocument.uri}] "
  let _ ← IO.setStderr e
  try
@@ -25,53 +25,6 @@ open Lsp
 open JsonRpc
 open IO

-def getGame (game : Name): GameServerM Json := do
-  let some game ← getGame? game
-    | throwServerError "Game not found"
-  let gameJson : Json := toJson game
-  -- Add world sizes to Json object
-  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
-  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
-  return gameJson
-
-/--
-Fields:
- description: Lemma in mathematical language.
- descriptionGoal: Lemma printed as Lean-Code.
-/
-structure LevelInfo where
-  index : Nat
-  title : String
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  introduction : String
-  conclusion : String
-  descrText : Option String := none
-  descrFormat : String := ""
-  lemmaTab : Option String
-  displayName : Option String
-  statementName : Option String
-  template : Option String
-deriving ToJson, FromJson
-
-structure InventoryOverview where
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  lemmaTab : Option String
-deriving ToJson, FromJson
-
-structure LoadLevelParams where
-  world : Name
-  level : Nat
-  deriving ToJson, FromJson
-
-- structure LoadTemplateParams where
--   world : Name
--   level : Nat
--   deriving ToJson, FromJson
-
 structure DidOpenLevelParams where
  uri : String
  gameDir : String
@@ -91,11 +44,6 @@ structure DidOpenLevelParams where
  statementName : Name
  deriving ToJson, FromJson

-structure LoadDocParams where
-  name : Name
-  type : InventoryType
-deriving ToJson, FromJson
-
 structure SetInventoryParams where
  inventory : Array String
  difficulty : Nat
@@ -131,86 +79,10 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
    }
  }

-
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
  match ev with
  | ServerEvent.clientMsg msg =>
    match msg with
-    | Message.request id "info" _ =>
-      let s ← get
-      let c ← read
-      c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩
-      return true
-    | Message.request id "loadLevel" params =>
-      let p ← parseParams LoadLevelParams (toJson params)
-      let s ← get
-      let c ← read
-      let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
-        | do
-          c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
-          return true
-
-      let env ← getEnv
-
-      let levelInfo : LevelInfo :=
-          { index := lvl.index,
-            title := lvl.title,
-            tactics := lvl.tactics.tiles,
-            lemmas := lvl.lemmas.tiles,
-            definitions := lvl.definitions.tiles,
-            descrText := lvl.descrText,
-            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
-            introduction := lvl.introduction
-            conclusion := lvl.conclusion
-            lemmaTab := match lvl.lemmaTab with
-            | some tab => tab
-            | none =>
-              -- Try to set the lemma tab to the category of the first added lemma
-              match lvl.lemmas.tiles.find? (·.new) with
-              | some tile => tile.category
-              | none => none
-            statementName := lvl.statementName.toString
-            displayName := match lvl.statementName with
-              | .anonymous => none
-              | name => match (inventoryExt.getState env).find?
-                  (fun x => x.name == name && x.type == .Lemma) with
-                | some n => n.displayName
-                | none => name.toString
-                -- Note: we could call `.find!` because we check in `Statement` that the
-                -- lemma doc must exist.
-            template := lvl.template
-            }
-      c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
-      return true
-    -- | Message.request id "loadTemplate" params =>
-    --   let p ← parseParams LoadTemplateParams (toJson params)
-    --   let s ← get
-    --   let c ← read
-
-    --   let some game ← getGame? s.game
-    --     | throwServerError "Game not found"
-    --   let some world := game.worlds.nodes.find? p.world
-    --     | throwServerError "World not found"
-
-    --   let mut templates : Array <| Option String := #[]
-    --   for (_, level) in world.levels.toArray do
-    --     templates := templates.push level.template
-    --   c.hOut.writeLspResponse ⟨id, ToJson.toJson templates⟩
-    --   return true
-    | Message.request id "loadDoc" params =>
-      let p ← parseParams LoadDocParams (toJson params)
-      let c ← read
-      let some doc ← getInventoryItem? p.name p.type
-        | do
-            c.hOut.writeLspResponseError ⟨id, .invalidParams,
-              s!"Documentation not found: {p.name}", none⟩
-            return true
-      -- TODO: not necessary at all?
-      -- Here we only need to convert the fields that were not `String` in the `InventoryDocEntry`
-      -- let doc : InventoryItem := { doc with
-      --   name := doc.name.toString }
-      c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
-      return true
    | Message.notification "$/game/setInventory" params =>
      let p := (← parseParams SetInventoryParams (toJson params))
      let s ← get
@@ -0,0 +1,108 @@
+import Lean.Environment
+import Std.Tactic.OpenPrivate
+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`
+
+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, 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
+      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
+    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
+      | (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
@@ -78,7 +78,7 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
  | _, _ => none

 /-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
-def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM (Option FVarBijection) := do
  -- We iterate through the array backwards hoping that this will find us faster results
  -- TODO: implement backtracking
  let mut bij := initBij
@@ -97,11 +97,11 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
        -- usedFvars := usedFvars.set! (fvars.size - j - 1) true
        bij := bij'.insert pattern.fvarId! fvar.fvarId!
        break
-    if ! bij.forward.contains pattern.fvarId! then return false
+    if ! bij.forward.contains pattern.fvarId! then return none

-  if strict then
-    return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
-  return true
+  if !strict || fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
+  then return some bij
+  else return none

 unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
  evalExpr (Array Expr → MessageData)
@@ -122,10 +122,11 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
        if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
        then
          let lctx := (← goal.getDecl).lctx
-          if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
          then
-            let text := (← evalHintMessage hint.text) hintFVars
-            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+            let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
+            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
+            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
            let text ← (MessageData.withContext ctx text).toString
            return some { text := text, hidden := hint.hidden }
          else return none