Merge branch 'dev' into world_overviews

This reverts commit 6bced7575b.

.env

@@ -1 +0,0 @@
-LEAN4GAME_SINGLE_GAME=false

.github/workflows/build.yml

@@ -5,7 +5,17 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      - uses: actions/checkout@v4
       - uses: actions/setup-node@v3
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
       - run: npm install
       - run: npm run build

.gitignore

@@ -1,4 +1,5 @@
 node_modules
 client/dist
-server/build
-**/lake-packages/
+games/
+server/.lake
+**/.DS_Store

NOTES.md

@@ -15,9 +15,6 @@ npm install -g http-server
 
 ```
 git clone https://github.com/hhu-adam/NNG4.git
-cd NNG4
-docker rmi nng4:latest
-docker build --pull --rm -f "Dockerfile" -t nng4:latest "."
 ```
 
 
@@ -146,12 +143,6 @@ Activate config:
 ```
 
 
-## Install `unzip` for Importing Docker Images
-
-```
-sudo apt-get install unzip
-```
-
 ## Install bubblewrap (bwrap)
 ```
 sudo apt-get install bubblewrap

README.md

@@ -2,30 +2,33 @@
 
 This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
-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.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
-
 ## Creating a Game
 
-Please follow the tutorial [Creating a Game](doc/create_game.md).
-In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
+Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
 
-### 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).
+* 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)
 
 ## 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
 
@@ -34,3 +37,10 @@ Contributions to `lean4game` are always welcome!
 ## Security
 
 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
+
+## Credits
+
+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/)
+by Kevin Buzzard and Mohammad Pedramfar.
+The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

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<string>(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 (
     <div className="app">
       <GameIdContext.Provider value={gameId}>

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) {
@@ -347,6 +347,7 @@ export function TypewriterInterface({props}) {
   const uri = model.uri.toString()
 
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
+  const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(MobileContext)
   const { proof } = React.useContext(ProofContext)
@@ -366,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)
 
@@ -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 <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
@@ -521,7 +533,7 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress />
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
         }
       </div>
     </div>

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[],
@@ -86,7 +159,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
       {[...modifiedItems].sort(
           // For lemas, sort entries `available > disabled > locked`
           // otherwise alphabetically
-          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled)
+          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return <InventoryItem key={`${item.category}-${item.name}`}
               showDoc={() => {openDoc({name: item.name, type: docType})}}
@@ -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

@@ -7,11 +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 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': '🇳🇱',
@@ -19,6 +20,7 @@ const flag = {
   'French': '🇫🇷',
   'German': '🇩🇪',
   'Italian': '🇮🇹',
+  'Spanish': '🇪🇸',
 }
 
 function GithubIcon({url='https://github.com'}) {
@@ -32,47 +34,42 @@ function GithubIcon({url='https://github.com'}) {
     </div>
 }
 
-function GameTile({
-  title,
-  gameId,
-  intro, // Catchy intro phrase.
-  image=null,
-  worlds='?',
-  levels='?',
-  prereq='&ndash;', // 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 <div className="game" onClick={routeChange}>
     <div className="wrapper">
-      <div className="title">{title}</div>
-      <div className="short-description">{intro}
+      <div className="title">{data.title}</div>
+      <div className="short-description">{data.short}
       </div>
-      { image ? <img className="image" src={image} alt="" /> : <div className="image"/> }
-      <div className="long description"><Markdown>{description}</Markdown></div>
+      { data.image ? <img className="image" src={path.join("data", gameId, data.image)} alt="" /> : <div className="image"/> }
+      <div className="long description"><Markdown>{data.long}</Markdown></div>
     </div>
     <table className="info">
       <tbody>
       <tr>
         <td title="consider playing these games first.">Prerequisites</td>
-        <td><Markdown>{prereq}</Markdown></td>
+        <td><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
       </tr>
       <tr>
         <td>Worlds</td>
-        <td>{worlds}</td>
+        <td>{data.worlds}</td>
       </tr>
       <tr>
         <td>Levels</td>
-        <td>{levels}</td>
+        <td>{data.levels}</td>
       </tr>
       <tr>
         <td>Language</td>
-        <td title={`in ${language}`}>{flag[language]}</td>
+        <td title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
       </tr>
       </tbody>
     </table>
@@ -88,6 +85,58 @@ 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",
+    "hhu-adam/robo",
+    "djvelleman/stg4",
+    "miguelmarco/STG4",
+  ]
+  let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
@@ -104,49 +153,26 @@ function LandingPage() {
       </div>
     </header>
     <div className="game-list">
-
-      <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="4"
-        levels="30"
-        language="English"
-        />
-
-      <GameTile
-        title="Formaloversum"
-        gameId="g/hhu-adam/Robo"
-        intro="Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
-        description="
-Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.
-
-(Das Spiel befindet sich noch in der Entstehungsphase.)"
-        image={coverRobo}
-        language="German"
-        />
-
-      <GameTile
-        title="NNG (OLD)"
-        gameId="g/hhu-adam/nng4-old"
-        intro="The old version of the NNG copied from lean3."
-        description="This version is not maintained and might break at any point. You should play the new version instead"
-        worlds="9"
-        levels="72"
-        language="English"
-        />
+      {allTiles.length == 0 ?
+        <p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
+          game directly from a local folder.
+        </p>
+        : allGames.map((id, i) => (
+          <Tile
+            key={id}
+            gameId={`g/${id}`}
+            data={allTiles[i]}
+          />
+        ))
+      }
     </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
@@ -160,18 +186,19 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
         <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>
@@ -189,9 +216,6 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
       <a className="link" onClick={openImpressum}>Impressum</a>
       {impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
     </footer>
-
-    {/* <PrivacyPolicy/> */}
-
   </div>
 
 }

client/src/components/level.tsx

@@ -22,18 +22,19 @@ 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';
 
 import '@fontsource/roboto/300.css'
 import '@fontsource/roboto/400.css'
@@ -48,7 +49,6 @@ function Level() {
   const params = useParams()
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
-  // useLoadWorldFiles(worldId)
 
   const [impressum, setImpressum] = React.useState(false)
 
@@ -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(),
@@ -466,6 +473,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)
   }
@@ -479,8 +491,14 @@ function Introduction({impressum, setImpressum}) {
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
           <IntroductionPanel gameInfo={gameInfo} />
-          <div className="world-image-container empty"></div>
-          <InventoryPanel levelInfo={inventory?.data} />
+          <div className="world-image-container empty">
+            {image &&
+              // TODO: Temporary for testing
+              <img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
+            }
+
+          </div>
+          <InventoryOverviewPanel data={inventory?.data} />
         </Split>
       }
 
@@ -615,7 +633,8 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
       return () => {
         editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose(); }
+        model.dispose();
+      }
     }
   }, [editor, levelId, connection, leanClientStarted])
 
