diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 9b50ce7..e6f4214 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -13,6 +13,7 @@ import bgImage from '../assets/bg.jpg' import Markdown from './markdown'; import {PrivacyPolicyPopup} from './popup/privacy_policy' +import { GameTile, useGetGameInfoQuery } from '../state/api' const flag = { 'Dutch': '🇳🇱', @@ -33,47 +34,42 @@ function GithubIcon({url='https://github.com'}) { } -function GameTile({ - title, - gameId, - intro, // Catchy intro phrase. - image=null, - worlds='?', - levels='?', - prereq='–', // Optional list of games that this game builds on. Use markdown. - description, // Longer description. Supports Markdown. - language}) { +function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); } + if (typeof data === 'undefined') { + return <> + } + return
-
{title}
-
{intro} +
{data.title}
+
{data.short}
- { image ? :
} -
{description}
+ { data.image ? :
} +
{data.long}
- + - + - + - +
Prerequisites{prereq}{data.prerequisites.join(', ')}
Worlds{worlds}{data.worlds}
Levels{levels}{data.levels}
Language{flag[language]}{data.languages.map((lan) => flag[lan]).join(', ')}
@@ -89,6 +85,56 @@ function LandingPage() { const openImpressum = () => setImpressum(true); const closeImpressum = () => setImpressum(false); + // const [allGames, setAllGames] = React.useState([]) + // const [allTiles, setAllTiles] = React.useState([]) + + // const getTiles=()=>{ + // fetch('featured_games.json', { + // headers : { + // 'Content-Type': 'application/json', + // 'Accept': 'application/json' + // } + // } + // ).then(function(response){ + // return response.json() + // }).then(function(data) { + // setAllGames(data.featured_games) + + // }) + // } + + // React.useEffect(()=>{ + // getTiles() + // },[]) + + // React.useEffect(()=>{ + + // Promise.allSettled( + // allGames.map((gameId) => ( + // fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined}))) + // ).then(responses => + // responses.forEach((result) => console.log(result))) + // // Promise.all(responses.map(res => { + // // if (res.status == "fulfilled") { + // // console.log(res.value.json()) + // // return res.value.json() + // // } else { + // // return undefined + // // } + // // })) + // // ).then(allData => { + // // setAllTiles(allData.map(data => data?.tile)) + // // }) + // },[allGames]) + + // TODO: I would like to read the supported games list form a JSON, + // Then load all these games in + // + let allGames = [ + "leanprover-community/nng4", + "djvelleman/stg4", + "hhu-adam/robo"] + let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) return
@@ -105,8 +151,19 @@ function LandingPage() {
- - No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a + game directly from a local folder. +

+ : allGames.map((id, i) => ( + + )) + } + {/* - - + */}
diff --git a/client/src/state/api.ts b/client/src/state/api.ts index a41f9f4..299cf8d 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -3,6 +3,18 @@ */ import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react' + +export interface GameTile { + title: string + short: string + long: string + languages: Array + prerequisites: Array + worlds: number + levels: number + image: string +} + export interface GameInfo { title: null|string, introduction: null|string, @@ -11,6 +23,7 @@ export interface GameInfo { worldSize: null|{[key: string]: number}, authors: null|string[], conclusion: null|string, + tile: null|GameTile } export interface InventoryTile { diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index d6b9ea5..e9e193f 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -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 @@ -71,6 +73,33 @@ 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 "Image" t:str : command => do + modifyCurGame fun game => pure {game with + tile := {game.tile with image := t.getString}} + /-! # Inventory @@ -848,8 +877,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 @@ -888,9 +921,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 @@ -902,7 +938,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 @@ -958,6 +994,11 @@ elab "MakeGame" : command => do 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 diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index bcef5cc..f94478f 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -342,6 +342,32 @@ instance : ToJson World := ⟨ /-! ## 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 @@ -356,6 +382,7 @@ structure Game where /-- TODO: currently unused. -/ authors : List String := default worlds : Graph Name World := default + tile : GameTile := default deriving Inhabited, ToJson def getGameJson (game : «Game») : Json := Id.run do diff --git a/server/index.mjs b/server/index.mjs index 83441d4..ac3ef6d 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -35,7 +35,7 @@ router.get('/import/status/:owner/:repo', importStatus) router.get('/import/trigger/:owner/:repo', importTrigger) const server = app - .use(express.static(path.join(__dirname, '../client/dist/'))) + .use(express.static(path.join(__dirname, '../client/dist/'))) // TODO: add a dist folder from inside the game .use('/data/g/:owner/:repo/*', (req, res, next) => { const owner = req.params.owner; const repo = req.params.repo @@ -95,7 +95,7 @@ function startServerProcess(owner, repo) { let serverProcess if (isDevelopment) { let args = ["--server", game_dir] - serverProcess = cp.spawn("./gameserver", args, + serverProcess = cp.spawn("./gameserver", args, // TODO: find gameserver inside the games { cwd: path.join(__dirname, "./.lake/build/bin/") }) } else { serverProcess = cp.spawn("./bubblewrap.sh",