Merge branch 'v4.4.0'

Mobile option (template)

.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,6 +1,5 @@
 node_modules
 client/dist
-server/build
-server/lakefile.olean
-**/lake-packages/
+games/
+server/.lake
 **/.DS_Store

README.md

@@ -1,6 +1,6 @@
 # Lean 4 Game
 
-This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
+This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
 ## Creating a Game
 
@@ -8,21 +8,29 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 
 * Step 5: [How to Run Games Locally](doc/running_locally.md)
 * Step 7: [How to Update an existing Game](doc/update_game.md)
-
-### Publishing a Game
-
-We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
-
-For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
+* 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 fully written yet.
+
+* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
 
 ## Contributing
 
@@ -34,7 +42,8 @@ Providing the use access to a Lean instance running on the server is a severe se
 
 ## Credits
 
-The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
+
+It 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).
+by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

client/src/app.tsx

@@ -9,20 +9,37 @@ import '@fontsource/roboto/700.css';
 import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
-import { useWindowDimensions } from './window_width';
+import { useMobile } from './hooks';
+import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
+  const { mobile, setMobile, lockMobile, setLockMobile } = useMobile();
+
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
-  const {width, height} = useWindowDimensions()
-  const [mobile, setMobile] = React.useState(width < 800)
+
+  const automaticallyAdjustLayout = () => {
+    const {width} = getWindowDimensions()
+    setMobile(width < AUTO_SWITCH_THRESHOLD)
+  }
+
+  React.useEffect(()=>{
+    if (!lockMobile){
+      void automaticallyAdjustLayout()
+      window.addEventListener('resize', automaticallyAdjustLayout)
+
+      return () => {
+        window.removeEventListener('resize', automaticallyAdjustLayout)
+      }
+    }
+  }, [lockMobile])
 
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile}}>
+        <MobileContext.Provider value={{mobile, setMobile, lockMobile, setLockMobile}}>
           <Outlet />
         </MobileContext.Provider>
       </GameIdContext.Provider>

client/src/components/app_bar.tsx

@@ -5,7 +5,7 @@ import * as React from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
   faArrowRight, faArrowLeft, faXmark, faBars, faCode,
-  faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
+  faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
 import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
@@ -150,22 +150,23 @@ function InventoryButton({pageNumber, setPageNumber}) {
 }
 
 /** the navigation bar on the welcome page */
-export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
   pageNumber: number,
   setPageNumber: any,
   gameInfo: GameInfo,
   toggleImpressum: any,
   toggleEraseMenu: any,
   toggleUploadMenu: any,
-  toggleInfo: any
+  toggleInfo: any,
+  togglePreferencesPopup: () => void;
 }) {
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile, setMobile} = React.useContext(MobileContext)
   const [navOpen, setNavOpen] = React.useState(false)
 
   return <div className="app-bar">
-    <div>
+    <div className='app-bar-left'>
       <Button inverted="false" title="back to games selection" to="/">
         <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
       </Button>
@@ -194,6 +195,9 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
       <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
         <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
       </Button>
+      <Button title="Preferences" inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
+         <FontAwesomeIcon icon={faGear} />&nbsp;Preferences
+       </Button>
     </div>
   </div>
 }
@@ -237,7 +241,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
       </> :
       <>
         {/* DESKTOP VERSION */}
-        <div>
+        <div className='app-bar-left'>
           <HomeButton isDropdown={false} />
           <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
         </div>

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/context.ts

@@ -62,12 +62,18 @@ export const ProofStateContext = React.createContext<{
   setProofState: () => {},
 })
 
-export const MobileContext = React.createContext<{
+export interface IMobileContext {
   mobile : boolean,
   setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-}>({
-  mobile : false,
+  lockMobile: boolean,
+  setLockMobile: React.Dispatch<React.SetStateAction<Boolean>>,
+}
+
+export const MobileContext = React.createContext<IMobileContext>({
+  mobile: false,
   setMobile: () => {},
+  lockMobile: false,
+  setLockMobile: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{

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">
@@ -481,18 +493,20 @@ export function TypewriterInterface({props}) {
                       <Markdown>{props.data?.introduction}</Markdown>
                     </div>
                   }
-                  {mobile && <>
+                  {mobile &&
                     <Hints key={`hints-${i}`}
                       hints={step.hints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
-                    {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                      <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                        Show more help!
-                      </Button>
-                    }
-                  </>
                   }
                   <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+
+                  {mobile && i == proof.length - 1 &&
+                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                      Show more help!
+                    </Button>
+                  }
+
                   {/* Show a message that there are no goals left */}
                   {!step.goals.length && (
                     <div className="message information">
@@ -509,7 +523,7 @@ export function TypewriterInterface({props}) {
               }
             })}
             {mobile && completed &&
-              <div className="button-row">
+              <div className="button-row mobile">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
                     <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
@@ -521,7 +535,7 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress />
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
         }
       </div>
     </div>

client/src/components/inventory.tsx

@@ -2,7 +2,8 @@ import * as React from 'react';
 import { useState, useEffect } from 'react';
 import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
+import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
+import { faClipboard } from '@fortawesome/free-regular-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
@@ -10,10 +11,12 @@ import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
 
-export function Inventory({levelInfo, openDoc, enableAll=false} :
+export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
   {
     levelInfo: LevelInfo|InventoryOverview,
     openDoc: (props: {name: string, type: string}) => void,
+    lemmaTab: any,
+    setLemmaTab: any,
     enableAll?: boolean,
   }) {
 
@@ -31,19 +34,20 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
       }
       <h2>Theorems</h2>
       {levelInfo?.lemmas &&
-        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
       }
     </div>
   )
 }
 
-function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
+function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
   {
     items: InventoryTile[],
     docType: string,
     openDoc(props: {name: string, type: string}): void,
-    defaultTab? : string,
-    level? : LevelInfo|InventoryOverview,
+    tab?: any,
+    setTab?: any,
+    level?: LevelInfo|InventoryOverview,
     enableAll?: boolean,
   }) {
   // TODO: `level` is only used in the `useEffect` below to check if a new level has
@@ -59,8 +63,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
   }
   const categories = Array.from(categorySet).sort()
 
-  const [tab, setTab] = useState(defaultTab)
-
   // Add inventory items from local store as unlocked.
   // Items are unlocked if they are in the local store, or if the server says they should be
   // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
@@ -68,13 +70,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
   let inv: string[] = selectInventory(gameId)(store.getState())
   let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)
 
-  useEffect(() => {
-    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
-    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
-    if (defaultTab) {
-      setTab(defaultTab)
-    }}, [level])
-
   return <>
     {categories.length > 1 &&
       <div className="tab-bar">
@@ -86,24 +81,29 @@ 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}`}
+              item={item}
               showDoc={() => {openDoc({name: item.name, type: docType})}}
               name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
-              disabled={item.disabled} newly={item.new} enableAll={enableAll}/>
+              disabled={item.disabled} newly={item.new} enableAll={enableAll} />
         })
       }
     </div>
     </>
 }
 
-function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
   const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
-               disabled ? <FontAwesomeIcon icon={faBan} /> : ""
+               disabled ? <FontAwesomeIcon icon={faBan} /> : item.st
   const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
+  // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
+  // `Namespace.statement_name (x y : Nat) : some type`
   const title = locked ? "Not unlocked yet" :
-                disabled ? "Not available in this level" : ""
+                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
+
+  const [copied, setCopied] = useState(false)
 
   const handleClick = () => {
     if (enableAll || !locked) {
@@ -111,7 +111,21 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena
     }
   }
 
-  return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</div>
+  const copyItemName = (ev) => {
+    navigator.clipboard.writeText(displayName)
+    setCopied(true)
+    setInterval(() => {
+      setCopied(false)
+    }, 3000);
+    ev.stopPropagation()
+  }
+
+return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>
+    {icon} {displayName}
+    <div className="copy-button" onClick={copyItemName}>
+      {copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
+    </div>
+  </div>
 }
 
 export function Documentation({name, type, handleClose}) {
@@ -131,16 +145,25 @@ export function Documentation({name, type, handleClose}) {
 export function InventoryPanel({levelInfo, visible = true}) {
   const gameId = React.useContext(GameIdContext)
 
+  const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
+
   // 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)}
 
+    useEffect(() => {
+    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
+    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
+    if (levelInfo?.lemmaTab) {
+      setLemmaTab(levelInfo?.lemmaTab)
+    }}, [levelInfo])
+
   return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
     {inventoryDoc ?
       <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
       :
-      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true}/>
+      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
     }
   </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

@@ -18,11 +18,10 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
 
 import { GameIdContext } from '../app'
-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'
@@ -32,8 +31,9 @@ import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContex
   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'
@@ -43,12 +43,20 @@ import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
 import '../css/level.css'
 import { LevelAppBar } from './app_bar'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient'
+import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader'
+import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
+import { IConnectionProvider } from 'monaco-languageclient'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+import { onigasmH } from 'onigasm/lib/onigasmH'
+
+
+monacoSetup()
 
 function Level() {
   const params = useParams()
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
-  // useLoadWorldFiles(worldId)
 
   const [impressum, setImpressum] = React.useState(false)
 
@@ -138,19 +146,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,10 +217,13 @@ function PlayableLevel({impressum, setImpressum}) {
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(MobileContext)
 
-  const difficulty = useSelector(selectDifficulty(gameId))
+  const dispatch = useAppDispatch()
+
   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 +237,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)}
@@ -284,12 +299,6 @@ function PlayableLevel({impressum, setImpressum}) {
   // a hint at the beginning of the proof...
   const [selectedStep, setSelectedStep] = useState<number>()
 
-  // if the user inventory changes, notify the server
-  useEffect(() => {
-    let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
-  }, [inventory])
-
   useEffect (() => {
     // Lock editor mode
     if (level?.data?.template) {
@@ -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(),
@@ -365,7 +372,7 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (editor && typewriterMode) {
+    if (onigasmH && editor && typewriterMode) {
       let code = editor.getModel().getLinesContent().filter(line => line.trim())
       editor.executeEdits("typewriter", [{
         range: editor.getModel().getFullModelRange(),
@@ -388,7 +395,7 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode])
+  }, [editor, typewriterMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -434,6 +441,7 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
+  const {mobile} = React.useContext(MobileContext)
 
   let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
 
@@ -444,7 +452,7 @@ function IntroductionPanel({gameInfo}) {
           hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     </div>
-    <div className="button-row">
+    <div className={`button-row${mobile ? ' mobile' : ''}`}>
       {gameInfo.data?.worldSize[worldId] == 0 ?
         <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
         <Button to={`/${gameId}/world/${worldId}/level/1`}>
@@ -466,6 +474,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,7 +492,13 @@ 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>
+          <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>
           <InventoryPanel levelInfo={inventory?.data} />
         </Split>
       }
@@ -512,21 +531,32 @@ function Introduction({impressum, setImpressum}) {
 
 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
 
-  const connection = React.useContext(ConnectionContext)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
 
-
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState<null|InfoviewApi>(null)
   const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)
 
-  // Create Editor
+  const uriStr = `file:///${worldId}/${levelId}`
+  const uri = monaco.Uri.parse(uriStr)
+
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
+  const difficulty: number = useSelector(selectDifficulty(gameId))
+
   useEffect(() => {
+    const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
+    if (onDidChangeContent) {
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+    }
+
     const editor = monaco.editor.create(codeviewRef.current!, {
+      model,
       glyphMargin: true,
       quickSuggestions: false,
+      lineDecorationsWidth: 5,
+      folding: false,
+      lineNumbers: 'on',
       lightbulb: {
         enabled: true
       },
@@ -538,11 +568,61 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
         enabled: false
       },
       lineNumbersMinChars: 3,
+      tabSize: 2,
       'semanticHighlighting.enabled': true,
       theme: 'vs-code-theme-converted'
     })
+    if (onDidChangeSelection) {
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+    }
+    if (initialSelections) {
+      console.debug("Initial Selection: ", initialSelections)
+      // BUG: Somehow I get an `invalid arguments` bug here
+      // editor.setSelections(initialSelections)
+    }
+    setEditor(editor)
+    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-    const infoProvider = new InfoProvider(connection.getLeanClient(gameId))
+    const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
+
+    const connectionProvider : IConnectionProvider = {
+      get: async () => {
+        return await new Promise((resolve, reject) => {
+          console.log(`connecting ${socketUrl}`)
+          const websocket = new WebSocket(socketUrl)
+          websocket.addEventListener('error', (ev) => {
+            reject(ev)
+          })
+          websocket.addEventListener('message', (msg) => {
+            // console.log(msg.data)
+          })
+          websocket.addEventListener('open', () => {
+            const socket = toSocket(websocket)
+            const reader = new DisposingWebSocketMessageReader(socket)
+            const writer = new WebSocketMessageWriter(socket)
+            resolve({
+              reader,
+              writer
+            })
+          })
+        })
+      }
+    }
+
+    // Following `vscode-lean4/webview/index.ts`
+    const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
+    const infoProvider = new InfoProvider(client)
+    // const div: HTMLElement = infoviewRef.current!
+    const imports = {
+      '@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
+      'react': `${window.location.origin}/react.production.min.js`,
+      'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
+      'react-dom': `${window.location.origin}/react-dom.production.min.js`,
+      'react-popper': `${window.location.origin}/react-popper.production.min.js`
+    }
+    // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
+    setInfoProvider(infoProvider)
+    client.restart()
 
     const editorApi = infoProvider.getApi()
 
@@ -587,77 +667,27 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
     setEditor(editor)
     setInfoProvider(infoProvider)
-    setInfoviewApi(infoviewApi)
 
-    return () => { infoProvider.dispose(); editor.dispose() }
-  }, [])
+    infoProvider.openPreview(editor, infoviewApi)
+    const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
 
-  const {leanClient, leanClientStarted} = useLeanClient(gameId)
-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
+    // TODO:
+    // setRestart(() => restart)
 
-  // Create model when level changes
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      if (!model) {
-        model = monaco.editor.createModel(initialCode, 'lean4', uri)
-      }
-      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-      editor.setModel(model)
-      if (initialSelections) {
-        console.debug("Initial Selection: ", initialSelections)
-        // BUG: Somehow I get an `invalid arguments` bug here
-        // editor.setSelections(initialSelections)
-      }
-
-      return () => {
-        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-      }
+    return () => {
+      editor.dispose();
+      model.dispose();
+      abbrevRewriter.dispose();
+      taskgutter.dispose();
+      infoProvider.dispose();
+      client.dispose();
     }
-  }, [editor, levelId, connection, leanClientStarted])
+  }, [gameId, worldId, levelId])
 