@@ -637,27 +656,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])
-}

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/app.css

@@ -42,12 +42,6 @@ body {
   border-radius: .3em;
 }
 
-
-/* Hide monaco editor notifications */
-.monaco-workbench > .notifications-toasts.visible {
-  display: none !important;
-}
-
 .loading {
   margin: auto;
   height: 100%;

client/src/css/landing_page.css

@@ -48,6 +48,7 @@ a {
   border: 1px solid rgb(140, 140, 140);
   border-radius: 20px;
   box-shadow: 5px 5px 8px rgb(140, 140, 140);
+  width: 100%;
   max-width: 500px;
   display: flex;
   flex-direction: column;

client/src/css/level.css

@@ -336,6 +336,21 @@ td code  {
   background-color: #eee;
 }
 
+.world-image-container {
+  display: flex;
+  flex-direction: column;
+  justify-content: center;
+}
+
+.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/index.tsx

@@ -1,32 +1,44 @@
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
+import * as React from 'react'
+import { createRoot } from 'react-dom/client'
+import App from './app'
 import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
-  createHashRouter,
-  RouterProvider,
-  Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
+import { store } from './state/store'
+import { Provider } from 'react-redux'
+import type { RouteObject } from "react-router"
+import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
+import ErrorPage from './components/error_page'
+import Welcome from './components/welcome'
+import LandingPage from './components/landing_page'
+import Level from './components/level'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+
 
 monacoSetup()
 
+
+// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
+// `/g/local/game`. This is used for the devcontainer setup
+let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
+let root_object: RouteObject = single_game ? {
+  path: "/",
+  loader: () => redirect("/g/local/game")
+} : {
+  path: "/",
+  element: <LandingPage />,
+}
+
 const router = createHashRouter([
+  root_object,
   {
-    path: "/",
-    element: <LandingPage />,
-  },
-  {
+    // For backwards compatibility
     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: <App />,

client/src/index_local.tsx

@@ -1,55 +0,0 @@
-// This file is a copy of `index.tsx` where the path "/" is redirected to "/g/local/game".
-// It is used for the dev. setup where there is only one game in a folder called `game`.
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
-import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
-  createHashRouter,
-  RouterProvider,
-  Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
-
-monacoSetup()
-
-const router = createHashRouter([
-  {
-    path: "/",
-    loader: () => redirect("/g/local/game")
-  },
-  {
-    path: "/g/:owner/:repo",
-    element: <App />,
-    errorElement: <ErrorPage />,
-    children: [
-      {
-        path: "/g/:owner/:repo",
-        element: <Welcome />,
-      },
-      {
-        path: "/g/:owner/:repo/world/:worldId/level/:levelId",
-        element: <Level />,
-      },
-    ],
-  },
-]);
-
-const container = document.getElementById('root');
-const root = createRoot(container!);
-root.render(
-  <React.StrictMode>
-    <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
-    </Provider>
-  </React.StrictMode>
-);

client/src/state/api.ts

@@ -2,16 +2,29 @@
  * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
-import { Connection } from '../connection'
+
+
+export interface GameTile {
+  title: string
+  short: string
+  long: string
+  languages: Array<string>
+  prerequisites: Array<string>
+  worlds: number
+  levels: number
+  image: string
+}
 
 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,
+  image: null|string
 }
 
 export interface InventoryTile {
@@ -37,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 */
@@ -57,40 +71,29 @@ 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}
-   }
+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',
-  baseQuery: customBaseQuery,
+  baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/data" }),
   endpoints: (builder) => ({
     getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: ({game}) => {return {game, method: 'info', params: {}}},
+      query: ({game}) => `${game}/game.json`,
     }),
     loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
-      query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
+      query: ({game, world, level}) => `${game}/level__${world}__${level}.json`,
     }),
-    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
-      query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}},
+    loadInventoryOverview: builder.query<WorldOverview[], {game: string}>({
+      query: ({game}) => `${game}/inventory.json`,
     }),
     loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
