Merge branch 'dev' into world_overviews

Add the function of caching typewriterMode

.gitignore

@@ -1,5 +1,4 @@
 node_modules
-games/
 client/dist
 games/
 server/.lake

README.md

@@ -10,20 +10,25 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 * 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
-
-We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
-
-For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
-
 ## Documentation
 
-The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game.
+The documentation is very much work in progress but the linked documentation here
+should be up-to-date:
 
-Some documentation:
+### Game creation API
 
-- [NPM Scripts](doc/npm_scripts.md)
-- [Old documentation](doc/DOCUMENTATION.md)
+- [Creating a Game](doc/create_game.md): **the main document to consult**.
+- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
+
+### Frontend API
+
+* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
+* [How to Update an existing Game](doc/update_game.md): update to a new lean version
+* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
+
+### Backend
+
+not written yet
 
 ## Contributing
 
@@ -37,5 +42,5 @@ Providing the use access to a Lean instance running on the server is a severe se
 
 The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-of Kevin Buzzard and Mohammad Pedramfar.
+by Kevin Buzzard and Mohammad Pedramfar.
 The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

client/src/components/hints.tsx

@@ -1,6 +1,7 @@
 import { GameHint } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
+import { ProofStep } from "./infoview/context";
 
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
@@ -43,3 +44,24 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
     {hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
   </>
 }
+
+/** Filter hints to not show consequtive identical hints twice.
+ *
+ * This function takes a `ProofStep[]` and extracts the hints in form of an
+ * element of type `GameHint[][]` where it removes hints that are identical to hints
+ * appearing in the previous step. Hidden hints are not filtered.
+ *
+ * This effectively means we prevent consequtive identical hints from being shown.
+ */
+export function filterHints(proof: ProofStep[]): GameHint[][] {
+  return proof.map((step, i) => {
+    if (i == 0){
+      return step.hints
+    } else {
+      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
+      // good way to shallow-compare objects?
+      return step.hints.filter((hint) => hint.hidden ||
+        (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
+    }
+  })
+}

client/src/components/infoview/main.tsx

@@ -34,7 +34,7 @@ import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
 import { GameHint } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints } from '../hints';
+import { Hints, filterHints } from '../hints';
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
@@ -156,7 +156,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
 
   const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
 
-  console.debug(`template: ${props.data.template}`)
+  console.debug(`template: ${props.data?.template}`)
 
   // React.useEffect (() => {
   //   if (props.data.template) {
@@ -367,9 +367,9 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      proof.slice(line).map((step, i) => {
+      filterHints(proof).slice(line).map((hintsAtStep, i) => {
         // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
       })
       setDeletedChat(deletedChat)
 

client/src/components/inventory.tsx

@@ -5,7 +5,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
-import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
+import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery, WorldOverview } from '../state/api';
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
@@ -37,6 +37,79 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
   )
 }
 
