diff --git a/client/src/assets/covers/formaloversum.png b/client/src/assets/covers/formaloversum.png
deleted file mode 100644
index df9723d..0000000
Binary files a/client/src/assets/covers/formaloversum.png and /dev/null differ
diff --git a/client/src/assets/covers/nng.png b/client/src/assets/covers/nng.png
deleted file mode 100644
index 69b0df5..0000000
Binary files a/client/src/assets/covers/nng.png and /dev/null differ
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
index e6f4214..c36730a 100644
--- a/client/src/components/landing_page.tsx
+++ b/client/src/components/landing_page.tsx
@@ -7,13 +7,12 @@ import '@fontsource/roboto/500.css';
import '@fontsource/roboto/700.css';
import '../css/landing_page.css'
-import coverRobo from '../assets/covers/formaloversum.png'
-import coverNNG from '../assets/covers/nng.png'
import bgImage from '../assets/bg.jpg'
import Markdown from './markdown';
import {PrivacyPolicyPopup} from './popup/privacy_policy'
import { GameTile, useGetGameInfoQuery } from '../state/api'
+import path from 'path';
const flag = {
'Dutch': '🇳🇱',
@@ -50,7 +49,7 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
{data.title}
{data.short}
- { data.image ?
: }
+ { data.image ?
: }
{data.long}
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 922fddb..e936a21 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -34,6 +34,7 @@ import { DualEditor } from './infoview/main'
import { GameHint } from './infoview/rpc_api'
import { DeletedHints, Hint, Hints } from './hints'
import { PrivacyPolicyPopup } from './popup/privacy_policy'
+import path from 'path';
import '@fontsource/roboto/300.css'
import '@fontsource/roboto/400.css'
@@ -465,6 +466,11 @@ function Introduction({impressum, setImpressum}) {
const gameInfo = useGetGameInfoQuery({game: gameId})
+ const {worldId} = useContext(WorldLevelIdContext)
+
+ let image: string = gameInfo.data?.worlds.nodes[worldId].image
+
+
const toggleImpressum = () => {
setImpressum(!impressum)
}
@@ -478,7 +484,12 @@ function Introduction({impressum, setImpressum}) {
:
-
+
+ {image &&
+

+ }
+
+
}
diff --git a/client/src/css/level.css b/client/src/css/level.css
index faa2c0d..01d36b6 100644
--- a/client/src/css/level.css
+++ b/client/src/css/level.css
@@ -336,6 +336,16 @@ td code {
background-color: #eee;
}
+.world-image-container {
+ display: flex;
+ flex-direction: column;
+ justify-content: center;
+}
+
+.world-image-container img {
+ object-fit: contain;
+}
+
.typewriter-interface .proof {
background-color: #fff;
}
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 299cf8d..2bdbe8b 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -19,11 +19,12 @@ export interface GameInfo {
title: null|string,
introduction: null|string,
info: null|string,
- worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]},
+ worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string, image: string}}, edges: string[][]},
worldSize: null|{[key: string]: number},
authors: null|string[],
conclusion: null|string,
- tile: null|GameTile
+ tile: null|GameTile,
+ image: null|string
}
export interface InventoryTile {
@@ -49,7 +50,8 @@ export interface LevelInfo {
lemmaTab: null|string,
statementName: null|string,
displayName: null|string,
- template: null|string
+ template: null|string,
+ image: null|string
}
/** Used to display the inventory on the welcome page */
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 0789c59..9cd98f1 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -60,10 +60,32 @@ elab "Introduction" t:str : command => do
/-- Define the info of the current game. Used for e.g. credits -/
elab "Info" t:str : command => do
match ← getCurLayer with
- | .Level => pure ()
- | .World => pure ()
+ | .Level =>
+ logError "Can't use `Info` in a level!"
+ pure ()
+ | .World =>
+ logError "Can't use `Info` in a world"
+ pure ()
| .Game => modifyCurGame fun game => pure {game with info := t.getString}
+/-- Provide the location of the image for the current game/world/level.
+Paths are relative to the lean project's root. -/
+elab "Image" t:str : command => do
+ let file := t.getString
+ if not <| ← System.FilePath.pathExists file then
+ logWarningAt t s!"Make sure the cover image '{file}' exists."
+ if not <| file.startsWith "images/" then
+ logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
+
+ match ← getCurLayer with
+ | .Level =>
+ logWarning "Level-images not implemented yet" -- TODO
+ modifyCurLevel fun level => pure {level with image := file}
+ | .World =>
+ modifyCurWorld fun world => pure {world with image := file}
+ | .Game =>
+ logWarning "Main image of the game not implemented yet" -- TODO
+ modifyCurGame fun game => pure {game with image := file}
/-- Define the conclusion of the current game or current level if some
building a level. -/
@@ -96,10 +118,15 @@ elab "Languages" t:str* : command => do
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}}
+elab "CoverImage" t:str : command => do
+ let file := t.getString
+ if not <| ← System.FilePath.pathExists file then
+ logWarningAt t s!"Make sure the cover image '{file}' exists."
+ if not <| file.startsWith "images/" then
+ logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
+ modifyCurGame fun game => pure {game with
+ tile := {game.tile with image := file}}
/-! # Inventory
@@ -655,6 +682,26 @@ elab "Template" tacs:tacticSeq : tactic => do
modifyLevel (←getCurLevelId) fun level => do
return {level with template := s!"{template}"}
+
+
+open IO.FS System FilePath in
+/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
+def copyImages : IO Unit := do
+ let target : FilePath := ".lake" / "gamedata"
+ for file in ← walkDir "images" do
+ let outFile := target.join file
+ -- create the directories
+ if ← file.isDir then
+ createDirAll outFile
+ else
+ if let some parent := outFile.parent then
+ createDirAll parent
+ -- copy file
+ let content ← readBinFile file
+ writeBinFile outFile content
+
+
+
-- TODO: Notes for testing if a declaration has the simp attribute
-- -- Test: From zulip
@@ -676,7 +723,7 @@ elab "Template" tacs:tacticSeq : tactic => do
#eval IO.FS.createDirAll ".lake/gamedata/"
-- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit:= do
+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"
@@ -685,6 +732,9 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : Comma
IO.FS.removeDirAll path
IO.FS.createDirAll path
+ -- copy the images folder
+ copyImages
+
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)))
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index f94478f..a1e15f3 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -265,7 +265,9 @@ structure GameLevel where
lemmas: InventoryInfo := default
/-- A proof template that is printed in an empty editor. -/
template: Option String := none
- deriving Inhabited, Repr
+ /-- The image for this level. -/
+ image : String := default
+deriving Inhabited, Repr
/-- Json-encodable version of `GameLevel`
Fields:
@@ -286,6 +288,7 @@ structure LevelInfo where
displayName : Option String
statementName : Option String
template : Option String
+ image: Option String
deriving ToJson, FromJson
def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
@@ -315,6 +318,7 @@ def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
-- Note: we could call `.find!` because we check in `Statement` that the
-- lemma doc must exist.
template := lvl.template
+ image := lvl.image
}
/-! ## World -/
@@ -331,13 +335,16 @@ structure World where
conclusion : String := default
/-- The levels of the world. -/
levels: HashMap Nat GameLevel := default
+ /-- The introduction image of the world. -/
+ image: String := default
deriving Inhabited
instance : ToJson World := ⟨
fun world => Json.mkObj [
("name", toJson world.name),
("title", world.title),
- ("introduction", world.introduction)]
+ ("introduction", world.introduction),
+ ("image", world.image)]
⟩
/-! ## Game -/
@@ -382,7 +389,10 @@ structure Game where
/-- TODO: currently unused. -/
authors : List String := default
worlds : Graph Name World := default
+ /-- The tile displayed on the server's landing page. -/
tile : GameTile := default
+ /-- The path to the background image of the world. -/
+ image : String := default
deriving Inhabited, ToJson
def getGameJson (game : «Game») : Json := Id.run do