-
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      infoviewApi.serverRestarted(leanClient.initializeResult)
-
-      infoProvider.openPreview(editor, infoviewApi)
-
-      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
-    }
-  }, [editor, connection, leanClientStarted])
+  const showRestartMessage = () => {
+    // setRestartMessage(true)
+    console.log("TODO: SHOW RESTART MESSAGE")
+  }
 
   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/popup/preferences.tsx

@@ -0,0 +1,55 @@
+import * as React from 'react'
+import { Input, Typography } from '@mui/material'
+import Markdown from '../markdown'
+import Switch from '@mui/material/Switch';
+import FormControlLabel from '@mui/material/FormControlLabel';
+
+import { IMobileContext } from "../infoview/context"
+
+interface PreferencesPopupProps extends IMobileContext{
+    handleClose: () => void
+} 
+
+export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
+    return <div className="modal-wrapper">
+        <div className="modal-backdrop" onClick={handleClose} />
+        <div className="modal">
+            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+            <Typography variant="body1" component="div" className="settings">
+                <div className='preferences-category'>
+                    <div className='category-title'>
+                        <h3>Mobile layout</h3>
+                    </div>
+                    <div className='preferences-item'>
+                        <FormControlLabel
+                            control={
+                            <Switch
+                                checked={mobile}
+                                onChange={() => setMobile(!mobile)}
+                                name="checked"
+                                color="primary"
+                            />
+                            }
+                            label="Enable"
+                            labelPlacement="start"
+                        />
+                    </div>
+                    <div className='preferences-item'>
+                        <FormControlLabel
+                            control={
+                            <Switch
+                                checked={!lockMobile}
+                                onChange={() => setLockMobile(!lockMobile)}
+                                name="checked"
+                                color="primary"
+                            />
+                            }
+                            label="Auto"
+                            labelPlacement="start"
+                        />
+                    </div>
+                </div>
+            </Typography>
+        </div>
+    </div>
+}

client/src/components/welcome.tsx

@@ -17,6 +17,7 @@ import { InfoPopup } from './popup/game_info'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import { RulesHelpPopup } from './popup/rules_help'
 import { UploadPopup } from './popup/upload'
+import { PreferencesPopup} from "./popup/preferences"
 import { WorldTreePanel } from './world_tree'
 
 import '../css/welcome.css'