-      query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
+      query: ({game, type, name}) => `${game}/doc__${type}__${name}.json`,
     }),
   }),
 })

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

@@ -4,7 +4,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
 
 ## 1. Create the project
 
-1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
+1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
 2. Clone the game repo.
 3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
 
@@ -223,25 +223,40 @@ 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:
+NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
 
+## 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](doc/update_game.md).
+
+## 8. Publish 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"
 ```
-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.
+* `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
 

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

@@ -0,0 +1,32 @@
+# 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!
+
+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

@@ -4,13 +4,15 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
 
 There are several options to play a game locally:
 
-- VSCode Dev Container: needs `docker` installed on your machine
-- Codespaces: Needs active internet connection and computing time is limited.
-- Gitpod: does not work yet (I that true?)
-- Manual installation: Needs `npm` installed on your system
+1. VSCode Dev Container: needs `docker` installed on your machine
+2. Codespaces: Needs active internet connection and computing time is limited.
+3. Gitpod: does not work yet (Is that true?)
+4. Manual installation: Needs `npm` installed on your system
 
 The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup.
 
+The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) contains all the relevant files to make your local setup (dev container / gitpod / codespaces) work. You might need to update these files manually by copying them from there if you need any new improvements to the dev setup you're using in an existing game.
+
 ## VSCode Dev Containers
 
 1.  **Install Docker and Dev Containers** *(once)*:<br/>
@@ -27,9 +29,9 @@ The recommended option is "VSCode Dev containers" but you may choose any option
     Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
     A message appears asking you to "Reopen in Container".
 
-    * The first start will take a while, ca. 2-10 minutes. After the first
+    * The first start will take a while, ca. 2-15 minutes. After the first
       start this should be very quickly.
-    * Once built, you can open http://localhost:3000 in your browser. which should load the game
+    * Once built, you can open http://localhost:3000 in your browser. which should load the game.
 
 3.  **Editing Files** *(everytime)*:<br/>
     After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
@@ -42,12 +44,13 @@ The recommended option is "VSCode Dev containers" but you may choose any option
   you might have deleted stuff from docker via your shell. Try deleting the container and image
   explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
   container. (this will again take some time)
+* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
 
 ## Codespaces
 
 You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
 
