From 6a849de3508af2b994a797d7a7819df788c770a9 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 16 Jul 2023 23:41:15 +0200
Subject: [PATCH] fix merge error

---
 server/GameServer/Commands.lean | 49 ---------------------------------
 1 file changed, 49 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 3f31170..49695ae 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -762,55 +762,6 @@ elab "MakeGame" : command => do
   -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
   let game ← getCurGame
 
-  -- Which items are used/new in which world?
-  let mut usedItemsInWorld : HashMap Name (HashSet Name) := {}
-  let mut newItemsInWorld : HashMap Name (HashSet Name) := {}
-  for (worldId, world) in game.worlds.nodes.toArray do
-    let mut usedItems : HashSet Name := {}
-    let mut newItems : HashSet Name := {}
-    for inventoryType in #[.Tactic, .Definition, .Lemma] do
-      for (levelId, level) in world.levels.toArray do
-          usedItems := usedItems.insertMany (level.getInventory inventoryType).used
-          newItems := newItems.insertMany (level.getInventory inventoryType).new
-    usedItemsInWorld := usedItemsInWorld.insert worldId usedItems
-    newItemsInWorld := newItemsInWorld.insert worldId newItems
-
-  let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
-  for (worldId, world) in game.worlds.nodes.toArray do
-    for newItem in newItemsInWorld.find! worldId do
-      worldsWithNewItem := worldsWithNewItem.insert newItem $
-        (worldsWithNewItem.findD newItem {}).insert worldId
-
-  -- which world depends on which world?
-  let mut worldDependsOnWorlds : HashMap Name (HashSet Name) := {}
-  let mut dependencyReason : HashMap (Name × Name) Name := {}
-  for (dependentWorldId, dependentWorld) in game.worlds.nodes.toArray do
-    let mut dependsOnWorlds : HashSet Name := {}
-    for usedItem in usedItemsInWorld.find! dependentWorldId do
-      match worldsWithNewItem.find? usedItem with
-      | some worldIds =>
-        if !worldIds.contains dependentWorldId then
-          dependsOnWorlds := dependsOnWorlds.insertMany worldIds
-          for worldId in worldIds do
-            dependencyReason := dependencyReason.insert (dependentWorldId, worldId) usedItem
-      | none => logWarning m!"No world introducing {usedItem}, but required by {dependentWorldId}"
-    worldDependsOnWorlds := worldDependsOnWorlds.insert dependentWorldId dependsOnWorlds
-
-  let loop := findLoops worldDependsOnWorlds
-  if loop != [] then
-    logError m!"Loop: Dependency graph has a loop: {loop}"
-    for i in [:loop.length] do
-      let w1 := loop[i]!
-      let w2 := loop[if i == loop.length - 1 then 0 else i + 1]!
-      let item := dependencyReason.find! (w1, w2)
-      logError m!"{w1} depends on {w2} because of {item}"
-  else
-    worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
-    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))}}
-
   -- Compute which inventory items are available in which level:
   for inventoryType in #[.Tactic, .Definition, .Lemma] do