+export function OverviewInventory({data, openDoc, enableAll=false, showOverview=true} :
+  {
+    data: WorldOverview[],
+    openDoc: (props: {name: string, type: string}) => void,
+    enableAll?: boolean,
+    showOverview?: boolean
+  }) {
+
+  const gameId = React.useContext(GameIdContext)
+  const difficulty = useSelector(selectDifficulty(gameId))
+  const [tab, setTab] = useState<string>()
+  let inv: string[] = selectInventory(gameId)(store.getState())
+
+  let levelInfo : InventoryOverview = {
+    tactics : data ? data.map(world => (world.tactics.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
+    lemmas : data ? data.map(world => (world.lemmas.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
+    definitions : data ? data.map(world => (world.definitions.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
+    lemmaTab: null,
+  }
+
+  return (
+    <>
+      <Inventory levelInfo={levelInfo} openDoc={openDoc} enableAll={enableAll}/>
+      {showOverview &&
+        <div className="inventory">
+          {data && <>
+            <h2>Overviews</h2>
+            <div className="tab-bar">
+              {data.map(world => {
+                return <div key={`category-${world.world}`} className={`tab ${world.world == tab ? "active": ""}`} onClick={() => { setTab((tab == world.world) ? null : world.world) }}>{world.world}</div>
+              })}
+            </div>
+            <div className="inventory-list">
+              {/* TODO: a bit hacky, do we need to redesign inventory completely and provide it in a better order? */}
+              {data.map(world => {
+                if (world.world == tab) {
+                  return [
+                    ...world.tactics.map(item => {
+                      return <InventoryItem
+                        key={`${world.world}-${item.name}`}
+                        showDoc={() => {openDoc({name: item.name, type: 'Tactic'})}}
+                        name={item.name} displayName={item.displayName}
+                        locked={difficulty > 0 ? !inv.includes(item.name) : false}
+                        disabled={item.disabled} newly={false} enableAll={enableAll} />
+                    }),
+                    ...world.lemmas.map(item => {
+                      return <InventoryItem
+                        key={`${world.world}-${item.name}`}
+                        showDoc={() => {openDoc({name: item.name, type: 'Lemma'})}}
+                        name={item.name} displayName={item.displayName}
+                        locked={difficulty > 0 ? item.locked : false}
+                        disabled={item.disabled} newly={false} enableAll={enableAll} />
+                    }),
+                    ...world.definitions.map(item => {
+                      return <InventoryItem
+                        key={`${world.world}-${item.name}`}
+                        showDoc={() => {openDoc({name: item.name, type: 'Definition'})}}
+                        name={item.name} displayName={item.displayName}
+                        locked={difficulty > 0 ? item.locked : false}
+                        disabled={item.disabled} newly={false} enableAll={enableAll} />
+                    })
+                  ]
+                }
+              })}
+            </div>
+          </>}
+        </div>
+      }
+    </>
+
+  )
+}
+
 function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
   {
     items: InventoryTile[],
@@ -144,3 +217,21 @@ export function InventoryPanel({levelInfo, visible = true}) {
     }
   </div>
 }
+
+/** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */
+export function InventoryOverviewPanel({data, visible = true, showOverview=true} : {data : WorldOverview[], visible?: boolean, showOverview?: boolean}) {
+  const gameId = React.useContext(GameIdContext)
+
+  // The inventory is overlayed by the doc entry of a clicked item
+  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
+  // Set `inventoryDoc` to `null` to close the doc
+  function closeInventoryDoc() {setInventoryDoc(null)}
+
+  return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
+    {inventoryDoc ?
+      <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
+      :
+      <OverviewInventory data={data} openDoc={setInventoryDoc} enableAll={true} showOverview={showOverview}/>
+    }
+  </div>
+}

client/src/components/landing_page.tsx

@@ -20,6 +20,7 @@ const flag = {
   'French': '🇫🇷',
   'German': '🇩🇪',
   'Italian': '🇮🇹',
+  'Spanish': '🇪🇸',
 }
 
 function GithubIcon({url='https://github.com'}) {
@@ -131,8 +132,10 @@ function LandingPage() {
   //
   let allGames = [
     "leanprover-community/nng4",
+    "hhu-adam/robo",
     "djvelleman/stg4",
-    "hhu-adam/robo"]
+    "miguelmarco/STG4",
+  ]
   let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 
   return <div className="landing-page">
@@ -162,38 +165,14 @@ function LandingPage() {
           />
         ))
       }
-      {/* <GameTile
-        title="Natural Number Game"
-        gameId="g/hhu-adam/NNG4"
-        intro="The classical introduction game for Lean."
-        description="In this game you recreate the natural numbers $\mathbb{N}$ from the Peano axioms,
-learning the basics about theorem proving in Lean.
-
-This is a good first introduction to Lean!"
-        worlds="8"
-        levels="67"
-        image={coverNNG}
-        language="English"
-        />
-
-      <GameTile
-        title="Set Theory Game"
-        gameId="g/djvelleman/STG4"
-        intro="A game about set theory"
-        description=""
-        worlds="5"
-        levels="30"
-        language="English"
-        />
-   */}
     </div>
     <section>
       <div className="wrapper">
         <h2>Development notes</h2>
         <p>
           As this server runs lean on our university machines, it has a limited capacity.
-          Our current estimate is about 55 copies of the NNG or 25 copies of games importing
-          mathlib. We hope to address this limitation in the future.
+          Our current estimate is about 70 simultaneous games.
+          We hope to address and test this limitation better in the future.
         </p>
         <p>
           Most aspects of the games and the infrastructure are still in development. Feel free to
@@ -207,18 +186,19 @@ This is a good first introduction to Lean!"
         <h2>Adding new games</h2>
         <p>
           If you are considering writing your own game, you should use
-          the <a target="_blank" href="https://github.com/hhu-adam/NNG4">NNG Github Repo</a> as
-          a template.
+          the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
+          a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
         </p>
         <p>
-          There is an option to load and run your own games directly on the server,
-          instructions are in the NNG repo. Since this is still in development we'd like to
-          encourage you to contact us for support creating your own game. The documentation is
-          not polished yet.
+          You can directly load your games into the server and play it using
+          the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> also
+          explain the details for how to load your game to the server.
+
+          We'd like to encourage you to contact us if you have any questions.
         </p>
         <p>
-          To add games to this main page, you should get in contact as
-          games will need to be added manually.
+          Featured games on this page are added manually.
+          Please get in contact and we-ll happily add yours.
         </p>
       </div>
     </section>
@@ -236,9 +216,6 @@ This is a good first introduction to Lean!"
       <a className="link" onClick={openImpressum}>Impressum</a>
       {impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
     </footer>
-
-    {/* <PrivacyPolicy/> */}
-
   </div>
 
 }

client/src/components/level.tsx

@@ -22,17 +22,17 @@ import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
-  selectHelp, selectDifficulty, selectInventory } from '../state/progress'
+  selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
 import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
-import {InventoryPanel} from './inventory'
+import {InventoryOverviewPanel, InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
   ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints } from './hints'
+import { DeletedHints, Hint, Hints, filterHints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import path from 'path';
 
@@ -138,19 +138,24 @@ function ChatPanel({lastLevel}) {
 
   let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
 
+  // experimental: Remove all hints that appeared identically in the previous step
+  // This effectively prevent consequtive hints being shown.
+  let modifiedHints : GameHint[][] = filterHints(proof)
+
   return <div className="chat-panel">
     <div ref={chatRef} className="chat">
       {introText?.filter(t => t.trim()).map(((t, i) =>
+        // Show the level's intro text as hints, too
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {proof.map((step, i) => {
+      {modifiedHints.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
         if (!(i == proof.length - 1 && withErr)) {
           // TODO: Should not use index as key.
           return <Hints key={`hints-${i}`}
-            hints={step.hints} showHidden={showHelp.has(i)} step={i}
+            hints={step} showHidden={showHelp.has(i)} step={i}
             selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
         }
       })}
@@ -204,11 +209,16 @@ function PlayableLevel({impressum, setImpressum}) {
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(MobileContext)
 
+  const dispatch = useAppDispatch()
+
   const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
   const inventory: Array<String> = useSelector(selectInventory(gameId))
 
+  const typewriterMode = useSelector(selectTypewriterMode(gameId))
+  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
@@ -221,12 +231,11 @@ function PlayableLevel({impressum, setImpressum}) {
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
-  const [typewriterMode, setTypewriterMode] = useState(true)
+
   // set to true to prevent switching between typewriter and editor
   const [lockInputMode, setLockInputMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
-  const dispatch = useAppDispatch()
 
   // impressum pop-up
   function toggleImpressum() {setImpressum(!impressum)}
@@ -320,8 +329,6 @@ function PlayableLevel({impressum, setImpressum}) {
           console.debug(`not inserting template.`)
         }
       }
-    } else {
-      setTypewriterMode(true)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -336,7 +343,7 @@ function PlayableLevel({impressum, setImpressum}) {
   }, [gameId, worldId, levelId])
 
   useEffect(() => {
-    if (!typewriterMode) {
+    if (!typewriterMode && editor) {
       // Delete last input attempt from command line
       editor.executeEdits("typewriter", [{
         range: editor.getSelection(),
@@ -486,11 +493,12 @@ function Introduction({impressum, setImpressum}) {
           <IntroductionPanel gameInfo={gameInfo} />
           <div className="world-image-container empty">
             {image &&
-              <img src={path.join("data", gameId, image)} alt="" />
+              // TODO: Temporary for testing
+              <img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
             }
 
           </div>
-          <InventoryPanel levelInfo={inventory?.data} />
+          <InventoryOverviewPanel data={inventory?.data} />
         </Split>
       }
 

client/src/components/welcome.tsx

@@ -11,7 +11,7 @@ import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { MobileContext } from './infoview/context'
-import { InventoryPanel } from './inventory'
+import { InventoryOverviewPanel, InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/game_info'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
@@ -111,7 +111,7 @@ function Welcome() {
               <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
                 rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             :
-              <InventoryPanel levelInfo={inventory?.data} />
+              <InventoryOverviewPanel data={inventory?.data} />
             )}
           </div>
         :
@@ -119,7 +119,7 @@ function Welcome() {
             <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
             <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
               rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
-            <InventoryPanel levelInfo={inventory?.data} />
+            <InventoryOverviewPanel data={inventory?.data} />
           </Split>
       }
     </div>

client/src/css/level.css

@@ -342,10 +342,15 @@ td code  {
   justify-content: center;
 }
 
-.world-image-container img {
+.world-image-container img.contain {
   object-fit: contain;
 }
 
+.world-image-container img.cover {
+  height: 100%;
+  object-fit: cover;
+}
+
 .typewriter-interface .proof {
   background-color: #fff;
 }

client/src/state/api.ts

@@ -71,6 +71,13 @@ interface Doc {
   category: string,
 }
 
+export interface WorldOverview {
+  world: string
+  tactics: InventoryTile[]
+  lemmas: InventoryTile[]
+  definitions: InventoryTile[]
+}
+
 // Define a service using a base URL and expected endpoints
 export const apiSlice = createApi({
   reducerPath: 'gameApi',
@@ -82,7 +89,7 @@ export const apiSlice = createApi({
     loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
       query: ({game, world, level}) => `${game}/level__${world}__${level}.json`,
     }),
-    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
+    loadInventoryOverview: builder.query<WorldOverview[], {game: string}>({
       query: ({game}) => `${game}/inventory.json`,
     }),
     loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({

client/src/state/progress.ts

@@ -26,7 +26,8 @@ export interface GameProgressState {
   inventory: string[],
   difficulty: number,
   openedIntro: boolean,
-  data: WorldProgressState
+  data: WorldProgressState,
+  typewriterMode?: boolean
 }
 
 /**
@@ -126,6 +127,11 @@ export const progressSlice = createSlice({
       addGameProgress(state, action)
       state.games[action.payload.game].openedIntro = action.payload.openedIntro
     },
+    /** set the typewriter mode */
+    changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) {
+      addGameProgress(state, action)
+      state.games[action.payload.game].typewriterMode = action.payload.typewriterMode
+    }
   }
 })
 
@@ -196,7 +202,14 @@ export function selectOpenedIntro(game: string) {
   }
 }
 
+/** return typewriter mode for the current game if it exists */
+export function selectTypewriterMode(game: string) {
+  return (state) => {
+    return state.progress.games[game]?.typewriterMode ?? true
+  }
+}
+
 /** Export actions to modify the progress */
 export const { changedSelection, codeEdited, levelCompleted, deleteProgress,
   deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro,
-  changedDifficulty } = progressSlice.actions
+  changedDifficulty, changeTypewriterMode} = progressSlice.actions

doc/DOCUMENTATION.md

@@ -1,6 +1,8 @@
+**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
+
 # Creating a game.
 
-Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
+Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
 
 ## Game Structure
 
@@ -295,8 +297,9 @@ cd lean4game
 npm install
 ```
 
+TODO: This is outdated!
 If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/server/index.mjs`:
+code at the beginning of `lean4game/relay/index.mjs`:
 ```typescript
 const games = {
     "g/hhu-adam/robo": {

doc/create_game.md

@@ -223,25 +223,17 @@ One thing to keep in mind is that the game will look at the main proof to figure
 Most important for game development are probably the `Hints`.
 
 The hints will be displayed whenever the player's current goal matches the goal the hint is
-placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. If you specify
+placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.
 
-```
-Hint (strict := true) "some hidden hint"
-```
+Read [More about Hints](doc/hints.md) for how they work and what the options are.
 
-a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context)
+### 6. e) Extra: Images
+You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
 
-Further, you can choose to hide hints and only have them displayed when the player presses "More Help":
-```
-Hint (hidden := true) "some hidden hint"
-```
+The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"` 
+in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
 
-Lastly, you should put variable names in hints inside brackets:
-
-```
-Hint "now use `rw [{h}]` to use your assumption {h}."
-```
-That way, the game will replace it with the actual name the assumption has in the player's proof state.
+NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
 
 ## 7. Update your game
 
@@ -251,6 +243,21 @@ In principle, it is as simple as modifying `lean-toolchain` to update your game
 
 To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
 
+There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
+
+```lean
+Languages "English"
+CaptionShort "Game Template"
+CaptionLong "You should use this game as a template for your own game and add your own levels."
+Prerequisites "NNG"
+CoverImage "images/cover.png"
+```
+* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
+* `CaptionShort`: One catch phrase. Appears above the image.
+* `CaptionLong`: 2-4 sentences to describe the game.
+* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
+* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
+
 ## Further Notes
 
 Here are some random further things you should consider designing a new game:

doc/hints.md

@@ -0,0 +1,87 @@
+# Hints
+
+Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic
+
+```
+Statement .... := by
+  Hint "Hint to show at the start"
+  rw [h]
+  Hint "some tip after using rw"
+  ...
+```
+
+## 1. When do hints show?
+
+A hint will be displayed if the player's goal matches the one where the hint was placed in the
+sample solutions and the entire context from the sample solutions is present in the
+player's context. The player's context may contain additional items.
+
+This means if you have multiple identical
+subgoals, you should only place a single hint in one of them and it will be displayed in
+all of them.
+
+However, identical (non-hidden) hints which where already present in the step
+before are omitted. This is to allow a player to add new assumptions to context, for example
+with `have`, without seeing the same hint over and over again.
+Hidden hints are not filtered.
+
+## 2. Alternative Proofs / `Branch`
+
+You can use `Branch` to place hints
+in dead ends or alternative proof strands.
+
+A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end
+so that no progress has been made on proofing the goal.
+
+```
+Statement .... := by
+  Hint "Huse `rw` or `rewrite`."
+  Branch
+    rewrite [h]
+    Hint "now you still need `rfl`"
+  rw [h]
+```
+
+## 3. Variables names
+
+Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
+the variable's name with the one the user actually used.
+
+For example, if the sample proof contains
+
+```
+have h : True := trivial
+Hint "Now use `rw [{h}]` to use your assumption `{h}`."
+```
+
+but the player writes `have g : True := trivial`, they will see a hint saying
+"Now use `rw [g]` to use your assumption `g`."
+
+## 4. Hidden hints
+
+Some hints can be hidden, and only show after the user clicks on a button to get additional
+help. You mark a hint as hidden with `(hidden := true)`:
+
+```
+Hint (hidden := true) "some hidden hint"
+```
+
+## 5. Strict context matching
+
+If you use the attribute `(strict := true)` a hint is only shown if the entire context
+matches exactly the one where the hint is placed. With `(hint := false)`, which is the default,
+it does not matter if additional assumptions are present in the player's context.
+
+```
+Hint (strict := true) "now use `have` to create a new assumption."
+```
+
+You should probably use `(strict := true)` if you want to give fine-grained details about
+tactics like `have` which do not modify the goal or any existing assumptions, but only
+create new assumptions.
+
+## 6. Formatting
+
+You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
+
+TODO: Write a doc about latex/markdown options available.

doc/publish_game.md

@@ -28,3 +28,5 @@ Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITOR
 
 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!
+
+For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).

doc/running_locally.md

@@ -86,11 +86,10 @@ Download dependencies and build the game:
 ```bash
 cd GameSkeleton
 lake update -R
-lake exe cache get   # if your game depends on mathlib
 lake build
 ```
 
-Clone the game repository into a directory next to the game:
+Clone the server repository into a directory next to the game:
 ```bash
 cd ..
 git clone https://github.com/leanprover-community/lean4game.git

doc/update_game.md

@@ -10,15 +10,14 @@ 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
+* Local Setup: in your game's folder run the following:
   ```
   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:
+    you should update this one to the matching version. Run the following in the folder `lean4game/`:
     ```
     git fetch
     git checkout {VERSION_TAG}
@@ -27,7 +26,7 @@ Then, depending on the setup you use, do one of the following:
     where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
 * Gitpod/Codespaces: Create a fresh one
 
-This will your game (and the mathlib version you might be using) to the new lean version.
+This will update your game (and the mathlib version you might be using) to the new lean version.
 
 ## Newest developing setup
 

ecosystem.config.cjs

@@ -2,7 +2,7 @@
 module.exports = {
   apps : [{
     name   : "lean4game",
-    script : "server/index.mjs",
+    script : "relay/index.mjs",
     env: {
       LEAN4GAME_GITHUB_USER: "",
       LEAN4GAME_GITHUB_TOKEN: "",

package-lock.json

@@ -16122,9 +16122,9 @@
       }
     },
     "node_modules/vite": {
-      "version": "4.5.0",
-      "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.0.tgz",
-      "integrity": "sha512-ulr8rNLA6rkyFAlVWw2q5YJ91v098AFQ2R0PRFwPzREXOUJQPtFUG0t+/ZikhaOCDqFoDhN6/v8Sq0o4araFAw==",
+      "version": "4.5.1",
+      "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.1.tgz",
+      "integrity": "sha512-AXXFaAJ8yebyqzoNB9fu2pHoo/nWX+xZlaRwoeYUxEqBO+Zj4msE5G+BhGBll9lYEKv9Hfks52PAF2X7qDYXQA==",
       "dependencies": {
         "esbuild": "^0.18.10",
         "postcss": "^8.4.27",

package.json

@@ -63,13 +63,13 @@
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "cd server && lake build && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
+    "start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")",
     "start_client": "cross-env NODE_ENV=development vite --host",
     "build": "npm run build_server && npm run build_client",
     "preview": "vite preview",
     "build_server": "cd server && lake build",
     "build_client": "cross-env NODE_ENV=production vite build",
-    "production": "cross-env NODE_ENV=production node server/index.mjs"
+    "production": "cross-env NODE_ENV=production node relay/index.mjs"
   },
   "eslintConfig": {
     "extends": [

relay/bubblewrap.sh

@@ -2,7 +2,9 @@
 
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
-
+# $1 : the game directory
+# $2 : the lean4game folder
+# $3 : the gameserver executable
 
 (exec bwrap\
   --bind $2 /lean4game \
@@ -24,6 +26,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
   --unshare-uts  \
   --unshare-cgroup \
   --die-with-parent \
-  --chdir "/lean4game/server/.lake/build/bin/" \
+  --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
   ./gameserver --server /game
 )

relay/import.mjs

@@ -79,17 +79,17 @@ async function doImport (owner, repo, id) {
     artifactId = artifact.id
     const url = artifact.archive_download_url
     // Make sure the download folder exists
-    if (!fs.existsSync(`${__dirname}/../games`)){
-      fs.mkdirSync(`${__dirname}/../games`);
+    if (!fs.existsSync(path.join(__dirname, "..", "games"))){
+      fs.mkdirSync(path.join(__dirname, "..", "games"));
     }
-    if (!fs.existsSync(`${__dirname}/../games/tmp`)){
-      fs.mkdirSync(`${__dirname}/../games/tmp`);
+    if (!fs.existsSync(path.join(__dirname, "..", "games", "tmp"))){
+      fs.mkdirSync(path.join(__dirname, "..", "games", "tmp"));
     }
     progress[id].output += `Download from ${url}\n`
-    await download(id, url, `${__dirname}/../games/tmp/${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`)
+    await download(id, url, path.join(__dirname, "..", "games", "tmp", `${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`))
     progress[id].output += `Download finished.\n`
 
-    await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId, owner.toLowerCase(), repo.toLowerCase()], `${__dirname}/..`)
+    await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, ".."))
 
 
     // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
@@ -110,8 +110,8 @@ async function doImport (owner, repo, id) {
   } finally {
     // clean-up temp. files
     if (artifactId) {
-      fs.rmSync(`${__dirname}/../games/tmp/${owner}_${repo}_${artifactId}.zip`, {force: true, recursive: false});
-      fs.rmSync(`${__dirname}/../games/tmp/${owner}_${repo}_${artifactId}`, {force: true, recursive: true});
+      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}.zip`), {force: true, recursive: false});
+      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}`), {force: true, recursive: true});
     }
     progress[id].done = true
   }

relay/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/'))) // TODO: add a dist folder from inside the game
+  .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,13 +95,22 @@ function startServerProcess(owner, repo) {
   let serverProcess
   if (isDevelopment) {
     let args = ["--server", game_dir]
-    serverProcess = cp.spawn("./gameserver", args,  // TODO: find gameserver inside the games
-        { cwd: path.join(__dirname, "./.lake/build/bin/") })
+    let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin")
+    // Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again
+    if (fs.existsSync(binDir)) {
+      // Try to use the game's own copy of `gameserver`.
+      serverProcess = cp.spawn("./gameserver", args, { cwd: binDir })
+    } else {
+      // If the game is built with `-Klean4game.local` there is no copy in the lake packages.
+      serverProcess = cp.spawn("./gameserver", args,
+        { cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") })
+    }
   } else {
     serverProcess =  cp.spawn("./bubblewrap.sh",
-      [game_dir, path.join(__dirname, '..')],
+      [ game_dir, path.join(__dirname, '..')],
       { cwd: __dirname })
   }
+
   serverProcess.on('error', error =>
     console.error(`Launching Lean Server failed: ${error}`)
   )

relay/unpack.sh

@@ -6,7 +6,7 @@ REPO=$3
 
 # mkdir -p games
 cd games
-pwd
+
 # mkdir -p tmp
 mkdir -p ${OWNER}
 

server/.gitignore

@@ -1,3 +0,0 @@
-build/
-games/
-.lake

server/GameServer/EnvExtensions.lean

@@ -269,6 +269,13 @@ structure GameLevel where
   image : String := default
 deriving Inhabited, Repr
 
+structure WorldOverview where
+  world: Name
+  tactics: Array InventoryTile := default
+  definitions: Array InventoryTile := default
+  lemmas: Array InventoryTile := default
+  deriving FromJson, ToJson, Inhabited, Repr
+
 /-- Json-encodable version of `GameLevel`
 Fields:
 - description: Lemma in mathematical language.

server/GameServer/Game.lean

@@ -93,6 +93,54 @@ 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
+
+      let mut overview : Array WorldOverview := #[]
+      for ⟨worldId, world⟩ in game.worlds.nodes.toList do
+        let mut tactics : Array InventoryTile := #[]
+        let mut theorems : Array InventoryTile := #[]
+        let mut definitions : Array InventoryTile := #[]
+        for ⟨_levelId, lvl⟩ in world.levels.toList do
+          tactics := tactics ++ lvl.tactics.tiles.filterMap (fun tile => match tile.new with
+            | true => some {tile with new := false, locked := true, disabled := false}
+            | false => none)
+          theorems := theorems ++ lvl.lemmas.tiles.filterMap (fun tile => match tile.new with
+            | true => some {tile with new := false, locked := true, disabled := false}
+            | false => none)
+          definitions := definitions ++ lvl.definitions.tiles.filterMap (fun tile => match tile.new with
+            | true => some {tile with new := false, locked := true, disabled := false}
+            | false => none)
+        overview := overview.push {
+          world := worldId,
+          tactics := tactics,
+          lemmas := theorems,
+          definitions := definitions }
+      let c ← read
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson overview⟩
+      return true
+      -- -- 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
 

server/lakefile.lean

@@ -15,3 +15,13 @@ lean_exe gameserver {
   root := `Main
   supportInterpreter := true
 }
+
+/--
+When a package depending on GameServer updates its dependencies,
+build the `gameserver` executable.
+-/
+post_update pkg do
+  let rootPkg ← getRootPackage
+  if rootPkg.name = pkg.name then
+    return -- do not run in GameServer itself
+  discard <| runBuild gameserver.build >>= (·.await)

tsconfig.json

@@ -12,5 +12,5 @@
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
   },
-  "exclude": ["server"]
+  "exclude": ["server", "relay"]
 }

vite.config.ts

@@ -8,7 +8,7 @@ export default defineConfig({
   //root: 'client/src',
   build: {
     // Relative to the root
-    // Note: This has to match the path in `server/index.mjs`
+    // Note: This has to match the path in `relay/index.mjs`
     outDir: 'client/dist',
   },
   plugins: [