-Note: You have to wait until npm started properly. In particular, this is after a message like `[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
+Note: You have to wait until npm started properly, which might take a good while.
 
 As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
 
@@ -73,27 +76,26 @@ Now install node:
 nvm install node
 ```
 
-Clone the game (e.g. `NNG4` here):
+Clone the game (e.g. `GameSkeleton` here):
 ```bash
-git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/NNG4.git
+git clone https://github.com/hhu-adam/GameSkeleton.git
+# or: git clone git@github.com:hhu-adam/GameSkeleton.git
 ```
 
 Download dependencies and build the game:
 ```bash
-cd NNG4
-lake update
-lake exe cache get   # if your game depends on mathlib
+cd GameSkeleton
+lake update -R
 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
 # or: git clone git@github.com:leanprover-community/lean4game.git
 ```
-The folders `NNG4` and `lean4game` must be in the same directory!
+The folders `GameSkeleton` and `lean4game` must be in the same directory!
 
 In `lean4game`, install dependencies:
 ```bash
@@ -106,16 +108,16 @@ Run the game:
 npm start
 ```
 
-This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/NNG4. Replace `NNG4` with the folder name of your local game.
+This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.
 
 ## Modifying the GameServer
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export NODE_ENV=development` inside your local game before building it:
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`:
 
 ```bash
 cd NNG4
-export NODE_ENV=development
-lake update
+lake update -R -Klean4game.local
 lake build
 ```
