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/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/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/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/index.mjs b/server/index.mjs index aa1e037..0f2ce06 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -34,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) @@ -53,7 +79,7 @@ function getTag(owner, repo) { return `g/${owner.toLowerCase()}/${repo.toLowerCase()}` } -function startServerProcess(owner, repo) { +function getGameDir(owner, repo) { owner = owner.toLowerCase() if (owner == 'local') { if(!isDevelopment) { @@ -77,6 +103,14 @@ function startServerProcess(owner, repo) { 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", game_dir] diff --git a/vite.config.ts b/vite.config.ts index ab40967..6ec0c2d 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -41,6 +41,9 @@ export default defineConfig({ '/import': { target: 'http://localhost:8080', }, + '/api': { + target: 'http://localhost:8080', + }, } }, resolve: {