diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 5ac3717..257def4 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -1,4 +1,3 @@ -import Lean import GameServer.EnvExtensions open Lean Meta Elab Command diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 200082c..19313b6 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -1,6 +1,5 @@ -import Lean -import GameServer.Graph import GameServer.AbstractCtx +import GameServer.Graph /-! # Environment extensions diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 9075307..bdacdf6 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -1,11 +1,6 @@ /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/ - -import Lean -import GameServer.EnvExtensions -import GameServer.RpcHandlers -import GameServer.Game - import Lean.Server.FileWorker +import GameServer.Game namespace MyModule open Lean diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index 8d018c9..0674dc8 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -1,8 +1,5 @@ -import Lean -import GameServer.EnvExtensions import GameServer.RpcHandlers - open Lean structure GameServerState := diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index 78304a5..8cdc928 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -1,4 +1,3 @@ -import Lean import GameServer.EnvExtensions import GameServer.InteractiveGoal diff --git a/server/leanserver/GameServer/Watchdog.lean b/server/leanserver/GameServer/Watchdog.lean index 8b6cfca..e3ad48f 100644 --- a/server/leanserver/GameServer/Watchdog.lean +++ b/server/leanserver/GameServer/Watchdog.lean @@ -1,7 +1,6 @@ /- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/ -import Lean -import GameServer.Game import Lean.Server.Watchdog +import GameServer.Game namespace MyServer.Watchdog open Lean diff --git a/server/leanserver/Main.lean b/server/leanserver/Main.lean index 39964b7..d18aac9 100644 --- a/server/leanserver/Main.lean +++ b/server/leanserver/Main.lean @@ -1,6 +1,5 @@ -import GameServer.Watchdog import GameServer.FileWorker - +import GameServer.Watchdog unsafe def main : List String → IO UInt32 := fun args => do let e ← IO.getStderr