-This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`.
+This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, you can the local copy of the edit `GameServer` in `../lean4game` and
+`lake build` will then directly use this modified copy to build your game.

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.

doc/update_game.md

@@ -0,0 +1,52 @@
+# How to update your Game
+
+## New Lean version
+
+You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the
+new lean version `leanprover/lean4:v4.X.0`.
+
+Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags).
+
+Then, depending on the setup you use, do one of the following:
+
+* Dev Container: Rebuild the VSCode Devcontainer.
+* Local Setup: in your game's folder run the following:
+  ```
+  lake update -R
+  lake build
+  ```
+
+  * Additionally, if you have a local copy of the server `lean4game`,
+    you should update this one to the matching version. Run the following in the folder `lean4game/`:
+    ```
+    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 your game (and the mathlib version you might be using) to the new lean version.
+
+## Newest developing setup
+
+There are a few files in your game repository which are used for the developing setup
+(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
+anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
+
+The relevant files are:
+
+```
+.devcontainer/
+.docker/
+.github/
+.gitpod/
+.vscode/
+lakefile.lean
+```
+
+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, or remove mathlib if you don't need it.)

ecosystem.config.cjs

@@ -2,10 +2,12 @@
 module.exports = {
   apps : [{
     name   : "lean4game",
-    script : "server/index.mjs",
+    script : "relay/index.mjs",
     env: {
-       NODE_ENV: "production",
-       PORT: 8002
+      LEAN4GAME_GITHUB_USER: "",
+      LEAN4GAME_GITHUB_TOKEN: "",
+      NODE_ENV: "production",
+      PORT: 8002
     },
   }]
 }

env.d.ts

@@ -0,0 +1,10 @@
+/// <reference types="vite/client" />
+
+interface ImportMetaEnv {
+  readonly VITE_LEAN4GAME_SINGLE: string
+  // more env variables...
+}
+
+interface ImportMeta {
+  readonly env: ImportMetaEnv
+}

index.html

@@ -33,7 +33,7 @@
       </p>
     </div>
   </noscript>
-  <script src="bundle.js"></script>
+  <script type="module" src="/client/src/index.tsx"></script>
 </body>
 
 </html>

package.json

@@ -1,6 +1,7 @@
 {
   "name": "lean4-game",
   "version": "0.1.0",
+  "type": "module",
   "private": true,
   "homepage": ".",
   "dependencies": {
@@ -15,6 +16,7 @@
     "@reduxjs/toolkit": "^1.9.1",
     "@types/cytoscape": "^3.19.9",
     "@types/react-router-dom": "^5.3.3",
+    "@vitejs/plugin-react-swc": "^3.4.0",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",
@@ -35,45 +37,39 @@
     "rehype-katex": "^6.0.2",
     "remark-gfm": "^3.0.1",
     "remark-math": "^5.1.1",
+    "request": "^2.88.2",
     "request-progress": "^3.0.0",
+    "vite": "^4.5.0",
+    "vite-plugin-static-copy": "^0.17.0",
+    "vite-plugin-svgr": "^4.1.0",
     "vscode-ws-jsonrpc": "^2.0.1",
     "web-worker": "^1.2.0",
     "ws": "^8.11.0"
   },
   "devDependencies": {
-    "@babel/cli": "^7.19.3",
-    "@babel/core": "^7.20.5",
-    "@babel/preset-env": "^7.20.2",
-    "@babel/preset-react": "^7.18.6",
-    "@babel/preset-typescript": "^7.18.6",
     "@pmmmwh/react-refresh-webpack-plugin": "^0.5.10",
     "@redux-devtools/core": "^3.13.1",
     "@testing-library/react": "^13.4.0",
     "@types/debounce": "^1.2.1",
-    "babel-loader": "^8.3.0",
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",
     "file-loader": "^6.2.0",
-    "nodemon": "^2.0.20",
+    "nodemon": "^3.0.1",
     "react-refresh": "^0.14.0",
     "style-loader": "^3.3.1",
     "ts-loader": "^9.4.2",
     "typescript": "^4.9.4",
-    "url-loader": "^4.1.1",
-    "webpack": "^5.75.0",
-    "webpack-cli": "^4.10.0",
-    "webpack-dev-server": "^4.11.1",
-    "webpack-shell-plugin-next": "^2.3.1"
+    "url-loader": "^4.1.1"
   },
   "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_client": "cross-env NODE_ENV=development webpack-dev-server --hot",
-    "build": "cross-env NODE_ENV=production webpack",
-    "production": "cross-env NODE_ENV=production node server/index.mjs",
-    "build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag g/hhu-adam/robo && rm -rf ./Robo",
-    "build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag g/hhu-adam/nng4 && rm -rf ./NNG4",
-    "update_lean": "./UPDATE_LEAN.sh"
+    "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 relay/index.mjs"
   },
   "eslintConfig": {
     "extends": [

relay/bubblewrap.sh

@@ -2,11 +2,15 @@
 
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
+# $1 : the game directory
+# $2 : the lean4game folder
+# $3 : the gameserver executable
+
 (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 +26,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
   --unshare-uts  \
   --unshare-cgroup \
   --die-with-parent \
-  --chdir "/lean4game/server/build/bin/" \
+  --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
   ./gameserver --server /game
 )

relay/import.mjs

@@ -11,6 +11,7 @@ const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
+const USERNAME = process.env.LEAN4GAME_GITHUB_USER
 const octokit = new Octokit({
   auth: TOKEN
 })
@@ -41,9 +42,10 @@ async function download(id, url, dest) {
     requestProgress(request({
       url,
       headers: {
-        'User-Agent': 'abentkamp',
+        'accept': 'application/vnd.github+json',
+        'User-Agent': USERNAME,
         'X-GitHub-Api-Version': '2022-11-28',
-        'Authorization': 'Bearer '+TOKEN
+        'Authorization': 'Bearer ' + TOKEN
       }
     }))
     .on('progress', function (state) {
@@ -76,35 +78,44 @@ 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(path.join(__dirname, "..", "games"))){
+      fs.mkdirSync(path.join(__dirname, "..", "games"));
+    }
+    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, `tmp/artifact_${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],".")
-    let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
-    manifest = JSON.parse(manifest);
-    if (manifest.length !== 1) {
-      throw `Unexpected manifest: ${JSON.stringify(manifest)}`
-    }
-    manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
-    fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
-    await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
-    await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
+
+    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`);
+    // manifest = JSON.parse(manifest);
+    // if (manifest.length !== 1) {
+    //   throw `Unexpected manifest: ${JSON.stringify(manifest)}`
+    // }
+    // manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
+    // fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
+    // await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
+    // // await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
+
     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 {
+    // clean-up temp. files
     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});
+      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
   }
+  await new Promise(resolve => setTimeout(resolve, 10000))
 }
 
 export const importTrigger = (req, res) => {

relay/index.mjs

@@ -6,25 +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 { 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/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);
@@ -36,11 +31,18 @@ const PORT = process.env.PORT || 8080;
 
 var router = express.Router();
 
-// router.get('/import/status/:owner/:repo', importStatus)
-// router.get('/import/trigger/:owner/:repo', importTrigger)
+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
+    const filename = req.params[0];
+    req.url = filename;
+    express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
+  })
   .use('/', router)
   .listen(PORT, () => console.log(`Listening on ${PORT}`));
 
