diff --git a/.env b/.env deleted file mode 100644 index 01fee6b..0000000 --- a/.env +++ /dev/null @@ -1 +0,0 @@ -LEAN4GAME_SINGLE_GAME=false diff --git a/.gitignore b/.gitignore index a3629ab..9508154 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,6 @@ node_modules +games/ client/dist -server/build -server/tmp -server/lakefile.olean -**/lake-packages/ +games/ +server/.lake **/.DS_Store diff --git a/README.md b/README.md index da77885..5ee0d7f 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, * Step 5: [How to Run Games Locally](doc/running_locally.md) * Step 7: [How to Update an existing Game](doc/update_game.md) +* Step 8: [How to Publishing a Game](doc/publish_game.md) ### Publishing a Game diff --git a/client/src/app.tsx b/client/src/app.tsx index c45f6d0..8420d4b 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -10,6 +10,7 @@ import './css/reset.css'; import './css/app.css'; import { MobileContext } from './components/infoview/context'; import { useWindowDimensions } from './window_width'; +import { connection } from './connection'; export const GameIdContext = React.createContext(undefined); @@ -19,6 +20,10 @@ function App() { const {width, height} = useWindowDimensions() const [mobile, setMobile] = React.useState(width < 800) + React.useEffect(() => { + connection.startLeanClient(gameId); + }, [gameId]) + return (
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index ab670a1..b77c395 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,17 @@ export function TypewriterInterface({props}) { let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false + + useServerNotificationEffect("$/game/loading", (params : any) => { + 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
@@ -521,7 +533,7 @@ export function TypewriterInterface({props}) { }
} - : + : }
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 806082d..922fddb 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -48,7 +48,6 @@ function Level() { const params = useParams() const levelId = parseInt(params.levelId) const worldId = params.worldId - // useLoadWorldFiles(worldId) const [impressum, setImpressum] = React.useState(false) @@ -615,6 +614,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange return () => { editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}}) + model.dispose(); } } }, [editor, levelId, connection, leanClientStarted]) @@ -637,27 +637,3 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange return {editor, infoProvider, editorConnection} } - -/** Open all files in this world on the server so that they will load faster when accessed */ -function useLoadWorldFiles(worldId) { - const gameId = React.useContext(GameIdContext) - const gameInfo = useGetGameInfoQuery({game: gameId}) - const store = useStore() - - useEffect(() => { - if (gameInfo.data) { - const models = [] - for (let levelId = 1; levelId <= gameInfo.data.worldSize[worldId]; levelId++) { - const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`) - let model = monaco.editor.getModel(uri) - if (model) { - models.push(model) - } else { - const code = selectCode(gameId, worldId, levelId)(store.getState()) - models.push(monaco.editor.createModel(code, 'lean4', uri)) - } - } - return () => { for (let model of models) { model.dispose() } } - } - }, [gameInfo.data, worldId]) -} diff --git a/client/src/index.tsx b/client/src/index.tsx index 9367f4c..c42b6dc 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -34,6 +34,11 @@ const router = createHashRouter([ path: "/game/nng", loader: () => redirect("/g/hhu-adam/NNG4") }, + { + // For backwards compatibility + path: "/g/hhu-adam/NNG4", + loader: () => redirect("/g/leanprover-community/NNG4") + }, { path: "/g/:owner/:repo", element: , diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 725c7ad..a37ca5e 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -2,7 +2,6 @@ * @fileOverview Define API of the server-client communication */ import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react' -import { Connection } from '../connection' export interface GameInfo { title: null|string, @@ -57,40 +56,22 @@ interface Doc { category: string, } - -const customBaseQuery = async ( - args : {game: string, method: string, params?: any}, - { signal, dispatch, getState, extra }, - extraOptions -) => { - try { - const connection : Connection = extra.connection - let leanClient = await connection.startLeanClient(args.game) - console.log(`Sending request ${args.method}`) - let res = await leanClient.sendRequest(args.method, args.params) - console.log('Received response') //, res) - return {'data': res} - } catch (e) { - return {'error': e} - } -} - // Define a service using a base URL and expected endpoints export const apiSlice = createApi({ reducerPath: 'gameApi', - baseQuery: customBaseQuery, + baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/api" }), endpoints: (builder) => ({ getGameInfo: builder.query({ - query: ({game}) => {return {game, method: 'info', params: {}}}, + query: ({game}) => `${game}/game`, }), loadLevel: builder.query({ - query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}}, + query: ({game, world, level}) => `${game}/level/${world}/${level}`, }), loadInventoryOverview: builder.query({ - query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}}, + query: ({game}) => `${game}/inventory`, }), loadDoc: builder.query({ - query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}}, + query: ({game, type, name}) => `${game}/doc/${type}/${name}`, }), }), }) diff --git a/doc/create_game.md b/doc/create_game.md index 86bf0a2..0bf24d1 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -245,7 +245,11 @@ That way, the game will replace it with the actual name the assumption has in th ## 7. Update your game -In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md). +In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md). + +## 8. Publish your game + +To publish your game on the official server, see [Publishing a game](doc/publish_game.md) ## Further Notes diff --git a/doc/publish_game.md b/doc/publish_game.md new file mode 100644 index 0000000..684f5d6 --- /dev/null +++ b/doc/publish_game.md @@ -0,0 +1,30 @@ +# Publishing games + +You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple +steps. + +## 1. Upload Game to github + +First, you need your game in a public Github repository and make sure the github action has run. +You can check this by spotting the green checkmark on the start page, or by looking at the "Actions" +tab. + +## 2. Import the game + +You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call +the URL of the form + +> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY} + +where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name. + +You should see a white screen which shows import updates and eventually reports "Done." + +## 3. Play the game + +Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`! + +## 4. Main page + +Adding games to the main page happens manually by the server maintainers. Tell us if you want us +to add a tile for your game! diff --git a/doc/server.md b/doc/server.md new file mode 100644 index 0000000..41698a0 --- /dev/null +++ b/doc/server.md @@ -0,0 +1,28 @@ + +# Notes for Server maintainer + +In order to set up the server to allow imports, one needs to create a +[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public +repos will suffice. + +You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN` +with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if +you're using `pm2` + +Then people can call: + +> https://{website}/import/trigger/{owner}/{repo} + +where you replace: +- website: The website your server runs on, e.g. `localhost:3000` +- owner, repo: The owner and repository name of the game you want to load from github. + + will trigger to download the latest version of your game from github onto your server. + Once this import reports "Done", you should be able to play your game under: + +> https://{website}/#/g/{owner}/{repo} + +## data management +Everything downloaded remains in the folder `lean4game/games`. +the subfolder `tmp` contains downloaded artifacts and can be deleted without loss. +The other folders should only contain the built lean-games, sorted by owner and repo. diff --git a/doc/update_game.md b/doc/update_game.md index 1a18d58..8fcb037 100644 --- a/doc/update_game.md +++ b/doc/update_game.md @@ -10,10 +10,24 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https: Then, depending on the setup you use, do one of the following: * Dev Container: Rebuild the VSCode Devcontainer. -* Local Setup: run `lake update -R` (followed by `lake exe cache get` if you depend on mathlib.) +* Local Setup: run + ``` + lake update -R + lake build + ``` + in your game folder. + + * Additionally, if you have a local copy of the server `lean4game`, + you should update this one to the matching version, too: + ``` + git fetch + git checkout {VERSION_TAG} + npm install + ``` + where `{VERSION_TAG}` is the tag from above of the form `v4.X.0` * Gitpod/Codespaces: Create a fresh one -This will update `lean4game` and `mathlib` in your project to the new lean version. +This will your game (and the mathlib version you might be using) to the new lean version. ## Newest developing setup @@ -24,14 +38,16 @@ anymore, you will need to copy the relevant files from the [GameSkeleton](https: The relevant files are: ``` +.devcontainer/ +.docker/ +.github/ +.gitpod/ +.vscode/ lakefile.lean -.devcontainer/** -.docker/** -.gitpod -.vscode/** ``` -simply copy them from the `GameSkeleton` into your game. +simply copy them from the `GameSkeleton` into your game and proceed as above, +i.e. `lake update -R && lake build`. (Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`, -where you need to add any dependencies of your game.) +where you need to add any dependencies of your game, or remove mathlib if you don't need it.) diff --git a/ecosystem.config.js b/ecosystem.config.cjs similarity index 63% rename from ecosystem.config.js rename to ecosystem.config.cjs index 20e44ee..b3665a0 100644 --- a/ecosystem.config.js +++ b/ecosystem.config.cjs @@ -4,8 +4,10 @@ module.exports = { name : "lean4game", script : "server/index.mjs", env: { - NODE_ENV: "production", - PORT: 8002 + LEAN4GAME_GITHUB_USER: "", + LEAN4GAME_GITHUB_TOKEN: "", + NODE_ENV: "production", + PORT: 8002 }, }] } diff --git a/server/.gitignore b/server/.gitignore index 103f95b..6eac252 100644 --- a/server/.gitignore +++ b/server/.gitignore @@ -1,3 +1,3 @@ -build -adam -nng +build/ +games/ +.lake diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 9ccbbb0..d6b9ea5 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -644,6 +644,44 @@ 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 + + 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 @@ -923,6 +961,7 @@ elab "MakeGame" : command => do -- 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 +1091,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 -/ diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index b1662f3..bcef5cc 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -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 -/ @@ -256,6 +267,55 @@ structure GameLevel where template: Option String := none deriving 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 +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 + } /-! ## World -/ @@ -298,6 +358,13 @@ structure Game where worlds : Graph Name World := 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 : β → β → β) : 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/Game.lean b/server/GameServer/Game.lean index 13cc25b..fb59fdb 100644 --- a/server/GameServer/Game.lean +++ b/server/GameServer/Game.lean @@ -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 @@ -221,30 +93,6 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do fw.stdin.writeLspMessage msg return true - | Message.request id "loadInventoryOverview" _ => - let s ← get - let some game ← getGame? s.game - | return false - -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world - -- and reset `new`, `disabled` and `unlocked`. - -- Note: as we allow worlds without any levels (for developing), we might need - -- to try until we find the first world with levels. - for ⟨worldId, _⟩ in game.worlds.nodes.toList do - let some lvl ← getLevel? {game := s.game, world := worldId, level := 1} - | do continue - let inventory : InventoryOverview := { - tactics := lvl.tactics.tiles.map - ({ · with locked := true, disabled := false, new := false }), - lemmas := lvl.lemmas.tiles.map - ({ · with locked := true, disabled := false, new := false }), - definitions := lvl.definitions.tiles.map - ({ · with locked := true, disabled := false, new := false }), - lemmaTab := none - } - let c ← read - c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩ - return true - return false | _ => return false | _ => return false diff --git a/server/GameServer/ImportModules.lean b/server/GameServer/ImportModules.lean new file mode 100644 index 0000000..055bed1 --- /dev/null +++ b/server/GameServer/ImportModules.lean @@ -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 diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index ed6286d..ae71a25 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -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,9 +122,10 @@ 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 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 := ← getLCtx, opts := {}} let text ← (MessageData.withContext ctx text).toString return some { text := text, hidden := hint.hidden } diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh index 7d3f10e..6f6cd20 100755 --- a/server/bubblewrap.sh +++ b/server/bubblewrap.sh @@ -2,11 +2,13 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) + + (exec bwrap\ - --ro-bind ../../lean4game /lean4game \ - --ro-bind ../../$1 /game \ - --ro-bind $ELAN_HOME /elan \ - --ro-bind /usr /usr \ + --bind $2 /lean4game \ + --bind $1 /game \ + --bind $ELAN_HOME /elan \ + --bind /usr /usr \ --dev /dev \ --proc /proc \ --symlink usr/lib /lib\ @@ -22,6 +24,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) --unshare-uts \ --unshare-cgroup \ --die-with-parent \ - --chdir "/lean4game/server/build/bin/" \ + --chdir "/lean4game/server/.lake/build/bin/" \ ./gameserver --server /game ) diff --git a/server/import.mjs b/server/import.mjs index 0ac479e..6643cd7 100644 --- a/server/import.mjs +++ b/server/import.mjs @@ -78,13 +78,20 @@ async function doImport (owner, repo, id) { .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc) artifactId = artifact.id const url = artifact.archive_download_url - if (!fs.existsSync("tmp")){ - fs.mkdirSync("tmp"); + // Make sure the download folder exists + if (!fs.existsSync(`${__dirname}/../games`)){ + fs.mkdirSync(`${__dirname}/../games`); + } + if (!fs.existsSync(`${__dirname}/../games/tmp`)){ + fs.mkdirSync(`${__dirname}/../games/tmp`); } progress[id].output += `Download from ${url}\n` - await download(id, url, `tmp/artifact_${artifactId}.zip`) + await download(id, url, `${__dirname}/../games/tmp/${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`) progress[id].output += `Download finished.\n` - await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId],".") + + await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId, owner.toLowerCase(), repo.toLowerCase()], `${__dirname}/..`) + + // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`); // manifest = JSON.parse(manifest); // if (manifest.length !== 1) { @@ -95,22 +102,21 @@ async function doImport (owner, repo, id) { // await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`) // // await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`]) - - // TODO: not implemented - progress[id].done = true - progress[id].output += `Done.\n` + progress[id].output += `Done!\n` + progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n` } catch (e) { progress[id].output += `Error: ${e.toString()}\n${e.stack}` } finally { - if (artifactId) { - // fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true}); - // fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true}); - // fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true}); - // fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true}); - } + // if (artifactId) { + // // fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true}); + // // fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true}); + // // fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true}); + // // fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true}); + // } progress[id].done = true } + await new Promise(resolve => setTimeout(resolve, 10000)) } export const importTrigger = (req, res) => { diff --git a/server/index.mjs b/server/index.mjs index 2caca9c..0f2ce06 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -6,30 +6,20 @@ import * as url from 'url'; import * as rpc from 'vscode-ws-jsonrpc'; import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'; import os from 'os'; +import fs from 'fs'; import anonymize from 'ip-anonymize'; import { importTrigger, importStatus } from './import.mjs' // import fs from 'fs' /** + * Add a game here if the server should keep a queue of pre-loaded games ready at all times. + * * IMPORTANT! Tags here need to be lower case! */ -const games = { - "g/hhu-adam/robo": { - dir: "Robo", - queueLength: 5 - }, - "g/hhu-adam/nng4": { - dir: "NNG4", - queueLength: 5 - }, - "g/djvelleman/stg4": { - dir: "STG4", - queueLength: 5 - }, - "g/hhu-adam/nng4-old": { - dir: "NNG4-OLD", - queueLength: 0 - } +const queueLength = { + "g/hhu-adam/robo": 2, + "g/hhu-adam/nng4": 5, + "g/djvelleman/stg4": 2, } const __filename = url.fileURLToPath(import.meta.url); @@ -44,6 +34,32 @@ var router = express.Router(); router.get('/import/status/:owner/:repo', importStatus) router.get('/import/trigger/:owner/:repo', importTrigger) +function loadJson(req, filename) { + const owner = req.params.owner; + const repo = req.params.repo + return JSON.parse(fs.readFileSync(path.join(getGameDir(owner,repo),".lake","gamedata",filename))) +} + +router.get("/api/g/:owner/:repo/game", (req, res) => { + res.send(loadJson(req, `game.json`)); +}); + +router.get("/api/g/:owner/:repo/inventory", (req, res) => { + res.send(loadJson(req, `inventory.json`)); +}); + +router.get("/api/g/:owner/:repo/level/:world/:level", (req, res) => { + const world = req.params.world; + const level = req.params.level; + res.send(loadJson(req, `level__${world}__${level}.json`)); +}); + +router.get("/api/g/:owner/:repo/doc/:type/:name", (req, res) => { + const type = req.params.type; + const name = req.params.name; + res.send(loadJson(req, `doc__${type}__${name}.json`)); +}); + const server = app .use(express.static(path.join(__dirname, '../client/dist/'))) .use('/', router) @@ -59,39 +75,50 @@ const isDevelopment = environment === 'development' /** We keep queues of started Lean Server processes to be ready when a user arrives */ const queue = {} -function tag(owner, repo) { +function getTag(owner, repo) { return `g/${owner.toLowerCase()}/${repo.toLowerCase()}` } -function startServerProcess(owner, repo) { - let game_dir = (owner == 'local') ? - repo : games[tag(owner, repo)]?.dir - +function getGameDir(owner, repo) { + owner = owner.toLowerCase() if (owner == 'local') { if(!isDevelopment) { console.error(`No local games in production mode.`) return } - // TODO: This test does not work - // if (!fs.existsSync(path.join("../", game_dir))) { - // console.error(`Game folder does not exists: ${game_dir}`) - // return - // } + } else { + if(!fs.existsSync(path.join(__dirname, '..', 'games'))) { + console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`) + console.error('Did you already import any games?') + return + } } - if (!game_dir) { - console.error(`Unknown game: ${tag(owner, repo)}`) + let game_dir = (owner == 'local') ? + path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive + path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`) + + if(!fs.existsSync(game_dir)) { + console.error(`Game '${game_dir}' does not exist!`) return } + return game_dir; +} + +function startServerProcess(owner, repo) { + + let game_dir = getGameDir(owner, repo) + if (!game_dir) return; + let serverProcess if (isDevelopment) { - let args = ["--server", path.join("../../../../", game_dir)] + let args = ["--server", game_dir] serverProcess = cp.spawn("./gameserver", args, - { cwd: path.join(__dirname, "./build/bin/") }) + { cwd: path.join(__dirname, "./.lake/build/bin/") }) } else { serverProcess = cp.spawn("./bubblewrap.sh", - [game_dir], + [game_dir, path.join(__dirname, '..')], { cwd: __dirname }) } serverProcess.on('error', error => @@ -106,15 +133,21 @@ function startServerProcess(owner, repo) { } /** start Lean Server processes to refill the queue */ -function fillQueue(owner, repo) { - while (queue[tag(owner, repo)].length < games[tag(owner, repo)].queueLength) { - const serverProcess = startServerProcess(tag(owner, repo)) - queue[tag(owner, repo)].push(serverProcess) +function fillQueue(tag) { + while (queue[tag].length < queueLength[tag]) { + let serverProcess + serverProcess = startServerProcess(tag) + if (serverProcess == null) { + console.error('serverProcess was undefined/null') + return } + queue[tag].push(serverProcess) + } } +// // TODO: We disabled queue for now // if (!isDevelopment) { // Don't use queue in development -// for (let tag in games) { +// for (let tag in queueLength) { // queue[tag] = [] // fillQueue(tag) // } @@ -127,19 +160,21 @@ wss.addListener("connection", function(ws, req) { if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; } const owner = reRes[1] const repo = reRes[2] - // const tag = `g/${owner.toLowerCase()}/${repo.toLowerCase()}` - // // TODO - // if (isDevelopment && process.env.DEV_CONTAINER) { - // tag = `g/local/game` - // } + const tag = getTag(owner, repo) - let ps; - if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) { - ps = startServerProcess(owner, repo) + let ps + if (!queue[tag] || queue[tag].length == 0) { + ps = startServerProcess(owner, repo) } else { - ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately - fillQueue(owner, repo) + console.info('Got process from the queue') + ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately + fillQueue(tag) + } + + if (ps == null) { + console.error('server process is undefined/null') + return } socketCounter += 1; @@ -152,14 +187,14 @@ wss.addListener("connection", function(ws, req) { onClose: (cb) => { ws.on("close", cb) }, send: (data, cb) => { ws.send(data,cb) } } - const reader = new rpc.WebSocketMessageReader(socket); - const writer = new rpc.WebSocketMessageWriter(socket); + const reader = new rpc.WebSocketMessageReader(socket) + const writer = new rpc.WebSocketMessageWriter(socket) const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close()) - const serverConnection = jsonrpcserver.createProcessStreamConnection(ps); + const serverConnection = jsonrpcserver.createProcessStreamConnection(ps) socketConnection.forward(serverConnection, message => { if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)} return message; - }); + }) serverConnection.forward(socketConnection, message => { if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)} return message; @@ -170,9 +205,9 @@ wss.addListener("connection", function(ws, req) { ws.on('close', () => { console.log(`[${new Date()}] Socket closed - ${ip}`) - socketCounter -= 1; + socketCounter -= 1 }) - socketConnection.onClose(() => serverConnection.dispose()); - serverConnection.onClose(() => socketConnection.dispose()); + socketConnection.onClose(() => serverConnection.dispose()) + serverConnection.onClose(() => socketConnection.dispose()) }) diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 5c8f511..c73e6a6 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -1,4 +1,14 @@ -{"version": 6, - "packagesDir": "lake-packages", - "packages": [], - "name": "GameServer"} +{"version": 7, + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover/std4.git", + "type": "git", + "subDir": null, + "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.3.0-rc2", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "GameServer", + "lakeDir": ".lake"} diff --git a/server/lakefile.lean b/server/lakefile.lean index 4ffee6f..851c78d 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -3,6 +3,11 @@ open Lake DSL package GameServer +-- Using this assumes that each dependency has a tag of the form `v4.X.0`. +def leanVersion : String := s!"v{Lean.versionString}" + +require std from git "https://github.com/leanprover/std4.git" @ leanVersion + lean_lib GameServer @[default_target] diff --git a/server/lean-toolchain b/server/lean-toolchain index 2f868c6..24a3cdb 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0 +leanprover/lean4:v4.3.0-rc2 diff --git a/server/unpack.sh b/server/unpack.sh old mode 100644 new mode 100755 index 5a765db..dc1bfb1 --- a/server/unpack.sh +++ b/server/unpack.sh @@ -1,13 +1,30 @@ #/bin/bash ARTIFACT_ID=$1 +OWNER=$2 +REPO=$3 + +# mkdir -p games +cd games +pwd +# mkdir -p tmp +mkdir -p ${OWNER} echo "Unpacking ZIP." -unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID} -echo "Unpacking TAR." -for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file +unzip -o tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip -d tmp/${OWNER}_${REPO}_${ARTIFACT_ID} +echo "Unpacking game." + +# exit the npm project to avoid reloading. TODO: Where should we actually save these? + + + +echo "Delete old version of the game" +rm -rf ${OWNER}/${REPO} +mkdir -p ${OWNER}/${REPO} + +for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file do echo "Unpacking $f" - mkdir tmp/artifact_${ARTIFACT_ID}_inner - tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner + #tar -xvzf $f -C games/${OWNER}/${REPO} + unzip -q -o $f -d ${OWNER}/${REPO} done diff --git a/vite.config.ts b/vite.config.ts index c0b536f..6ec0c2d 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -28,6 +28,9 @@ export default defineConfig({ }) ], publicDir: "client/public", + optimizeDeps: { + exclude: ['games'] + }, server: { port: 3000, proxy: { @@ -38,6 +41,9 @@ export default defineConfig({ '/import': { target: 'http://localhost:8080', }, + '/api': { + target: 'http://localhost:8080', + }, } }, resolve: {