@@ -63,7 +64,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
@@ -77,15 +78,20 @@ function Welcome() {
   const [info, setInfo] = React.useState(false)
   const [rulesHelp, setRulesHelp] = React.useState(false)
   const [uploadMenu, setUploadMenu] = React.useState(false)
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+
   function closeEraseMenu()   {setEraseMenu(false)}
   function closeImpressum()   {setImpressum(false)}
   function closeInfo()        {setInfo(false)}
   function closeRulesHelp()   {setRulesHelp(false)}
   function closeUploadMenu()  {setUploadMenu(false)}
+  function closePreferencesPopup() {setPreferencesPopup(false)}
   function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
   function toggleImpressum()  {setImpressum(!impressum)}
   function toggleInfo()       {setInfo(!info)}
   function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
+  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
+
 
   // set the window title
   useEffect(() => {
@@ -101,7 +107,7 @@ function Welcome() {
   : <>
     <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
       toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
-      toggleInfo={toggleInfo} />
+      toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
     <div className="app-content">
       { mobile ?
           <div className="welcome mobile">
@@ -128,6 +134,7 @@ function Welcome() {
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
+    {preferencesPopup ? <PreferencesPopup mobile={mobile} setMobile={setMobile} lockMobile={lockMobile} setLockMobile={setLockMobile} handleClose={closePreferencesPopup}/> : null}
   </>
 }
 

client/src/components/world_tree.tsx

@@ -11,7 +11,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch } from '../hooks'
+import { useAppDispatch, useMobile } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
 
@@ -197,13 +197,15 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
+  const { mobile } = useMobile()
+
 
   function label(x : number) {
     return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
   }
 
 
-  return <nav className="world-selection-menu">
+  return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
     <div className="slider-wrap">
       <span className="difficulty-label">Rules
         <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
@@ -213,7 +215,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
         title="Game Rules"
         min={0} max={2}
         aria-label="Game Rules"
-        defaultValue={difficulty}
+        value={difficulty}
         marks={[
           {value: 0, label: label(0)},
           {value: 1, label: label(1)},

client/src/connection.ts

@@ -1,68 +0,0 @@
-/**
- *  @fileOverview todo
- */
-
-import * as React from 'react';
-import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { LeanClient } from 'lean4web/client/src/editor/leanclient';
-
-export class Connection {
-  private game: string = undefined // We only keep a connection to a single game at a time
-  private leanClient: LeanClient = null
-
-  getLeanClient(game): LeanClient {
-    if (this.game !== game) {
-      if (this.leanClient) {
-        this.leanClient.stop() // Stop previous Lean client
-      }
-      this.game = game
-      // Start a new Lean client for the new `gameId`.
-      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
-      const uri = monaco.Uri.parse('file:///')
-      this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
-    }
-
-    return this.leanClient
-  }
-
-  /** If not already started, starts the Lean client. resolves the returned promise as soon as a
-   * Lean client is running.
-   */
-  startLeanClient = (game) => {
-    return new Promise<LeanClient>((resolve) => {
-      const leanClient = this.getLeanClient(game)
-      if (leanClient.isRunning()) {
-        resolve(leanClient)
-      } else {
-        if (!leanClient.isStarted()) {
-          leanClient.start()
-        }
-        leanClient.restarted(() => {
-          // This keep alive message is not recognized by the server,
-          // but it makes sure that the websocket connection does not
-          // time out after 60 seconds.
-          setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
-          resolve(leanClient)
-        })
-      }
-    })
-  }
-}
-
-export const connection = new Connection()
-
-export const ConnectionContext = React.createContext(null);
-
-export const useLeanClient = (gameId) => {
-  const leanClient = connection.getLeanClient(gameId)
-  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
-
-  React.useEffect(() => {
-    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
-    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
-
-    return () => {t1.dispose(); t2.dispose()}
-  }, [leanClient, setLeanClientStarted])
-
-  return {leanClientStarted, leanClient}
-}

client/src/css/app.css

@@ -105,11 +105,18 @@ em {
   position: relative;
   flex-direction: row;
   justify-content: space-between;
+  align-items: center;
   padding: 1.1em;
   filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
   z-index: 2;
 }
 
+.app-bar > .app-bar-left{
+  display: flex;
+  align-items: center;
+  gap: .5em;
+}
+
 .app-bar-title, .app-bar-subtitle {
   color: white;
   font-weight: 500;

client/src/css/inventory.css

@@ -26,7 +26,11 @@
 .inventory .item {
   background: #fff;
   border: solid 1px #777;
-  padding: .1em .5em;
+  padding-left: .5rem;
+  padding-right: 1.0rem;
+  padding-top: .1rem;
+  padding-bottom: .1rem;
+  position: relative;
 }
 
 .inventory .item.locked {
@@ -72,3 +76,21 @@
   color: black;
   border-bottom: 0.3em solid #999;
 }
+
+
+.inventory .item .copy-button {
+	min-width: 3px;
+	min-height: 3px;
+	display: inline-block;
+	color: #ccc;
+	font-size: 0.6em;
+	padding-right: .2rem;
+	vertical-align: top;
+	position: absolute;
+	top: 0;
+	right: 0;
+	height: 100%;
+	width: 1rem;
+	align-items: end;
+	text-align: end;
+}

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

@@ -232,6 +232,20 @@ td code  {
   height: 100%;
 } */
 
+.button-row.mobile {
+  margin: .5rem;
+  padding-top: .2rem;
+}
+
+.button-row.mobile .btn {
+  padding: .5em;
+  border-radius: .2em;
+  width: 100%;
+  margin: 0;
+  text-align: center;
+}
+
+
 .typewriter-interface {
   display: flex;
   flex-flow: column;
@@ -317,11 +331,6 @@ td code  {
   margin-right: 0;
 }
 
-#home-btn {
-  margin-right: .5em;
-  margin-left: 0;
-}
-
 .menu.dropdown .svg-inline--fa {
   width: 1.8rem;
 }
@@ -336,6 +345,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/css/world_tree.css

@@ -49,7 +49,6 @@ svg .disabled {
 }
 
 .world-selection-menu {
-  position: absolute;
   right: 1em;
   top: 1em;
   /* margin: 1em; */
@@ -60,6 +59,10 @@ svg .disabled {
   filter: drop-shadow(4px 4px 5px rgba(0,0,0,0.5));
 }
 
+.world-selection-menu.desktop {
+  position: absolute;
+}
+
 .world-selection-menu .btn, .welcome .btn {
   min-width: 5em;
   text-align: center;

client/src/hooks.ts

@@ -1,6 +1,30 @@
 import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
 import type { RootState, AppDispatch } from './state/store'
 
+import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences"
+
 // Use throughout your app instead of plain `useDispatch` and `useSelector`
 export const useAppDispatch: () => AppDispatch = useDispatch
 export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector
+
+export const useMobile = () => {
+  const dispatch = useAppDispatch();
+
+  const mobile = useAppSelector((state) => state.preferences.mobile);
+  const lockMobile = useAppSelector((state) => state.preferences.lockMobile);
+
+  const setMobile = (val: boolean) => {
+    dispatch(setMobileState(val));
+  };
+
+  const setLockMobile = (val: boolean) => {
+    dispatch(setLockMobileState(val));
+  };
+
+  return {
+    mobile,
+    setMobile,
+    lockMobile,
+    setLockMobile,
+  };
+};

client/src/index.tsx

@@ -1,7 +1,6 @@
 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 type { RouteObject } from "react-router"
@@ -10,20 +9,8 @@ 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()
-
-// // Do not show the landing page in the dev-container context
-// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? {
-//   path: "/",
-//   loader: () => redirect("/g/local/game")
-// } : {
-//   path: "/",
-//   element: <LandingPage />,
-// }
-
 
 // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
 // `/g/local/game`. This is used for the devcontainer setup
@@ -43,6 +30,11 @@ const router = createHashRouter([
     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 />,
@@ -65,9 +57,7 @@ const root = createRoot(container!);
 root.render(
   <React.StrictMode>
     <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
+      <RouterProvider router={router} />
     </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 {
@@ -22,6 +35,7 @@ export interface InventoryTile {
   locked: boolean,
   new: boolean,
   hidden: boolean
+  altTitle: string,
 }
 
 export interface LevelInfo {
@@ -37,7 +51,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 +72,22 @@ interface Doc {
   category: string,
 }
 
-
-const customBaseQuery = async (
-  args : {game: string, method: string, params?: any},
-  { signal, dispatch, getState, extra },
-  extraOptions
-) => {
-  try {
-    const connection : Connection = extra.connection
-    let leanClient = await connection.startLeanClient(args.game)
-    console.log(`Sending request ${args.method}`)
-    let res = await leanClient.sendRequest(args.method, args.params)
-    console.log('Received response') //, res)
-    return {'data': res}
-   } catch (e) {
-    return {'error': e}
-   }
-}
-
 // Define a service using a base URL and expected endpoints
 export const apiSlice = createApi({
   reducerPath: 'gameApi',
-  baseQuery: customBaseQuery,
+  baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/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: {}}},
+      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/local_storage.ts

@@ -36,3 +36,24 @@ export async function saveState(state: any) {
     // Ignore
   }
 }
+
+const PREFERENCES_KEY = "preferences"
+
+/** Load from browser storage */
+export function loadPreferences() {
+  try {
+    const serializedState = localStorage.getItem(PREFERENCES_KEY);
+    return JSON.parse(serializedState)
+  } catch (e) {
+    return undefined;
+  }
+}
+
+export function savePreferences(state: any) {
+  try {
+    const serializedState = JSON.stringify(state)
+    localStorage.setItem(PREFERENCES_KEY, serializedState);
+  } catch (e) {
+    // Ignore
+  }
+}

client/src/state/preferences.ts

@@ -0,0 +1,37 @@
+import { createSlice } from "@reduxjs/toolkit";
+
+import { loadPreferences } from "./local_storage";
+
+interface PreferencesState {
+  mobile: boolean;
+  lockMobile: boolean;
+}
+
+export function getWindowDimensions() {
+  const {innerWidth: width, innerHeight: height } = window
+  return {width, height}
+}
+
+const { width } = getWindowDimensions()
+
+export const AUTO_SWITCH_THRESHOLD = 800
+
+const initialState: PreferencesState = loadPreferences() ?? {
+    mobile: width < AUTO_SWITCH_THRESHOLD,
+    lockMobile: false
+}
+
+export const preferencesSlice = createSlice({
+  name: "preferences",
+  initialState,
+  reducers: {
+    setMobile: (state, action) => {
+      state.mobile = action.payload;
+    },
+    setLockMobile: (state, action) => {
+      state.lockMobile = action.payload;
+    },
+  },
+});
+
+export const { setMobile, setLockMobile } = preferencesSlice.actions;

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

client/src/state/store.ts

@@ -7,21 +7,19 @@ import { debounce } from "debounce";
 import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
-import { saveState } from "./local_storage";
+import { preferencesSlice } from "./preferences"
+import { saveState, savePreferences } from "./local_storage";
 
 
 export const store = configureStore({
   reducer: {
     [apiSlice.reducerPath]: apiSlice.reducer,
     [progressSlice.name]: progressSlice.reducer,
+    [preferencesSlice.name]: preferencesSlice.reducer,
   },
   // Make connection available in thunks:
   middleware: getDefaultMiddleware =>
-    getDefaultMiddleware({
-      thunk: {
-        extraArgument: { connection }
-      }
-    }).concat(apiSlice.middleware),
+    getDefaultMiddleware().concat(apiSlice.middleware),
 });
 
 /**
@@ -31,6 +29,7 @@ export const store = configureStore({
 store.subscribe(
   debounce(() => {
     saveState(store.getState()[progressSlice.name]);
+    savePreferences(store.getState()[preferencesSlice.name]);
   }, 800)
 );
 

client/src/window_width.tsx

@@ -1,21 +0,0 @@
-import {useState, useEffect} from 'react'
-
-function getWindowDimensions() {
-  const {innerWidth: width, innerHeight: height } = window
-  return {width, height}
-}
-
-export function useWindowDimensions() {
-  const [windowDimensions, setWindowDimensions] = useState(getWindowDimensions())
-
-  useEffect(() => {
-    function handleResize() {
-      setWindowDimensions(getWindowDimensions())
-    }
-    window.addEventListener('resize', handleResize)
-    return () => window.removeEventListener('resize', handleResize)
-
-  }, [])
-
-  return windowDimensions
-}

doc/DOCUMENTATION.md

@@ -1,332 +1,67 @@
-# Creating a game.
+# Server
 
-Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
+The server is made out of two parts, named "relay" and "server".
 
-## Game Structure
+The former, "relay", is the server which
+sets up a socket connection to the client, starts the lean servers to work on files and
+relays messages between the lean server and the client. `index.mjs` is the file that needs to
+be run, which is done for example using `pm2` or by calling `npm run start_server` or
+`npm run production`, see more later.
 
-A game consist of worlds which have multiple levels each. In the following we describe how to create a level file and how to combine these into a game.
+The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver"
+executable which is the lean server that handles the files the player plays on. The second job
+is to provide the lean commands which are used when creating a game. These are located in
+`Commands.lean`.
 
-### Level
 
-A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
+## Integration into Games
+
+Games need the "server" as a lake-dependency, which is done in the game's lakefile.
+
+A game imports `GameServer.Commands` which provides to all the API required to
+create a game.
+
+In particular the lean command `MakeGame` compiles the entire game. Static information is
+stored as JSON files in `.lake/gamedata` for faster loading, while other data is only
+saved to lean env-extensions which the lean server has access to after loading the lean file.
+
+For games to be run successfully, it is important that the "gameserver" executable inside
+the game's `.lake` folder is actually built.
+Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
+(both commands are to be executed in the game's directory!)
+
+## Modifying the server
+
+### Starting the server
+
+When using the [manual installation](running_locally.md#manual-installation) you can run the server
+using
 
-```lean
-Game "NNG"
-World "Addition"
-Level 1
-Title "The rfl tactic"
 ```
-
-Note that the levels inside a world must have consecutive numbering starting with `1`. The `Game`
-and `World` strings can be anything, see below.
-
-#### Statement
-
-The core of a level is the `Statement`, which is the exercise that should be proven.
-
-```lean
-/-- For all natural numbers $n$, we have $0 + n = n$. -/
-@[simp]
-Statement MyNat.zero_add
-    (n : ℕ) : 0 + n = n := by
-  Hint "You can start a proof by `induction n`."
-  induction n with n hn
-  · Hint "This is the base case."
-    rw [add_zero]
-    rfl
-  · Hint "This is the induction hypothesis"
-    rw [add_succ]
-    Branch
-      simp
-      Hint "A branch is an alternative tactic sequence. Does not need to finish the proof."
-    rw [hn]
-    rfl
-```
-
-##### Proof
-
-The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
-
-There are a few extra tactics that help you structuring the proof:
-
-- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
-  the one where `Hint` is placed. For more options about hints, see below.
-- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different   places. The `Branch` does not affect the main
-  proof and does not need to finish any goals.
-- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
-  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
-  having a `Template` will force the user to use Editor-mode for this level.
-
-##### Statement Name (optional)
-
-If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels.
-(Note that a future level must also import this level,
-so that Lean knows about the added statement).
-
-The name must be *fully qualified*. (TODO: is that still true? Did we implement namespaces?)
-
-##### Doc Comment (optional)
-
-There are three places where the documentation comment appears:
-
-1. as doc comment when hovering over the theorem
-2. as exercise description at the top of the level: ``Theorem `zero_add`: yada yada.``
-3. in the inventory. This can be overwritten by using
-  `LemmaDoc MyNat.zero_add "different yada yada"` as one might want to add a more detailed
-  description there including examples etc.
-
-Both latter points support Markdown (including katex).
-
-##### Attributes (optional)
-
-the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
-
-#### Introduction/Conclusion
-
-Optionally, you can add an `Introduction "some text"` and `Conclusion "some text"` to your level.
-The introduction will be shown at the beginning, the conclusion is displayed once the level
-is solved.
-
-#### Theorems/Tactics/Definitions
-
-Only enabled theorems/tactics/definitions (called "items" here) are available in a level.
-
-To add a new item in a level, you can add
-
-```lean
-NewTactic rfl simp
-NewLemma MyNat.add_zero MyNat.add_succ
-NewDefinition Nat Pow Mul
-```
-
-Once added, items will be available in all future levels/worlds,
-unless you disable them for a particular level with
-
-```lean
-DisabledTactic tauto
-DisabledLemma MyNat.add_zero
-```
-
-or specify explicitly which items should be available with
-
-```lean
-OnlyTactic rw rfl apply
-OnlyLemma MyNat.add_zero
-```
-
-Lastly, all items need documentation entries (which are imported in the level),
-see more about that below. There is also explains the `LemmaTab` keyword.
-
-### World
-
-Multiple levels are combined into a world and the worlds are then added to the game. It is recommended that all levels of a world are inside one folder (e.g. `NNG/Levels/Addition/`) and
-then there is one world file (`NNG/Levels/Addition.lean`) which contains the following
-
-```lean
-import NNG.Levels.Addition.Level_1
-import NNG.Levels.Addition.Level_2
-
-Game "NNG"
-World "Addition"
-Title "Addition World"
-
-Introduction "some text"
-```
-
-The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
-Note that all levels of a world should be imported by the world file.
-
-BUG: A level **must not** be imported in a different world's level. Instead, you have to import an entire world there: `import NNG.Levels.Addition`
-
-### Game
-
-The Game itself (i.e. the main file of you lake project, `NNG.lean`) should import all worlds and have the following layout, concluding with `MakeGame`:
-
-```lean
-import NNG.Levels.Addition
-import NNG.Levels.Multiplication
-import NNG.Levels.Power
-
-Game "NNG"
-Title "Natural Number Game"
-Introduction "some text"
-
-MakeGame
-```
-
-The game will automatically compute the order of the worlds depending on the sample proofs of the Levels (ignoring anything inside a `Branch`). You can add additional dependencies manually by adding `Dependency PowerWorld → ImpossibleWorld` before `MakeGame`.
-The order of worlds influences which tactics and lemmas will be unlocked in a given level.
-
-`MakeGame` will display warnings about things in the game that need to be fixed, like missing
-documentation or if a tactic is never introduced.
-
-### Documentation
-
-Each tactic, theorem, or definition (all called items here) that is introduced in the game
-needs a documentation entry. These are statements of the following form:
-
-```lean
-LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
-"(missing)"
-
-TacticDoc constructor
-"(missing)"
-
-DefinitionDoc One as "1"
-"(missing)"
-```
-
-Notes:
-
-* The lemma name must be **fully qualified**. The string display name can be arbitrary.
-* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
-  without french quotes.
-* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
-
-Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level file, you
-can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.
-
-There will be features added to get automatic information from mathlib!
-
-## Escaping
-(TODO: Move)
-
-
-Inside the doc comment you don't need to escape the backslashes:
-
-```lean
-/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
-Statement ...
-```
-
-However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclusion`)
-you do need to escape backslashes
-with `\\` and `{` with `\{`:
-
-```lean
-Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
-Notation for naturals is `\\N`."
-```
-
-## Game design
-Here are some things you should consider designing a new game:
-
-* A world with more than 16 levels will be displayed with the levels spiraling outwards,
-  it might be desirable to stay below that bound. Above 22 levels the spiral start getting out
-  of control.
-
-# Running Games Locally
-
-The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
-
-## VSCode Dev Containers
-
-1.  **Install Docker and Dev Containers** *(once)*:<br/>
-    See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
-    Explicitly this means:
-    * Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
-      I followed the "Server" instructions for linux.
-    * Note that on Linux you need to add your user to the `docker` group
-      ([see instructions](https://docs.docker.com/engine/install/linux-postinstall/)) and probably reboot.
-    * Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
-    * a message appears prompting you to install the "Dev Containers" extension (by Microsoft).
-
-2.  **Open Project in Dev Container** *(everytime)*:<br/>
-    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
-      start this should be very quickly.
-    * Once built, it should open a tab "Simple Browser" inside VSCode displaying
-      the game. (Alternatively, open http://localhost:3000 in your browser).
-
-3.  **Editing Files** *(everytime)*:<br/>
-    After editing some files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`.
-    Now you can reload your browser to see the changes.
-
-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-
-
-## Without Dev Containers
-Install `nvm`:
-```bash
-curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
-```
-then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
-
-Now install node:
-```bash
-nvm install node
-```
-
-Clone the game (e.g. `NNG4` here):
-```bash
-git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/NNG4.git
-```
-
-Download dependencies and build the game:
-```bash
-cd NNG4
-lake update
-lake exe cache get   # if your game depends on mathlib
-lake build
-```
-
-Clone the game 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!
-
-In `lean4game`, install dependencies:
-```bash
-cd lean4game
-npm install
-```
-
-If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/server/index.mjs`:
-```typescript
-const games = {
-    "g/hhu-adam/robo": {
-        dir: "../../../../Robo",
-        queueLength: 5
-    },
-    "g/hhu-adam/nng4": {
-        dir: "../../../../NNG4",
-        queueLength: 5
-    }
-}
-```
-
-Run the game:
-```bash
 npm start
 ```
 
-This takes a little time. Eventually, the server is available on http://localhost:3000/
-and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
+This way any changes to files in `client/` or `relay/` will cause the server to restart automatically.
 
-### Modifying the GameServer
+Alternative, you can run `npm run build` followed by the commands
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
-setup by setting `export NODE_ENV=development` inside your local game before building it:
-
-```bash
-cd NNG4
-export NODE_ENV=development
-lake update
-lake build
 ```
-This causes lake to search locally for the `GameServer` lake package instead of using the version from github.
+npm run start_client
+npm run production
+```
+
+(in two separate terminals) to test the production modus of the server. This way it will only
+change once you build and restart the server.
+
+### Modifying the lean server
+
+To test a modified lean server (i.e. content of `server/`), you can use the local dev setup and call
+`lake update -R -Klean4game.local` in your game followed by `lake build`.
+This will cause lake to look for the
+local lean server as a dependency instead of the version it downloaded from git.
+
+You can play a local game at https://localhost:3000/#/g/local/{FolderName} where you replace `{FolderName}` with the game folder name.
+
+After modifications in `server/`, you will need to call `lake build gameserver` (called in `server/` or in your game's folder) to rebuild
+the gameserver executable and
+`lake build` (called in the game's folder) to rebuild the game.

doc/create_game.md

@@ -129,6 +129,9 @@ NewLemma Nat.zero_mul
 NewDefinition Pow
 ```
 
+**Important:** All commands in this section 6a) expect the `Name` they take as input
+to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`.
+
 #### Doc entries
 
 You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
@@ -182,6 +185,8 @@ The statement is the exercise of the level. the basics work the same as they wou
 
 You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
 
+You can but a `Statement` inside namespaces like you would with `theorem`.
+
 #### Doc String / Exercise statement
 
 Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
@@ -223,29 +228,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:
-
-```
-Hint "now use `rw [{h}]` to use your assumption {h}."
-```
-That way, the game will replace it with the actual name the assumption has in the player's proof state.
+NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
 
 ## 7. Update your game
 
-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](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md).
+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"
+```
+* `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,89 @@
+# 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"
+  ...
+```
+
+Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof.
+
+## 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

@@ -85,12 +85,11 @@ git clone https://github.com/hhu-adam/GameSkeleton.git
 Download dependencies and build the game:
 ```bash
 cd GameSkeleton
-lake update
-lake exe cache get   # if your game depends on mathlib
+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
@@ -113,12 +112,12 @@ This takes a little time. Eventually, the game is available on http://localhost:
 
 ## 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 LEAN4GAME=local` 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 LEAN4GAME=local
-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

@@ -9,29 +9,44 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
 
 Then, depending on the setup you use, do one of the following:
 
-* Dev Container: Rebuild the VSCode Devcontainer.
-* Local Setup: run `lake update` (followed by `lake exe cache get` if you depend on mathlib.)
-* Gitpod/Codespaces: Create a fresh one
+* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
+* **Local Setup**: in your game's folder run the following:
+  ```
+  lake update -R
+  lake build
+  ```
 
-This will update `lean4game` and `mathlib` in your project to the new lean version.
+  * 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're developing setup, for example because it doesn't work
+(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
-.devcontainer/**
-.docker/**
-.gitpod
-.vscode/**
 ```
 
-simply copy them from the `GameSkeleton` into your game.
+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.)
+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
     },
   }]
 }

package.json

@@ -1,6 +1,7 @@
 {
   "name": "lean4-game",
   "version": "0.1.0",
+  "type": "module",
   "private": true,
   "homepage": ".",
   "dependencies": {
@@ -9,6 +10,10 @@
     "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",
     "@fontsource/roboto-mono": "^4.5.8",
+    "@fortawesome/fontawesome-svg-core": "^6.5.1",
+    "@fortawesome/free-regular-svg-icons": "^6.5.1",
+    "@fortawesome/free-solid-svg-icons": "^6.5.1",
+    "@fortawesome/react-fontawesome": "^0.2.0",
     "@leanprover/infoview": "^0.4.3",
     "@mui/icons-material": "^5.11.0",
     "@mui/material": "^5.11.1",
@@ -23,7 +28,7 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web",
+    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
     "octokit": "^2.0.14",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
@@ -36,6 +41,7 @@
     "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",
@@ -52,7 +58,7 @@
     "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",
@@ -61,12 +67,13 @@
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "cd server && lake build && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
+    "start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")",
     "start_client": "cross-env NODE_ENV=development vite --host",
     "build": "npm run build_server && npm run build_client",
+    "preview": "vite preview",
     "build_server": "cd server && lake build",
     "build_client": "cross-env NODE_ENV=production vite build",
-    "production": "cross-env NODE_ENV=production node server/index.mjs"
+    "production": "cross-env NODE_ENV=production node relay/index.mjs"
   },
   "eslintConfig": {
     "extends": [

relay/bubblewrap.sh

@@ -1,12 +1,17 @@
 #/bin/bash
 
+# Note: This fails if there is no default toolchain installed
 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 +27,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.lean

@@ -1,5 +1,4 @@
 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`
@@ -10,13 +9,9 @@ unsafe def main : List String → IO UInt32 := fun args => do
 
   Lean.enableInitializersExecution
 
+  -- TODO: remove this argument
   if args[0]? == some "--server" then
-    MyServer.Watchdog.watchdogMain args
-  else if args[0]? == some "--worker" then
-    MyServer.FileWorker.workerMain {}
+    MyServer.FileWorker.workerMain {} args
   else
-    e.putStrLn s!"Expected `--server` or `--worker`"
+    e.putStrLn s!"Expected `--server`"
     return 1
-
-
--- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection

server/GameServer/Commands.lean

@@ -1,23 +1,12 @@
-import GameServer.EnvExtensions
+import GameServer.Helpers
+import GameServer.Inventory
+import GameServer.Options
+import GameServer.SaveData
 
 open Lean Meta Elab Command
 
 set_option autoImplicit false
 
-/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
-register_option lean4game.showDependencyReasons : Bool := {
-  defValue := false
-  descr := "show reasons for calculated world dependencies."
-}
-
-/-- Let `MakeGame` print the reasons why the worlds depend on each other.
-
-Note: currently unused in favour of setting `set_option trace.debug true`. -/
-register_option lean4game.verbose : Bool := {
-  defValue := false
-  descr := "display more info messages to help developing the game."
-}
-
 /-! # Game metadata -/
 
 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -46,147 +35,101 @@ 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
+  let intro := t.getString
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
-  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
+  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
+  | .Game => modifyCurGame  fun game => pure {game with introduction := intro}
 
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
+  let info:= t.getString
   match ← getCurLayer with
-  | .Level => pure ()
-  | .World => pure ()
-  | .Game => modifyCurGame  fun game => pure {game with info := t.getString}
+  | .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 := info}
 
+/-- 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. -/
 elab "Conclusion" t:str : command => do
+  let conclusion := t.getString
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
-  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
+  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
+  | .Game => modifyCurGame  fun game => pure {game with conclusion := conclusion}
 
+/-- 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
+  let caption := t.getString
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with short := caption}}
+
+/-- More detailed description what the game is about (2-4 sentences). -/
+elab "CaptionLong" t:str : command => do
+  let caption := t.getString
+  modifyCurGame fun game => pure {game with
+    tile := {game.tile with long := caption}}
+
+/-- 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
 
-The inventory contains docs for tactics, lemmas, and definitions. These are all locked
+The inventory contains docs for tactics, theorems, and definitions. These are all locked
 in the first level and get enabled during the game.
 -/
 
 /-! ## Doc entries -/
 
-/-- Copied from `Mathlib.Tactic.HelpCmd`.
-
-Gets the initial string token in a parser description. For example, for a declaration like
-`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
-that don't start with a string constant. -/
-partial def getHeadTk (e : Expr) : Option String :=
-  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
-  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
-  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
-  | _ => none
-
-/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
-def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
-  let name := name.toString (escape := false)
-  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
-
-  let catName : Name := `tactic
-  let catStx : Ident := mkIdent catName -- TODO
-  let some cat := (Parser.parserExtension.getState env).categories.find? catName
-    | throwErrorAt catStx "{catStx} is not a syntax category"
-  liftTermElabM <| Term.addCategoryInfo catStx catName
-  for (k, _) in cat.kinds do
-    let mut used := false
-    if let some tk := do getHeadTk (← (← env.find? k).value?) then
-      let tk := tk.trim
-      if name ≠ tk then -- was `!name.isPrefixOf tk`
-        continue
-      used := true
-      decls := decls.insert tk ((decls.findD tk #[]).push k)
-  for (_name, ks) in decls do
-    for k in ks do
-      if let some doc ← findDocString? env k then
-        return doc
-
-  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
-    m!"using `TacticDoc {name} \"some doc\"`"
-  return none
-
-/-- Retrieve the docstring associated to an inventory item. For Tactics, this
-is not guaranteed to work. -/
-def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
-    CommandElabM (Option String) :=
-  match type with
-  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
-  | .Tactic => getTacticDocstring env name
-  | .Lemma => findDocString? env name
-  -- TODO: for definitions not implemented yet, does it work?
-  | .Definition => findDocString? env name
-
-/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
-a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
-warning.
-
-`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
-I used this workaround, because I needed a new name (with correct namespace etc)
-to be used, and I don't know how to create a new ident with same position but different name.
--/
-def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
-    (template : Option String := none) : CommandElabM Unit := do
-  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
-  let env ← getEnv
-  let n := name
-  -- Find a key with matching `(type, name)`.
-  match (inventoryTemplateExt.getState env).findIdx?
-    (fun x => x.name == n && x.type == type) with
-  -- Nothing to do if the entry exists
-  | some _ => pure ()
-  | none =>
-    match template with
-    -- Warn about missing documentation
-    | none =>
-      let docstring ← match (← getDocstring env name type) with
-      | some ds =>
-        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
-        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
-        pure s!"*(lean docstring)*\\\n{ds}"
-      | none =>
-        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
-        m!"somewhere above this statement.")
-        pure "(missing)"
-
-      -- We just add a dummy entry
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := docstring})
-    -- Add the default documentation
-    | some s =>
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := s })
-      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
-        m!"docstring) instead. If you want to write a different description, add " ++
-        m!"`{type}Doc {name}` somewhere above this statement.")
-
 /-- Documentation entry of a tactic. Example:
 
 ```
@@ -196,37 +139,40 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The identifier is the tactics name. Some need to be escaped like `«have»`.
 * The description is a string supporting Markdown.
  -/
-elab "TacticDoc" name:ident content:str : command =>
+elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
+  let doc ← parseDocCommentLegacy doc content
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
     displayName := name.getId.toString
-    content := content.getString })
+    content := doc })
 
-/-- Documentation entry of a lemma. Example:
+/-- Documentation entry of a theorem. Example:
 
 ```
-LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
+TheoremDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 ```
 
-* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
-  It is preferably the true name of the lemma. However, this is not required.
+* The first identifier is used in the commands `[New/Only/Disabled]Theorem`.
+  It is preferably the true name of the theorem. However, this is not required.
 * The string following `as` is the displayed name (in the Inventory).
-* The identifier after `in` is the category to group lemmas by (in the Inventory).
+* The identifier after `in` is the category to group theorems by (in the Inventory).
 * The description is a string supporting Markdown.
 
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The lemma/definition to have the same fully qualified name as in mathlib.
+The theorem/definition to have the same fully qualified name as in mathlib.
  -/
-elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
+elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
+    command => do
+  let doc ← parseDocCommentLegacy doc content
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
     category := category.getString
     displayName := displayName.getString
-    content := content.getString })
+    content := doc })
 -- TODO: Catch the following behaviour.
--- 1. if `LemmaDoc` appears in the same file as `Statement`, it will silently use
+-- 1. if `TheoremDoc` appears in the same file as `Statement`, it will silently use
 -- it but display the info that it wasn't found in `Statement`
 -- 2. if it appears in a later file, however, it will silently not do anything and keep
 -- the first one.
@@ -244,37 +190,25 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The description is a string supporting Markdown.
 
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The lemma/definition to have the same fully qualified name as in mathlib.
+The theorem/definition to have the same fully qualified name as in mathlib.
  -/
-elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
+elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
+  let doc ← parseDocCommentLegacy doc template
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
     displayName := displayName.getString,
-    content := template.getString })
+    content := doc })
 
 /-! ## Add inventory items -/
 
-def getStatement (name : Name) : CommandElabM MessageData := do
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
-    | none     => return "that's a bug." })
-
--- Note: We use `String` because we can't send `MessageData` as json, but
--- `MessageData` might be better for interactive highlighting.
-/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
-
-Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
-`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
-def getStatementString (name : Name) : CommandElabM String := do
-  try
-    return ← (← getStatement name).toString
-  catch
-  | _ => throwError m!"Could not find {name} in context."
-  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
+def checkCommandNotDuplicated (items : Array Name) (cmd := "Command") : CommandElabM Unit := do
+  if ¬ items.isEmpty then
+    logWarning s!"You should only use one `{cmd}` per level, but it takes multiple arguments: `{cmd} obj₁ obj₂ obj₃`!"
 
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.new) "NewTactic"
   for name in ↑args do
     checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
   modifyCurLevel fun level => pure {level with
@@ -282,14 +216,16 @@ elab "NewTactic" args:ident* : command => do
 
 /-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic"
   for name in ↑args do
     checkInventoryDoc .Tactic name (template := "")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId),
                                    hidden := level.tactics.hidden ++ args.map (·.getId)}}
 
-/-- Declare lemmas that are introduced by this level. -/
-elab "NewLemma" args:ident* : command => do
+/-- Declare theorems that are introduced by this level. -/
+elab "NewTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewTheorem"
   for name in ↑args do
     try let _decl ← getConstInfo name.getId catch
       | _ => logErrorAt name m!"unknown identifier '{name}'."
@@ -299,6 +235,7 @@ elab "NewLemma" args:ident* : command => do
 
 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.new) "NewDefinition"
   for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]")
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with new := args.map (·.getId)}}
@@ -306,31 +243,36 @@ elab "NewDefinition" args:ident* : command => do
 /-- Declare tactics that are temporarily disabled in this level.
 This is ignored if `OnlyTactic` is set. -/
 elab "DisabledTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.disabled) "DisabledTactic"
   for name in ↑args do checkInventoryDoc .Tactic name
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with disabled := args.map (·.getId)}}
 
-/-- Declare lemmas that are temporarily disabled in this level.
-This is ignored if `OnlyLemma` is set. -/
-elab "DisabledLemma" args:ident* : command => do
+/-- Declare theorems that are temporarily disabled in this level.
+This is ignored if `OnlyTheorem` is set. -/
+elab "DisabledTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledTheorem"
   for name in ↑args  do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with disabled := args.map (·.getId)}}
 
 /-- Declare definitions that are temporarily disabled in this level -/
 elab "DisabledDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.disabled) "DisabledDefinition"
   for name in ↑args do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with disabled := args.map (·.getId)}}
 
 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.only) "OnlyTactic"
   for name in ↑args do checkInventoryDoc .Tactic name
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with only := args.map (·.getId)}}
 
-/-- Temporarily disable all lemmas except the ones declared here -/
-elab "OnlyLemma" args:ident* : command => do
+/-- Temporarily disable all theorems except the ones declared here -/
+elab "OnlyTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyTheorem"
   for name in ↑args do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with only := args.map (·.getId)}}
@@ -338,65 +280,66 @@ elab "OnlyLemma" args:ident* : command => do
 /-- Temporarily disable all definitions except the ones declared here.
 This is ignored if `OnlyDefinition` is set. -/
 elab "OnlyDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.only) "OnlyDefinition"
   for name in ↑args do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with only := args.map (·.getId)}}
 
-/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
+/-- Define which tab of Lemmas is opened by default. Usage: `TheoremTab "Nat"`.
 If omitted, the current tab will remain open. -/
-elab "LemmaTab"  category:str : command =>
+elab "TheoremTab"  category:str : command =>
+  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
+
+
+/-! DEPRECATED -/
+
+elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
+    command => do
+  logWarning "Deprecated. Has been renamed to `TheoremDoc`"
+  let doc ← parseDocCommentLegacy doc content
+  modifyEnv (inventoryTemplateExt.addEntry · {
+    type := .Lemma
+    name := name.getId
+    category := category.getString
+    displayName := displayName.getString
+    content := doc })
+
+elab "NewLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `NewTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewLemma"
+  for name in ↑args do
+    try let _decl ← getConstInfo name.getId catch
+      | _ => logErrorAt name m!"unknown identifier '{name}'."
+    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with new := args.map (·.getId)}}
+
+elab "DisabledLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `DisabledTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledLemma"
+  for name in ↑args  do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with disabled := args.map (·.getId)}}
+
+elab "OnlyLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `OnlyTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyLemma"
+  for name in ↑args do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with only := args.map (·.getId)}}
+
+elab "LemmaTab"  category:str : command => do
+  logWarning "Deprecated. Has been renamed to `TheoremTab`"
   modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
 
 /-! # Exercise Statement -/
 
-/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
-syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
--- TODO
-
--- TODO: Reuse the following code for checking available tactics in user code:
-structure UsedInventory where
-(tactics : HashSet Name := {})
-(definitions : HashSet Name := {})
-(lemmas : HashSet Name := {})
-
-partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
-  match stx with
-  | .missing => return acc
-  | .node _info kind args =>
-    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
-    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
-  | .atom _info val =>
-    -- ignore syntax elements that do not start with a letter
-    -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
-    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
-      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      return {acc with tactics := acc.tactics.insert val}
-    else
-      return acc
-  | .ident _info _rawVal val _preresolved =>
-      let ns ←
-        try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
-      return ← ns.foldlM (fun acc n => do
-        if let some (.thmInfo ..) := (← getEnv).find? n then
-          return {acc with lemmas := acc.lemmas.insertMany ns}
-        else
-          return {acc with definitions := acc.definitions.insertMany ns}
-      ) acc
-
--- #check expandOptDocComment?
-
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
     "Statement" statementName:ident ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
-  let docContent : Option String := match doc with
-  | none => none
-  | some s => match s.raw[1] with
-    | .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
-    | _           => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
+  let docContent ← parseDocComment doc
 
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -497,23 +440,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 
 /-! # Hints -/
 
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/
@@ -626,6 +552,7 @@ elab "Template" tacs:tacticSeq : tactic => do
   modifyLevel (←getCurLevelId) fun level => do
     return {level with template := s!"{template}"}
 
+
 -- TODO: Notes for testing if a declaration has the simp attribute
 
 -- -- Test: From zulip
@@ -644,98 +571,6 @@ elab "Template" tacs:tacticSeq : tactic => do
 
 /-! # Make Game -/
 
-def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
-| .Tactic => level.tactics
-| .Definition => level.definitions
-| .Lemma => level.lemmas
-
-def GameLevel.setComputedInventory (level : GameLevel) :
-    InventoryType → Array InventoryTile → GameLevel
-| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
-| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
-| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
-
-partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
-      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
-    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
-  match (newArrows.find? id, decendants.find? id) with
-  | (some _, some _) => return (newArrows, decendants)
-  | _ =>
-    let mut newArr := newArrows
-    let mut desc := decendants
-    desc := desc.insert id {} -- mark as worked in case of loops
-    newArr := newArr.insert id {} -- mark as worked in case of loops
-    let children := arrows.findD id {}
-    let mut trimmedChildren := children
-    let mut theseDescs := children
-    for child in children do
-      (newArr, desc) := removeTransitiveAux child arrows newArr desc
-      let childDescs := desc.findD child {}
-      theseDescs := theseDescs.insertMany childDescs
-      for d in childDescs do
-        trimmedChildren := trimmedChildren.erase d
-    desc := desc.insert id theseDescs
-    newArr := newArr.insert id trimmedChildren
-    return (newArr, desc)
-
-def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
-  let mut newArr := {}
-  let mut desc := {}
-  for id in arrows.toArray.map Prod.fst do
-    (newArr, desc) := removeTransitiveAux id arrows newArr desc
-    if (desc.findD id {}).contains id then
-      logError <| m!"Loop at {id}. " ++
-        m!"This should not happen and probably means that `findLoops` has a bug."
-      -- DEBUG:
-      -- for ⟨x, hx⟩ in desc.toList do
-      --   m := m ++ m!"{x}: {hx.toList}\n"
-      -- logError m
-
-  return newArr
-
-/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
-
-For performance reason it returns a HashSet of visited
-nodes as well. This is filled with all nodes ever looked at as they cannot be
-part of a loop anymore. -/
-partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
-    (path : Array Name := #[]) (visited : HashSet Name := {}) :
-    Array Name × HashSet Name := Id.run do
-  let mut visited := visited
-  match path.getIdx? node with
-  | some i =>
-    -- Found a loop: `node` is already the iᵗʰ element of the path
-    return (path.extract i path.size, visited.insert node)
-  | none =>
-    for successor in arrows.findD node {} do
-      -- If we already visited the successor, it cannot be part of a loop anymore
-      if visited.contains successor then
-        continue
-      -- Find any loop involving `successor`
-      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
-      visited := visited.insert successor
-      -- No loop found in the dependants of `successor`
-      if loop.isEmpty then
-        continue
-      -- Found a loop, return it
-      return (loop, visited)
-  return (#[], visited.insert node)
-
-/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
-partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
-  let mut visited : HashSet Name := {}
-  for node in arrows.toArray.map (·.1) do
-    -- Skip a node if it was already visited
-    if visited.contains node then
-      continue
-    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
-    -- search starting from `node`
-    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
-    visited := moreVisited
-    if !loop.isEmpty then
-      return loop.toList
-  return []
-
 /-- The worlds of a game are joint by dependencies. These are
 automatically computed but can also be defined with the syntax
 `Dependency World₁ → World₂ → World₃`. -/
@@ -810,8 +645,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 +689,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 +706,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 +757,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
 
@@ -984,6 +837,7 @@ elab "MakeGame" : command => do
               name := item
               displayName := data.displayName
               category := data.category
+              altTitle := data.statement
               hidden := hiddenItems.contains item })
 
 
@@ -1003,6 +857,7 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
+            altTitle := data.statement
             hidden := hiddenItems.contains item }
       itemsInWorld := itemsInWorld.insert worldId items
 
@@ -1022,7 +877,8 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
-            hidden := levelInfo.hidden.contains item }
+            altTitle := data.statement
+            hidden := hiddenItems.contains item }
 
         -- add the exercise statement from the previous level
         -- if it was named
@@ -1035,6 +891,7 @@ elab "MakeGame" : command => do
               name := name
               displayName := data.displayName
               category := data.category
+              altTitle := data.statement
               locked := false }
 
         -- add marks for `disabled` and `new` lemmas here, so that they only apply to
@@ -1052,17 +909,18 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
+    allItemsByType := allItemsByType.insert inventoryType allItems
 
-/-! # Debugging tools -/
+  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).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    lemmaTab := none
+  }
 
--- /-- Print current game for debugging purposes. -/
--- elab "PrintCurGame" : command => do
---   logInfo (toJson (← getCurGame))
-
-/-- Print current level for debugging purposes. -/
-elab "PrintCurLevel" : command => do
-  logInfo (repr (← getCurLevel))
-
-/-- Print levels for debugging purposes. -/
-elab "PrintLevels" : command => do
-  logInfo $ repr $ (← getCurWorld).levels.toArray
+  saveGameData allItemsByType inventory

server/GameServer/EnvExtensions.lean

@@ -106,8 +106,16 @@ structure InventoryTile where
   new := false
   /-- hide the item in the inventory display -/
   hidden := false
+  /-- hover text -/
+  altTitle : String := default
 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 +143,18 @@ 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
 
+-- TODO: Reuse the following code for checking available tactics in user code:
+structure UsedInventory where
+(tactics : HashSet Name := {})
+(definitions : HashSet Name := {})
+(lemmas : HashSet Name := {})
 
 /-! ## Environment extensions for game specification -/
 
@@ -254,8 +273,63 @@ structure GameLevel where
   lemmas: InventoryInfo := default
   /-- A proof template that is printed in an empty editor. -/
   template: Option String := none
-  deriving Inhabited, Repr
+  /-- The image for this level. -/
+  image : String := default
+deriving Inhabited, Repr
 
+/-- Json-encodable version of `GameLevel`
+Fields:
+- 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
+  module : Name
+  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
+    module := lvl.module
+    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 +345,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, FromJson
+
 structure Game where
   /-- Internal name of the game. -/
   name : Name
@@ -296,7 +399,18 @@ structure Game where
   /-- TODO: currently unused. -/
   authors : List String := default
   worlds : Graph Name World := default
-deriving Inhabited, ToJson
+  /-- 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, FromJson
+
+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 -/
 

server/GameServer/FileWorker.lean

@@ -1,6 +1,8 @@
-/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
+/- This file is adapted from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
+import GameServer.ImportModules
+import GameServer.SaveData
 
 namespace MyModule
 open Lean
@@ -16,7 +18,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
   mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
-  (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
+  (mps : ModuleParserState) (messages : MessageLog) :
     Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
   let mut pos := mps.pos
   let mut recovering := mps.recovering
@@ -55,6 +57,20 @@ open IO
 open Snapshots
 open JsonRpc
 
+structure GameWorkerState :=
+  inventory : Array String
+  /--
+  Check for tactics/theorems that are not unlocked.
+  0: no check
+  1: give warnings
+  2: give errors
+  -/
+  difficulty : Nat
+  levelInfo : LevelInfo
+  deriving ToJson, FromJson
+
+abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+
 section Elab
 
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
@@ -72,29 +88,30 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
 partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
+    (gameWorkerState : GameWorkerState) (stx : Syntax) :
     Elab.Command.CommandElabM Unit := do
+  let levelInfo := gameWorkerState.levelInfo
   match stx with
   | .missing => return ()
   | .node _info _kind args =>
     for arg in args do
-      findForbiddenTactics inputCtx levelParams arg
+      findForbiddenTactics inputCtx gameWorkerState arg
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore "with" keyword
     let allowed := ["with", "fun", "at", "only", "by", "to"]
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelParams.tactics.find? (·.name.toString == val) with
+      match levelInfo.tactics.find? (·.name.toString == val) with
       | none =>
         -- Note: This case means that the tactic will never be introduced in the game.
-        match levelParams.inventory.find? (· == val) with
+        match gameWorkerState.inventory.find? (· == val) with
         | none =>
           addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
         | some _ => pure () -- tactic is in the inventory, allow it.
       | some tac =>
         if tac.locked then
-          match levelParams.inventory.find? (· == val) with
+          match gameWorkerState.inventory.find? (· == val) with
           | none =>
             addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
           | some _ => pure () -- tactic is in the inventory, allow it.
@@ -108,10 +125,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
         let some (.thmInfo ..) := (← getEnv).find? n
           | return () -- not a theorem -> ignore
         -- Forbid the theorem we are proving currently
-        if n = levelParams.statementName then
+        if some n = levelInfo.statementName then
           addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
 
-        let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
+        let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
         match lemmasAndDefs.find? (fun l => l.name == n) with
         | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
         | some lem =>
@@ -120,7 +137,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           else if lem.disabled then
             addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
 where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := levelParams.difficulty
+  let difficulty := gameWorkerState.difficulty
   if difficulty > 0 then
     modify fun st => { st with
       messages := st.messages.add {
@@ -136,7 +153,7 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
+    (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState)
     (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -167,7 +184,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     Elab.Command.catchExceptions
       (getResetInfoTrees *> do
         let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
-          | throwError "Level not found: {inputCtx.fileName}"
+          | panic! s!"Level not found: {inputCtx.fileName} / {GameServer.levelIdFromFileName? initParams inputCtx.fileName}"
         let scope := level.scope
 
         -- use open namespaces and options as in the level file
@@ -185,12 +202,12 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
             currNamespace := scope.currNamespace,
             openDecls := scope.openDecls }
           let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
-            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
+            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog
           modify (fun s => { s with messages := msgLog })
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          findForbiddenTactics inputCtx levelParams tacticStx
+          findForbiddenTactics inputCtx gameWorkerState tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
@@ -218,6 +235,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     }
 
   let (tacticStx, cmdParserState) ← parseResultRef.get
+  if tacticStx.isMissing then throwServerError "Tactic execution went wrong. No stx found."
 
   let postCmdSnap : Snapshot := {
     beginPos := tacticStx.getPos?.getD 0
@@ -269,7 +287,7 @@ where
 
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
+      (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams)
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
@@ -287,7 +305,7 @@ where
     -- we can see the current goal even on an empty document
     let couldBeEndSnap := s.snaps.size > 1
     let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
-      levelParams initParams
+      gameWorkerState initParams
     set { s with snaps := s.snaps.push snap }
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
@@ -309,7 +327,7 @@ where
 
   /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
   def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
+      (startAfterMs : UInt32) (gameWorkerState : GameWorkerState)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -325,21 +343,15 @@ where
       publishIleanInfoUpdate m ctx.hOut snaps
       return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
         IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
-structure GameWorkerState :=
-(levelParams : Game.DidOpenLevelParams)
-
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
-
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
   def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
     let s ← get
-    let levelParams := s.levelParams
     let ctx ← read
     let oldDoc := (← StateT.lift get).doc
     oldDoc.cancelTk.set
@@ -381,7 +393,7 @@ section Updates
           validSnaps := validSnaps.dropLast
       -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
       -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-      unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
+      unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
         (startAfterMs := ctx.initParams.editDelay.toUInt32)
     StateT.lift <| modify fun st => { st with
       doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -396,24 +408,23 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+      (gameDir : String) (module : Name):
       IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
     let out ← IO.Process.output
-      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+      { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
     if out.exitCode != 0 then
       throwServerError s!"Error while running Lake: {out.stderr}"
 
     -- Make the paths relative to the current directory
     let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
     let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
+    let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
 
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
-    -- return (env, paths)
+    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
 
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
@@ -457,10 +468,11 @@ section Initialization
       return (headerSnap, srcSearchPath)
 
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-       (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
+      (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams initParams
+      gameDir gameWorkerState.levelInfo.module
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -471,12 +483,14 @@ section Initialization
         clientHasWidgets
       }
     let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
+      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
       | Except.error e   => throw (e : ElabTaskError))
     let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
     return (ctx,
     { doc             := doc
       initHeaderStx   := headerStx
+      currHeaderStx      := headerStx
+      importCachingTask? := none
       pendingRequests := RBMap.empty
       rpcSessions     := RBMap.empty
     })
@@ -508,6 +522,7 @@ section MessageHandling
     match method with
     | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
     | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+    | "$/setTrace"        => pure ()
     | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
     | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
     | _                        => throwServerError s!"Got unsupported notification method: {method}"
@@ -546,26 +561,32 @@ section MainLoop
       let doc := st.doc
       doc.cancelTk.set
       return ()
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams Game.SetInventoryParams (toJson params))
-      let s ← get
-
-      set {s with levelParams := {s.levelParams with
-        inventory := p.inventory,
-        difficulty := p.difficulty}}
+    | Message.request id "shutdown" none =>
+      ctx.hOut.writeLspResponse ⟨id, Json.null⟩
       mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
       mainLoop
-    | _ => throwServerError "Got invalid JSON-RPC message"
+    | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
 end MainLoop
 
-def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
+def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  let initParams ← i.readLspRequestAs "initialize" InitializeParams
+  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
+  o.writeLspResponse {
+    id     := initRequest.id
+    result := {
+      capabilities := Watchdog.mkLeanServerCapabilities
+      serverInfo?  := some {
+        name     := "Lean 4 Game Server"
+        version? := "0.1.1"
+      }
+      : InitializeResult
+    }
+  }
+  discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
-  let ⟨_, levelParams⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams
 
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
@@ -577,9 +598,24 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
+    let game ← loadGameData gameDir
+    -- TODO: We misuse the `rootUri` field to the gameName
+    let rootUri? : Option String := some (toString game.name)
+    let initParams := {initRequest.param.toLeanInternal with rootUri?}
+    let some (levelId : LevelId) := GameServer.levelIdFromFileName?
+        initParams meta.mkInputContext.fileName
+      | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
+    let levelInfo ← loadLevelData gameDir levelId.world levelId.level
+    let some initializationOptions := initRequest.param.initializationOptions?
+      | throwServerError "no initialization options found"
+    let gameWorkerState : GameWorkerState:= {
+      inventory := initializationOptions.inventory
+      difficulty := initializationOptions.difficulty
+      levelInfo
+    }
+    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
+      StateT.run (s := gameWorkerState) <| (mainLoop)
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -589,12 +625,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
       message := e.toString }] o
     return (1 : UInt32)
 
-def workerMain (opts : Options) : IO UInt32 := do
+def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    let exitCode ← initAndRunWorker i o e opts
+    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
+    let exitCode ← initAndRunWorker i o e opts gameDir
     -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
     -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
     o.flush

server/GameServer/Game.lean

@@ -25,227 +25,56 @@ 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
+/- Game-specific version of `InitializeParams` that allows for extra options: -/
 
-/--
-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
+structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
+  difficulty : Nat
+  inventory : Array String
   deriving ToJson, FromJson
 
--- structure LoadTemplateParams where
---   world : Name
---   level : Nat
---   deriving ToJson, FromJson
+structure InitializeParams where
+  processId? : Option Int := none
+  clientInfo? : Option ClientInfo := none
+  /- We don't support the deprecated rootPath
+  (rootPath? : Option String) -/
+  rootUri? : Option String := none
+  initializationOptions? : Option InitializationOptions := none
+  capabilities : ClientCapabilities
+  /-- If omitted, we default to off. -/
+  trace : Trace := Trace.off
+  workspaceFolders? : Option (Array WorkspaceFolder) := none
+  deriving ToJson
 
-structure DidOpenLevelParams where
-  uri : String
-  gameDir : String
-  levelModule : Name
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  inventory : Array String
-  /--
-  Check for tactics/theorems that are not unlocked.
-  0: no check
-  1: give warnings
-  2: give errors
-  -/
-  difficulty : Nat
-  /-- The name of the theorem to be proven in this level. -/
-  statementName : Name
-  deriving ToJson, FromJson
+instance : FromJson InitializeParams where
+  fromJson? j := do
+    let processId? := j.getObjValAs? Int "processId"
+    let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"
+    let rootUri? := j.getObjValAs? String "rootUri"
+    let initializationOptions? := j.getObjValAs? InitializationOptions "initializationOptions"
+    let capabilities ← j.getObjValAs? ClientCapabilities "capabilities"
+    let trace := (j.getObjValAs? Trace "trace").toOption.getD Trace.off
+    let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
+    return ⟨
+      processId?.toOption,
+      clientInfo?.toOption,
+      rootUri?.toOption,
+      initializationOptions?.toOption,
+      capabilities,
+      trace,
+      workspaceFolders?.toOption⟩
 
-structure LoadDocParams where
-  name : Name
-  type : InventoryType
-deriving ToJson, FromJson
-
-structure SetInventoryParams where
-  inventory : Array String
-  difficulty : Nat
-deriving ToJson, FromJson
-
-def handleDidOpenLevel (params : Json) : GameServerM Unit := do
-  let p ← parseParams _ params
-  let m := p.textDocument
-  -- Execute the regular handling of the `didOpen` event
-  handleDidOpen p
-  let fw ← findFileWorker! m.uri
-  -- let s ← get
-  let c ← read
-  let some lvl ← GameServer.getLevelByFileName? c.initParams ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
-    | do
-      c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}"
-      c.hLog.flush
-  -- Send an extra notification to the file worker to inform it about the level data
-  let s ← get
-  fw.stdin.writeLspNotification {
-    method := "$/game/didOpenLevel"
-    param  := {
-      uri := m.uri
-      gameDir := s.gameDir
-      levelModule := lvl.module
-      tactics := lvl.tactics.tiles
-      lemmas := lvl.lemmas.tiles
-      definitions := lvl.definitions.tiles
-      inventory := s.inventory
-      difficulty := s.difficulty
-      statementName := lvl.statementName
-      : DidOpenLevelParams
-    }
+def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.InitializeParams :=
+{
+  processId? := p.processId?
+  clientInfo? := p.clientInfo?
+  rootUri? := p.rootUri?
+  initializationOptions? := p.initializationOptions?.map fun o => {
+    editDelay? := o.editDelay?
+    hasWidgets? := o.hasWidgets?
   }
-
-
-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
-      set {s with inventory := p.inventory, difficulty := p.difficulty}
-      let st ← read
-      let workers ← st.fileWorkersRef.get
-      for (_, fw) in workers do
-        fw.stdin.writeLspMessage msg
-
-      return true
-    | Message.request id "loadInventoryOverview" _ =>
-      let s ← get
-      let some game ← getGame? s.game
-        | return false
-      -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
-      -- and reset `new`, `disabled` and `unlocked`.
-      -- Note: as we allow worlds without any levels (for developing), we might need
-      -- to try until we find the first world with levels.
-      for ⟨worldId, _⟩ in game.worlds.nodes.toList do
-        let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
-          | do continue
-        let inventory : InventoryOverview := {
-          tactics := lvl.tactics.tiles.map
-            ({ · with locked := true, disabled := false, new := false }),
-          lemmas := lvl.lemmas.tiles.map
-            ({ · with locked := true, disabled := false, new := false }),
-          definitions := lvl.definitions.tiles.map
-            ({ · with locked := true, disabled := false, new := false }),
-          lemmaTab := none
-        }
-        let c ← read
-        c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
-        return true
-      return false
-    | _ => return false
-  | _ => return false
+  capabilities := p.capabilities
+  trace := p.trace
+  workspaceFolders? := p.workspaceFolders?
+}
 
 end Game

server/GameServer/Graph.lean

@@ -18,6 +18,14 @@ instance [ToJson β] : ToJson (Graph Name β) := {
   ]
 }
 
+-- Just a dummy implementation for now:
+instance : FromJson (Graph Name β) := {
+  fromJson? := fun _ => .ok {
+    nodes := {}
+    edges := {}
+  }
+}
+
 instance  : EmptyCollection (Graph α β) := ⟨default⟩
 
 def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=

server/GameServer/Helpers.lean

@@ -0,0 +1,190 @@
+import Lean
+
+/-! This document contains various things which cluttered `Commands.lean`. -/
+
+open Lean Meta Elab Command
+
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
+/-! ## Doc Comment Parsing -/
+
+/-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
+def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
+    CommandElabM String := do
+  match doc with
+  | none =>
+    logWarning "Add a text to this command with `/-- yada yada -/ MyCommand`!"
+    pure ""
+  | some s => match s.raw[1] with
+    | .atom _ val => pure <| val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
+    | _           => pure "" --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
+
+/-- Read a doc comment and get its content. Return `none` if no doc comment available. -/
+def parseDocComment (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
+    CommandElabM <| Option String := do
+  match doc with
+  | none => pure none
+  | some _ => parseDocComment! doc
+
+
+/-- TODO: This is only used to provide some backwards compatibility and you can
+replace `parseDocCommentLegacy` with `parseDocComment` in the future. -/
+def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment))
+    (t : Option (TSyntax `str)) : CommandElabM <| String := do
+  match doc with
+  | none =>
+    match t with
+    | none =>
+      pure <| ← parseDocComment! doc
+    | some t =>
+      logWarningAt t "You should use the new Syntax:
+
+      /-- yada yada -/
+      YourCommand
+
+      instead of
+
+      YourCommand \"yada yada\"
+      "
+      pure t.getString
+  | some _ =>
+    match t with
+      | none =>
+        pure <| ← parseDocComment! doc
+      | some t =>
+        logErrorAt t "You must not provide both, a docstring and a string following the command!
+        Only use
+
+        /-- yada yada -/
+        YourCommand
+
+        and remove the string following it!"
+        pure <| ← parseDocComment! doc
+
+/-! ## Statement string -/
+
+def getStatement (name : Name) : CommandElabM MessageData := do
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
+    | none     => return "that's a bug." })
+
+-- Note: We use `String` because we can't send `MessageData` as json, but
+-- `MessageData` might be better for interactive highlighting.
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
+
+Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
+`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
+def getStatementString (name : Name) : CommandElabM String := do
+  try
+    return ← (← getStatement name).toString
+  catch
+  | _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
+
+/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
+syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
+-- TODO
+
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""
+
+
+/-! ## Loops in Graph-like construct
+
+TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?
+-/
+
+partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
+      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
+    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
+  match (newArrows.find? id, decendants.find? id) with
+  | (some _, some _) => return (newArrows, decendants)
+  | _ =>
+    let mut newArr := newArrows
+    let mut desc := decendants
+    desc := desc.insert id {} -- mark as worked in case of loops
+    newArr := newArr.insert id {} -- mark as worked in case of loops
+    let children := arrows.findD id {}
+    let mut trimmedChildren := children
+    let mut theseDescs := children
+    for child in children do
+      (newArr, desc) := removeTransitiveAux child arrows newArr desc
+      let childDescs := desc.findD child {}
+      theseDescs := theseDescs.insertMany childDescs
+      for d in childDescs do
+        trimmedChildren := trimmedChildren.erase d
+    desc := desc.insert id theseDescs
+    newArr := newArr.insert id trimmedChildren
+    return (newArr, desc)
+
+
+def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
+  let mut newArr := {}
+  let mut desc := {}
+  for id in arrows.toArray.map Prod.fst do
+    (newArr, desc) := removeTransitiveAux id arrows newArr desc
+    if (desc.findD id {}).contains id then
+      logError <| m!"Loop at {id}. " ++
+        m!"This should not happen and probably means that `findLoops` has a bug."
+      -- DEBUG:
+      -- for ⟨x, hx⟩ in desc.toList do
+      --   m := m ++ m!"{x}: {hx.toList}\n"
+      -- logError m
+
+  return newArr
+
+/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
+
+For performance reason it returns a HashSet of visited
+nodes as well. This is filled with all nodes ever looked at as they cannot be
+part of a loop anymore. -/
+partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
+    (path : Array Name := #[]) (visited : HashSet Name := {}) :
+    Array Name × HashSet Name := Id.run do
+  let mut visited := visited
+  match path.getIdx? node with
+  | some i =>
+    -- Found a loop: `node` is already the iᵗʰ element of the path
+    return (path.extract i path.size, visited.insert node)
+  | none =>
+    for successor in arrows.findD node {} do
+      -- If we already visited the successor, it cannot be part of a loop anymore
+      if visited.contains successor then
+        continue
+      -- Find any loop involving `successor`
+      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
+      visited := visited.insert successor
+      -- No loop found in the dependants of `successor`
+      if loop.isEmpty then
+        continue
+      -- Found a loop, return it
+      return (loop, visited)
+  return (#[], visited.insert node)
+
+/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
+partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
+  let mut visited : HashSet Name := {}
+  for node in arrows.toArray.map (·.1) do
+    -- Skip a node if it was already visited
+    if visited.contains node then
+      continue
+    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
+    -- search starting from `node`
+    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
+    visited := moreVisited
+    if !loop.isEmpty then
+      return loop.toList
+  return []

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/Inventory.lean

@@ -0,0 +1,152 @@
+import Lean
+import GameServer.EnvExtensions
+
+open Lean Elab Command
+
+/-- Copied from `Mathlib.Tactic.HelpCmd`.
+
+Gets the initial string token in a parser description. For example, for a declaration like
+`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
+that don't start with a string constant. -/
+partial def getHeadTk (e : Expr) : Option String :=
+  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
+  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
+  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
+  | _ => none
+
+/-! ## Doc entries -/
+
+/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
+def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
+  let name := name.toString (escape := false)
+  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
+
+  let catName : Name := `tactic
+  let catStx : Ident := mkIdent catName -- TODO
+  let some cat := (Parser.parserExtension.getState env).categories.find? catName
+    | throwErrorAt catStx "{catStx} is not a syntax category"
+  liftTermElabM <| Term.addCategoryInfo catStx catName
+  for (k, _) in cat.kinds do
+    let mut used := false
+    if let some tk := do getHeadTk (← (← env.find? k).value?) then
+      let tk := tk.trim
+      if name ≠ tk then -- was `!name.isPrefixOf tk`
+        continue
+      used := true
+      decls := decls.insert tk ((decls.findD tk #[]).push k)
+  for (_name, ks) in decls do
+    for k in ks do
+      if let some doc ← findDocString? env k then
+        return doc
+
+  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
+    m!"using `TacticDoc {name} \"some doc\"`"
+  return none
+
+/-- Retrieve the docstring associated to an inventory item. For Tactics, this
+is not guaranteed to work. -/
+def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
+    CommandElabM (Option String) :=
+  match type with
+  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
+  | .Tactic => getTacticDocstring env name
+  | .Lemma => findDocString? env name
+  -- TODO: for definitions not implemented yet, does it work?
+  | .Definition => findDocString? env name
+
+/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
+a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
+warning.
+
+`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
+I used this workaround, because I needed a new name (with correct namespace etc)
+to be used, and I don't know how to create a new ident with same position but different name.
+-/
+def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
+    (template : Option String := none) : CommandElabM Unit := do
+  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
+  let env ← getEnv
+  let n := name
+  -- Find a key with matching `(type, name)`.
+  match (inventoryTemplateExt.getState env).findIdx?
+    (fun x => x.name == n && x.type == type) with
+  -- Nothing to do if the entry exists
+  | some _ => pure ()
+  | none =>
+    match template with
+    -- Warn about missing documentation
+    | none =>
+      let docstring ← match (← getDocstring env name type) with
+      | some ds =>
+        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
+        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
+        pure s!"*(lean docstring)*\\\n{ds}"
+      | none =>
+        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
+        m!"somewhere above this statement.")
+        pure "(missing)"
+
+      -- We just add a dummy entry
+      modifyEnv (inventoryTemplateExt.addEntry · {
+        type := type
+        name := name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := docstring})
+    -- Add the default documentation
+    | some s =>
+      modifyEnv (inventoryTemplateExt.addEntry · {
+        type := type
+        name := name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := s })
+      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
+        m!"docstring) instead. If you want to write a different description, add " ++
+        m!"`{type}Doc {name}` somewhere above this statement.")
+
+partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
+  match stx with
+  | .missing => return acc
+  | .node _info kind args =>
+    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
+    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
+  | .atom _info val =>
+    -- ignore syntax elements that do not start with a letter
+    -- and ignore some standard keywords
+    let allowed := ["with", "fun", "at", "only", "by"]
+    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
+      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
+      return {acc with tactics := acc.tactics.insert val}
+    else
+      return acc
+  | .ident _info _rawVal val _preresolved =>
+      let ns ←
+        try resolveGlobalConst (mkIdent val)
+        catch | _ => pure [] -- catch "unknown constant" error
+      return ← ns.foldlM (fun acc n => do
+        if let some (.thmInfo ..) := (← getEnv).find? n then
+          return {acc with lemmas := acc.lemmas.insertMany ns}
+        else
+          return {acc with definitions := acc.definitions.insertMany ns}
+      ) acc
+
+-- #check expandOptDocComment?
+
+def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
+| .Tactic => level.tactics
+| .Definition => level.definitions
+| .Lemma => level.lemmas
+
+def GameLevel.setComputedInventory (level : GameLevel) :
+    InventoryType → Array InventoryTile → GameLevel
+| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
+| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
+| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}

server/GameServer/Options.lean

@@ -0,0 +1,17 @@
+import Lean
+
+/-! This document contains custom options available in the game. -/
+
+/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
+register_option lean4game.showDependencyReasons : Bool := {
+  defValue := false
+  descr := "show reasons for calculated world dependencies."
+}
+
+/-- Let `MakeGame` print the reasons why the worlds depend on each other.
+
+Note: currently unused in favour of setting `set_option trace.debug true`. -/
+register_option lean4game.verbose : Bool := {
+  defValue := false
+  descr := "display more info messages to help developing the game."
+}

server/GameServer/RpcHandlers.lean

@@ -46,8 +46,8 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
   | .fvar i1, .fvar i2 => bij.insert? i1 i2
   | .mvar _, .mvar _ => bij
-  | .sort u1, .sort u2 => bij -- TODO?
-  | .const n1 ls1, .const n2 ls2 =>
+  | .sort _u1, .sort _u2 => bij -- TODO?
+  | .const n1 _ls1, .const n2 _ls2 =>
     if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
   | .app f1 a1, .app f2 a2 =>
     some bij
@@ -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/GameServer/SaveData.lean

@@ -0,0 +1,78 @@
+import GameServer.EnvExtensions
+
+open Lean Meta Elab Command
+
+
+/-! ## Copy images -/
+
+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
+
+namespace GameData
+  def gameDataPath : System.FilePath := ".lake" / "gamedata"
+  def gameFileName := s!"game.json"
+  def docFileName := fun (inventoryType : InventoryType) (name : Name) => s!"doc__{inventoryType}__{name}.json"
+  def levelFileName := fun (worldId : Name) (levelId : Nat) => s!"level__{worldId}__{levelId}.json"
+  def inventoryFileName := s!"inventory.json"
+end GameData
+
+open GameData in
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
+    (inventory : InventoryOverview): CommandElabM Unit := do
+  let game ← getCurGame
+  let env ← getEnv
+  let path := (← IO.currentDir) / gameDataPath
+
+  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 / levelFileName worldId levelId) (toString (toJson (level.toInfo env)))
+
+  IO.FS.writeFile (path / gameFileName) (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 / docFileName inventoryType name) (toString (toJson item))
+
+  IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
+
+open GameData
+
+def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
+  let str ← IO.FS.readFile f
+  let json ← match Json.parse str with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  let data ← match fromJson? json with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  return data
+
+def loadGameData (gameDir : System.FilePath) : IO Game :=
+  loadData (gameDir / gameDataPath / gameFileName) Game
+
+def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
+  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo

server/GameServer/Watchdog.lean

@@ -1,158 +0,0 @@
-/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
-import Lean.Server.Watchdog
-import GameServer.Game
-
-namespace MyServer.Watchdog
-open Lean
-open Server
-open Watchdog
-open IO
-open Lsp
-open JsonRpc
-open System.Uri
-
-  partial def mainLoop (clientTask : Task ServerEvent) : GameServerM Unit := do
-    let st ← read
-    let workers ← st.fileWorkersRef.get
-    let mut workerTasks := #[]
-    for (_, fw) in workers do
-      if let WorkerState.running := fw.state then
-        workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
-
-    let ev ← IO.waitAny (clientTask :: workerTasks.toList)
-
-    if ← Game.handleServerEvent ev then -- handle Game requests
-      mainLoop (←runClientTask)
-    else
-      match ev with
-      | ServerEvent.clientMsg msg =>
-        match msg with
-        | Message.request id "shutdown" _ =>
-          shutdown
-          st.hOut.writeLspResponse ⟨id, Json.null⟩
-        | Message.request id method (some params) =>
-          handleRequest id method (toJson params)
-          mainLoop (←runClientTask)
-        | Message.response .. =>
-          -- TODO: handle client responses
-          mainLoop (←runClientTask)
-        | Message.responseError _ _ e .. =>
-          throwServerError s!"Unhandled response error: {e}"
-        | Message.notification method (some params) =>
-          if method == "textDocument/didOpen" then
-            -- for lean4game, we need to pass in extra information when a level is opened:
-            Game.handleDidOpenLevel (← parseParams _ (toJson params))
-          else
-            handleNotification method (toJson params)
-          mainLoop (←runClientTask)
-        | _ => throwServerError "Got invalid JSON-RPC message"
-      | ServerEvent.clientError e => throw e
-      | ServerEvent.workerEvent fw ev =>
-        match ev with
-        | WorkerEvent.ioError e =>
-          throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
-        | WorkerEvent.crashed _ =>
-          handleCrash fw.doc.uri #[]
-          mainLoop clientTask
-        | WorkerEvent.terminated =>
-          throwServerError "Internal server error: got termination event for worker that should have been removed"
-        | .importsChanged =>
-          startFileWorker fw.doc
-          mainLoop clientTask
-
-def initAndRunWatchdogAux : GameServerM Unit := do
-  let st ← read
-  try
-    discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
-    let clientTask ← runClientTask
-    mainLoop clientTask
-  catch err =>
-    shutdown
-    throw err
-  /- NOTE(WN): It looks like instead of sending the `exit` notification,
-  VSCode just closes the stream. In that case, pretend we got an `exit`. -/
-  let Message.notification "exit" none ←
-    try st.hIn.readLspMessage
-    catch _ => pure (Message.notification "exit" none)
-    | throwServerError "Got `shutdown` request, expected an `exit` notification"
-
-def createEnv (gameDir : String) (module : String) : IO Environment := do
-  -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-  let out ← IO.Process.output
-    { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-  if out.exitCode != 0 then
-    throwServerError s!"Error while running Lake: {out.stderr}"
-
-  -- Make the paths relative to the current directory
-  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-  let currentDir ← IO.currentDir
-  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
-
-  -- Set the search path
-  Lean.searchPathRef.set paths
-
-  let env ← importModules #[{ module := `Init : Import }, { module := module : Import }] {} 0
-  return env
-
-def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
-  if args.length < 2 then
-    throwServerError s!"Expected 1-3 command line arguments in addition to `--server`:
-      game directory, the name of the main module (optional), and the name of the game (optional)."
-  let gameDir := args[1]!
-  let module := if args.length < 3 then defaultGameModule else args[2]!
-  let gameName := if args.length < 4 then defaultGameName else args[3]!
-  let workerPath := "./gameserver"
-  -- TODO: Do the following commands slow us down?
-  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
-  let references ← IO.mkRef (← loadReferences)
-  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
-  let i ← maybeTee "wdIn.txt" false i
-  let o ← maybeTee "wdOut.txt" true o
-  let e ← maybeTee "wdErr.txt" true e
-  let state := {
-    env := ← createEnv gameDir module,
-    game := gameName,
-    gameDir := gameDir,
-    inventory := #[]
-    difficulty := 0
-    }
-  let initRequest ← i.readLspRequestAs "initialize" InitializeParams
-  -- We misuse the `rootUri` field to the gameName
-  let rootUri? := gameName
-  let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
-  o.writeLspResponse {
-    id     := initRequest.id
-    result := {
-      capabilities := mkLeanServerCapabilities
-      serverInfo?  := some {
-        name     := "Lean 4 Game Server"
-        version? := "0.1.1"
-      }
-      : InitializeResult
-    }
-  }
-  let context : ServerContext := {
-    hIn            := i
-    hOut           := o
-    hLog           := e
-    args           := args
-    fileWorkersRef := fileWorkersRef
-    initParams     := initRequest.param
-    workerPath
-    srcSearchPath
-    references
-  }
-  discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
-
-def watchdogMain (args : List String) : IO UInt32 := do
-  let i ← IO.getStdin
-  let o ← IO.getStdout
-  let e ← IO.getStderr
-  try
-    initAndRunWatchdog args i o e
-    return 0
-  catch err =>
-    e.putStrLn s!"Watchdog error: {err}"
-    return 1
-
-end MyServer.Watchdog

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

server/lakefile.lean

@@ -3,10 +3,25 @@ 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]
 lean_exe gameserver {
-  root := `Main
+  root := `GameServer
   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.2.0
+leanprover/lean4:v4.4.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

@@ -5,6 +5,12 @@ 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({
@@ -22,6 +28,9 @@ export default defineConfig({
     })
   ],
   publicDir: "client/public",
+  optimizeDeps: {
+    exclude: ['games']
+  },
   server: {
     port: 3000,
     proxy: {
@@ -29,6 +38,12 @@ export default defineConfig({
         target: 'ws://localhost:8080',
         ws: true
       },
+      '/import': {
+        target: 'http://localhost:8080',
+      },
+      '/data': {
+        target: 'http://localhost:8080',
+      },
     }
   },
   resolve: {

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/]
-  };
-}