@@ -54,41 +56,61 @@ 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
+      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 ""
     }
-    // TODO: This test does not work
-    // if (!fs.existsSync(path.join("../", game_dir))) {
-    //   console.error(`Game folder does not exists: ${game_dir}`)
-    //   return
-    // }
   }
 
-  if (!game_dir) {
-    console.error(`Unknown game: ${tag(owner, repo)}`)
-    return
+  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)]
-    serverProcess = cp.spawn("./gameserver", args,
-        { cwd: path.join(__dirname, "./build/bin/") })
+    let args = ["--server", game_dir]
+    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],
+      [ game_dir, path.join(__dirname, '..')],
       { cwd: __dirname })
   }
+
   serverProcess.on('error', error =>
     console.error(`Launching Lean Server failed: ${error}`)
   )
@@ -101,15 +123,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)
 //   }
@@ -122,19 +150,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;
@@ -147,14 +177,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;
@@ -165,9 +195,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())
 })

relay/unpack.sh

@@ -0,0 +1,30 @@
+#/bin/bash
+
+ARTIFACT_ID=$1
+OWNER=$2
+REPO=$3
+
+# mkdir -p games
+cd games
+
+# mkdir -p tmp
+mkdir -p ${OWNER}
+
+echo "Unpacking ZIP."
+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"
+  #tar -xvzf $f -C games/${OWNER}/${REPO}
+  unzip -q -o $f -d ${OWNER}/${REPO}
+done

server/.gitignore

@@ -1,3 +0,0 @@
-build
-adam
-nng

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
@@ -58,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. -/
@@ -71,6 +95,38 @@ 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 "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
 
@@ -626,6 +682,27 @@ 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"
+  if ← FilePath.pathExists "images" then
+    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
@@ -644,6 +721,47 @@ 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
+
+  -- 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)))
+
+  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
@@ -810,8 +928,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
@@ -850,9 +972,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
@@ -864,7 +989,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
@@ -915,14 +1040,25 @@ elab "MakeGame" : command => do
         logError m!"{w1} depends on {w2} because of {items.toList}."
   else
     worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
+
+    -- need to delete all existing edges as they are already present in `worldDependsOnWorlds`.
+    modifyCurGame fun game =>
+      pure {game with worlds := {game.worlds with edges := Array.empty}}
+
     for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
       modifyCurGame fun game =>
         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
 
+  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 +1188,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 -/
 

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 -/
 
@@ -254,8 +265,68 @@ 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
 
+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.
+- 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
+  image: 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
+    image := lvl.image
+  }
 
 /-! ## World -/
 
@@ -271,17 +342,46 @@ 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 -/
 
+/-- 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
@@ -296,8 +396,19 @@ 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
+  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 : β → β → β) :

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
@@ -496,7 +497,7 @@ section NotificationHandling
       IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
     else if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
 
@@ -573,7 +574,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
     This is because LSP always refers to characters by (line, column),
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try

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
@@ -225,26 +97,50 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       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
+
+      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/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

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,10 +122,11 @@ 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 ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+            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 := lctx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
             return some { text := text, hidden := hint.hidden }
           else return none

server/Main.lean

@@ -1,5 +1,9 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
+import GameServer.Commands
+
+-- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
+-- should we have a different solution?
 
 unsafe def main : List String → IO UInt32 := fun args => do
   let e ← IO.getStderr

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": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "GameServer",
+ "lakeDir": ".lake"}

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]
@@ -10,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)

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.1.0
+leanprover/lean4:v4.3.0

server/unpack.sh

@@ -1,13 +0,0 @@
-#/bin/bash
-
-ARTIFACT_ID=$1
-
-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
-do
-  echo "Unpacking $f"
-  mkdir tmp/artifact_${ARTIFACT_ID}_inner
-  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
-done

tsconfig.json

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

vite.config.ts

@@ -0,0 +1,54 @@
+import { defineConfig } from 'vite'
+import react from '@vitejs/plugin-react-swc'
+import { viteStaticCopy } from 'vite-plugin-static-copy'
+import svgr from "vite-plugin-svgr"
+
+// https://vitejs.dev/config/
+export default defineConfig({
+  //root: 'client/src',
+  build: {
+    // Relative to the root
+    // Note: This has to match the path in `relay/index.mjs`
+    outDir: 'client/dist',
+  },
+  plugins: [
+    react(),
+    svgr({
+      svgrOptions: {
+        // svgr options
+      },
+    }),
+    viteStaticCopy({
+      targets: [
+        {
+          src: 'node_modules/@leanprover/infoview/dist/*.production.min.js',
+          dest: '.'
+        }
+      ]
+    })
+  ],
+  publicDir: "client/public",
+  optimizeDeps: {
+    exclude: ['games']
+  },
+  server: {
+    port: 3000,
+    proxy: {
+      '/websocket': {
+        target: 'ws://localhost:8080',
+        ws: true
+      },
+      '/import': {
+        target: 'http://localhost:8080',
+      },
+      '/data': {
+        target: 'http://localhost:8080',
+      },
+    }
+  },
+  resolve: {
+    alias: {
+      path: "path-browserify",
+    },
+  },
+})

webpack.config.js

@@ -1,106 +0,0 @@
-const path = require("path");
-const webpack = require('webpack');
-const ReactRefreshWebpackPlugin = require('@pmmmwh/react-refresh-webpack-plugin');
-const WebpackShellPluginNext = require('webpack-shell-plugin-next');
-
-module.exports = env => {
-
-  const single_game = process.env.LEAN4GAME_SINGLE_GAME
-
-
-  const environment = process.env.NODE_ENV
-  const isDevelopment = environment === 'development'
-
-  const babelOptions = {
-      presets: ['@babel/preset-env', '@babel/preset-react', '@babel/preset-typescript'],
-    plugins: [
-      isDevelopment && require.resolve('react-refresh/babel'),
-    ].filter(Boolean),
-  };
-
-  global.$RefreshReg$ = () => {};
-  global.$RefreshSig$ = () => () => {};
-
-  return {
-    entry: [single_game ? "./client/src/index_local.tsx" : "./client/src/index.tsx"],
-    mode: isDevelopment ? 'development' : 'production',
-    module: {
-      rules: [
-        {
-          test: /\.(js|jsx)$/,
-          exclude: [/server/, /node_modules/],
-          use: [{
-            loader: require.resolve('babel-loader'),
-            options: babelOptions,
-          }]
-        },
-        {
-          test: /\.tsx?$/,
-          use: [{
-            loader: 'ts-loader',
-            options: { allowTsInNodeModules: true }
-          }],
-          // exclude: /node_modules(?!\/(lean4web|lean4|lean4-infoview))/,
-          // Allow .ts imports from node_modules/lean4web and node_modules/lean4
-        },
-        {
-          test: /\.css$/,
-          use: ["style-loader", "css-loader"]
-        },
-        {
-          test: /\.(jpg|png)$/,
-          use: {
-            loader: 'file-loader',
-          },
-        },
-      ]
-    },
-    resolve: {
-      extensions: ["*", ".js", ".jsx", ".tsx", ".ts"],
-      fallback: {
-        "http": require.resolve("stream-http") ,
-        "path": require.resolve("path-browserify")
-      },
-    },
-    output: {
-      path: path.resolve(__dirname, "client/dist/"),
-      filename: "bundle.js",
-    },
-    devServer: {
-      proxy: {
-        '/websocket': {
-           target: 'ws://localhost:8080',
-           ws: true
-        },
-        '/import': {
-          target: 'http://localhost:3000',
-          router: () => 'http://localhost:8080',
-        },
-      },
-      static: path.join(__dirname, 'client/public/'),
-      port: 3000,
-      hot: true,
-    },
-    devtool: "source-map",
-    plugins: [
-      !isDevelopment && new WebpackShellPluginNext({
-        onBuildEnd:{
-          scripts: [
-            // It's hard to set up webpack to copy the index.html correctly,
-            // so we copy it explicitly after every build:
-            'cp client/public/index.html client/dist/',
-            // Similarly, I haven't been able to load `onigasm.wasm` properly:
-            'cp client/public/onigasm.wasm client/dist/',],
-          blocking: false,
-          parallel: true
-        }
-      }),
-      isDevelopment && new ReactRefreshWebpackPlugin(),
-    ].filter(Boolean),
-
-    // Webpack is not happy about the dynamically loaded widget code in the function
-    // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support
-    // dynamically loaded widget code, we need to make sure that the files are available.
-    ignoreWarnings: [/Critical dependency: the request of a dependency is an expression/]
-  };
-}