cleanup; including using doc comment syntax for documentation like TacticDoc

This reverts commit 6bced7575b.

.env

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

.github/workflows/build.yml

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

.gitignore

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

NOTES.md

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

README.md

@@ -1,33 +1,46 @@
 # Lean 4 Game
 
-This is a prototype for a Lean 4 game platform. The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
-(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-of Kevin Buzzard and Mohammad Pedramfar.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
+This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
-### Progress & Contributing
-Currently the interface is still undergoing bigger changes, contributions are of course welcome, but it might be better to wait with them for a bit until proper support for external games is implemented and the existing games are separated from this repository. (ca. Sept. 2023)
+## Creating a Game
 
+Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
 
-### Documentation
+* Step 5: [How to Run Games Locally](doc/running_locally.md)
+* Step 7: [How to Update an existing Game](doc/update_game.md)
+* Step 8: [How to Publishing a Game](doc/publish_game.md)
 
-For game developers, there is a work-in-progress Documentation: [Create a Game](DOCUMENTATION.md).
-Best to talk with us directly.
+## Documentation
 
-For the game engine itself, documentation is missing currently.
+The documentation is very much work in progress but the linked documentation here
+should be up-to-date:
 
-## NPM Scripts
+### Game creation API
 
-* `npm start`: Start the project in development mode. The browser will automatically reload when client files get changed. The Lean server will get recompiled and restarted when lean files get changed. The Lean server will be started without a container. The client and server can be started separately using the scripts `npm run start_client` and `npm run start_server`. The project can be accessed via `http://localhost:3000`.
-Internally, websocket requests to `ws://localhost:3000/websockets` will be forwarded to a Lean server running on port `8080`.
+- [Creating a Game](doc/create_game.md): **the main document to consult**.
+- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
 
-* `npm run build`: Build the project in production mode. All assets of the client will be compiled into `client/dist`.
-On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
+### Frontend API
 
-* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specifiv port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the docker-contained Lean server via the web socket protocol.
+* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
+* [How to Update an existing Game](doc/update_game.md): update to a new lean version
+* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
 
+### Backend
+
+not written yet
+
+## Contributing
+
+Contributions to `lean4game` are always welcome!
 
 ## Security
 
-Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server in a Docker container
-secured by [gVisor](https://gvisor.dev/).
+Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
+
+## Credits
+
+The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
+by Kevin Buzzard and Mohammad Pedramfar.
+The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

client/src/app.tsx

@@ -6,33 +6,28 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
-import './reset.css';
-import './app.css';
+import './css/reset.css';
+import './css/app.css';
 import { MobileContext } from './components/infoview/context';
 import { useWindowDimensions } from './window_width';
-import { selectOpenedIntro } from './state/progress';
-import { useSelector } from 'react-redux';
+import { connection } from './connection';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
-
-  // TODO: Make mobileLayout be changeable in settings
-  // TODO: Handle resize Events
   const {width, height} = useWindowDimensions()
   const [mobile, setMobile] = React.useState(width < 800)
 
-  // On mobile, there are multiple pages on the welcome page to switch between
-  const openedIntro = useSelector(selectOpenedIntro(gameId))
-  // On mobile, there are multiple pages to switch between
-  const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+  React.useEffect(() => {
+    connection.startLeanClient(gameId);
+  }, [gameId])
 
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile, pageNumber, setPageNumber}}>
+        <MobileContext.Provider value={{mobile, setMobile}}>
           <Outlet />
         </MobileContext.Provider>
       </GameIdContext.Provider>

client/src/components/app_bar.tsx

@@ -1,45 +1,45 @@
+/**
+ *  @file contains the navigation bars of the app.
+ */
 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'
 import { GameIdContext } from "../app"
 import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
 import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
-import { useSelector } from 'react-redux'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { Button } from './button'
-import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faDownload, faUpload, faEraser, faBook, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
-import { PrivacyPolicyPopup } from './privacy_policy'
-import { WorldSelectionMenu, downloadFile } from './world_tree'
+import { downloadProgress } from './popup/erase'
 
-/** navigation to switch between pages on mobile */
-function MobileNav({pageNumber, setPageNumber}:
+/** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
+function MobileNavButtons({pageNumber, setPageNumber}:
   { pageNumber: number,
     setPageNumber: any}) {
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
-  let prevText = {0 : null, 1: "Intro", 2: null}[pageNumber]
-  let prevIcon = {0 : null, 1: null, 2: faXmark}[pageNumber]
-  let prevTitle = {
-    0: null,
-    1: "Game Introduction",
-    2: "World selection"}[pageNumber]
-  let nextText = {0 : "Start", 1: null, 2: null}[pageNumber]
-  let nextIcon = {0 : null, 1: faBook, 2: null}[pageNumber]
-  let nextTitle = {
-    0: "World selection",
-    1: "Inventory",
-    2: null}[pageNumber]
+  // if `prevText` or `prevIcon` is set, show a button to go back
+  let prevText  = {0: null, 1: "Intro", 2: null}[pageNumber]
+  let prevIcon  = {0: null, 1: null, 2: faBookOpen}[pageNumber]
+  let prevTitle = {0: null, 1: "Game Introduction", 2: "World selection"}[pageNumber]
+  // if `nextText` or `nextIcon` is set, show a button to go forward
+  let nextText  = {0: "Start", 1: null, 2: null}[pageNumber]
+  let nextIcon  = {0: null, 1: faBook, 2: null}[pageNumber]
+  let nextTitle = {0: "World selection", 1: "Inventory", 2: null}[pageNumber]
 
   return <>
-    {(prevText || prevTitle || prevIcon) &&
-      <Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""} inverted="true" title={prevTitle}
+    {(prevText || prevIcon) &&
+      <Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""}
+          inverted="true" title={prevTitle}
           onClick={() => {pageNumber == 0 ? null : setPageNumber(pageNumber - 1)}}>
         {prevIcon && <FontAwesomeIcon icon={prevIcon} />}
         {prevText && `${prevText}`}
       </Button>
     }
-    {(nextText || nextTitle || nextIcon) &&
+    {(nextText || nextIcon) &&
       <Button className="btn btn-inverted toggle-width" to="" inverted="true"
           title={nextTitle} onClick={() => {
             console.log(`page number: ${pageNumber}`)
@@ -52,330 +52,20 @@ function MobileNav({pageNumber, setPageNumber}:
   </>
 }
 
-export function WelcomeAppBar({gameInfo, toggleImpressum, openEraseMenu, openUploadMenu, toggleInfo} : {
-  gameInfo: GameInfo,
-  toggleImpressum: any,
-  openEraseMenu: any,
-  openUploadMenu: any,
-  toggleInfo: any
-}) {
-  const gameId = React.useContext(GameIdContext)
-  const {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext)
-  const [navOpen, setNavOpen] = React.useState(false)
-
-
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const gameProgress = useSelector(selectProgress(gameId))
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-
-  return   <div className="app-bar" >
-    <>
-      <div>
-        <Button inverted="false" title="back to games selection" to="/">
-          <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
-        </Button>
-        <span className="app-bar-title"></span>
-      </div>
-      <div>
-        <span className="app-bar-title">
-          {mobile ? '' : gameInfo?.title}
-        </span>
-      </div>
-      <div className="nav-btns">
-        {mobile && <>
-          {/* BUTTONS for MOBILE */}
-          <MobileNav pageNumber={pageNumber} setPageNumber={setPageNumber} />
-
-        </>}
-
-        <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}} >
+/** button to toggle dropdown menu. */
+function MenuButton({navOpen, setNavOpen}) {
+  return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
     {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
   </Button>
-
-      </div>
-      <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
-        {/* {levelId < gameInfo.data?.worldSize[worldId] &&
-          <Button inverted="true"
-              to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
-              disabled={difficulty >= 2 && !(completed || levelId == 0)}
-              onClick={() => setNavOpen(false)}>
-            <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
-          </Button>
-        }
-        {levelId > 0 && <>
-              <Button disabled={levelId <= 0} inverted="true"
-                  to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-                  title="previous level"
-                  onClick={() => setNavOpen(false)}>
-                <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-              </Button>
-            </>}
-        <Button to={`/${gameId}`} inverted="true" title="back to world selection">
-          <FontAwesomeIcon icon={faHome} />&nbsp;Home
-        </Button>
-        <Button disabled={levelId <= 0} inverted="true" to=""
-            onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-            title="toggle Editor mode">
-          <FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
-        </Button> */}
-
-        <Button title="Game Info & Credits" inverted="true" to="" onClick={(ev) => {toggleInfo(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Game Info
-        </Button>
-        <Button title="Clear Progress" inverted="true" to="" onClick={(ev) => {openEraseMenu(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faEraser} />&nbsp;Erase
-        </Button>
-        <Button title="Download Progress" inverted="true" to="" onClick={(ev) => {downloadProgress(ev); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faDownload} />&nbsp;Download
-        </Button>
-        <Button title="Load Progress from JSON" inverted="true" to="" onClick={(ev) => {openUploadMenu(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faUpload} />&nbsp;Upload
-        </Button>
-        <Button title="Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
-        </Button>
-      </div>
-    </>
-  </div>
-
-
-
 }
 
-// /** The menu that is shown next to the world selection graph */
-// function WorldSelectionMenu() {
-//   const [file, setFile] = React.useState<File>();
-
-//   const gameId = React.useContext(GameIdContext)
-//   const store = useStore()
-//   const difficulty = useSelector(selectDifficulty(gameId))
-
-
-//   /* state variables to toggle the pop-up menus */
-//   const [eraseMenu, setEraseMenu] = React.useState(false);
-//   const openEraseMenu = () => setEraseMenu(true);
-//   const closeEraseMenu = () => setEraseMenu(false);
-//   const [uploadMenu, setUploadMenu] = React.useState(false);
-//   const openUploadMenu = () => setUploadMenu(true);
-//   const closeUploadMenu = () => setUploadMenu(false);
-
-//   const gameProgress = useSelector(selectProgress(gameId))
-//   const dispatch = useAppDispatch()
-
-//   /** Download the current progress (i.e. what's saved in the browser store) */
-//   const downloadProgress = (e) => {
-//     e.preventDefault()
-//     downloadFile({
-//       data: JSON.stringify(gameProgress, null, 2),
-//       fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-//       fileType: 'text/json',
-//     })
-//   }
-
-//   const handleFileChange = (e) => {
-//     if (e.target.files) {
-//       setFile(e.target.files[0])
-//     }
-//   }
-
-//   /** Upload progress from a  */
-//   const uploadProgress = (e) => {
-//     if (!file) {return}
-//     const fileReader = new FileReader()
-//     fileReader.readAsText(file, "UTF-8")
-//     fileReader.onload = (e) => {
-//       const data = JSON.parse(e.target.result.toString()) as GameProgressState
-//       console.debug("Json Data", data)
-//       dispatch(loadProgress({game: gameId, data: data}))
-//     }
-//     closeUploadMenu()
-//   }
-
-//   const eraseProgress = () => {
-//     dispatch(deleteProgress({game: gameId}))
-//     closeEraseMenu()
-//   }
-
-//   const downloadAndErase = (e) => {
-//     downloadProgress(e)
-//     eraseProgress()
-//   }
-
-//   function label(x : number) {
-//     return x == 0 ? 'none' : x == 1 ? 'lax' : 'regular'
-//   }
-
-//   return <nav className="world-selection-menu">
-//     <Button onClick={downloadProgress} title="Download game progress" to=""><FontAwesomeIcon icon={faDownload} /></Button>
-//     <Button title="Load game progress from JSON" onClick={openUploadMenu} to=""><FontAwesomeIcon icon={faUpload} /></Button>
-//     <Button title="Clear game progress" to="" onClick={openEraseMenu}><FontAwesomeIcon icon={faEraser} /></Button>
-//     <div className="slider-wrap">
-//       <span className="difficulty-label">Game Rules:</span>
-//       <Slider
-//         title="Game Rules:&#10;- regular: 🔐 levels, 🔐 tactics&#10;- lax: 🔓 levels, 🔐 tactics&#10;- none: 🔓 levels, 🔓 tactics"
-//         min={0} max={2}
-//         aria-label="Game Rules"
-//         defaultValue={difficulty}
-//         marks={[
-//           {value: 0, label: label(0)},
-//           {value: 1, label: label(1)},
-//           {value: 2, label: label(2)}
-//         ]}
-//         valueLabelFormat={label}
-//         getAriaValueText={label}
-//         valueLabelDisplay="auto"
-//         onChange={(ev, val: number) => {
-//           dispatch(changedDifficulty({game: gameId, difficulty: val}))
-//         }}
-//         ></Slider>
-
-//     </div>
-//     {eraseMenu?
-//       <div className="modal-wrapper">
-//         <div className="modal-backdrop" onClick={closeEraseMenu} />
-//         <div className="modal">
-//           <div className="codicon codicon-close modal-close" onClick={closeEraseMenu}></div>
-//           <h2>Delete Progress?</h2>
-
-//           <p>Do you want to delete your saved progress irreversibly?</p>
-//           <p>
-//             (This deletes your proofs and your collected inventory.
-//             Saves from other games are not deleted.)
-//           </p>
-
-//           <Button onClick={eraseProgress} to="">Delete</Button>
-//           <Button onClick={downloadAndErase} to="">Download & Delete</Button>
-//           <Button onClick={closeEraseMenu} to="">Cancel</Button>
-//         </div>
-//       </div> : null}
-//     {uploadMenu ?
-//       <div className="modal-wrapper">
-//         <div className="modal-backdrop" onClick={closeUploadMenu} />
-//         <div className="modal">
-//           <div className="codicon codicon-close modal-close" onClick={closeUploadMenu}></div>
-//           <h2>Upload Saved Progress</h2>
-
-//           <p>Select a JSON file with the saved game progress to load your progress.</p>
-
-//           <p><b>Warning:</b> This will delete your current game progress!
-//             Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
-
-//           <input type="file" onChange={handleFileChange}/>
-
-//           <Button to="" onClick={uploadProgress}>Load selected file</Button>
-//         </div>
-//       </div> : null}
-//   </nav>
-// }
-
-
-/** The top-navigation bar */
-export function LevelAppBar({
-    isLoading, levelTitle, impressum, toggleImpressum,
-    pageNumber = undefined, setPageNumber = undefined}) {
+/** button to go one level futher.
+ * for the last level, this button turns into a button going back to the welcome page.
+ */
+function NextButton({worldSize, difficulty, completed, setNavOpen}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
-  const gameInfo = useGetGameInfoQuery({game: gameId})
-
-  const {mobile} = React.useContext(MobileContext)
-
-  const difficulty = useSelector(selectDifficulty(gameId))
-  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
-
-  const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
-
-  const [navOpen, setNavOpen] = React.useState(false)
-
-  return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
-    {mobile ?
-      <>
-        {/* MOBILE VERSION */}
-        <div>
-          <span className="app-bar-title">
-            {levelTitle}
-          </span>
-        </div>
-        <div className="nav-btns">
-          {mobile && pageNumber == 0 ?
-            <Button to="" className="btn btn-inverted toggle-width"
-                title="show inventory" inverted="true" onClick={() => {setPageNumber(1)}}>
-              <FontAwesomeIcon icon={faBook}/>
-            </Button>
-          : pageNumber == 1 &&
-            <Button className="btn btn-inverted toggle-width" to=""
-                title="show inventory" inverted="true" onClick={() => {setPageNumber(0)}}>
-              <FontAwesomeIcon icon={faXmark}/>
-            </Button>
-          }
-          <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}} >
-            {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
-          </Button>
-        </div>
-        <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
-          {levelId < gameInfo.data?.worldSize[worldId] &&
-            <Button inverted="true"
-                to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
-                disabled={difficulty >= 2 && !(completed || levelId == 0)}
-                onClick={() => setNavOpen(false)}>
-              <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
-            </Button>
-          }
-          {levelId > 0 && <>
-                <Button disabled={levelId <= 0} inverted="true"
-                    to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-                    title="previous level"
-                    onClick={() => setNavOpen(false)}>
-                  <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-                </Button>
-              </>}
-          <Button to={`/${gameId}`} inverted="true" title="back to world selection">
-            <FontAwesomeIcon icon={faHome} />&nbsp;Home
-          </Button>
-          <Button disabled={levelId <= 0} inverted="true" to=""
-              onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-              title="toggle Editor mode">
-            <FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
-          </Button>
-          <Button title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
-            <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Info &amp; Impressum
-          </Button>
-        </div>
-      </>
-    :
-      <>
-        {/* DESKTOP VERSION */}
-        <div>
-          <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
-            <FontAwesomeIcon icon={faHome} />
-          </Button>
-          <span className="app-bar-title">
-            {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
-          </span>
-        </div>
-        <div>
-          <span className="app-bar-title">
-            {levelTitle}
-          </span>
-        </div>
-        <div className="nav-btns">
-          {levelId > 0 && <>
-            <Button disabled={levelId <= 0} inverted="true"
-                to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-                title="previous level"
-                onClick={() => setNavOpen(false)}>
-              <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-            </Button>
-          </>}
-          {levelId < gameInfo.data?.worldSize[worldId] ?
+  return (levelId < worldSize ?
     <Button inverted="true"
         to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
         disabled={difficulty >= 2 && !(completed || levelId == 0)}
@@ -386,15 +76,179 @@ export function LevelAppBar({
     <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
       <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
     </Button>
+  )
+}
+
+/** button to go one level back.
+ * only renders if the current level id is > 0.
+ */
+function PreviousButton({setNavOpen}) {
+  const gameId = React.useContext(GameIdContext)
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  return (levelId > 0 && <>
+    <Button disabled={levelId <= 0} inverted="true"
+        to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
+        title="previous level"
+        onClick={() => setNavOpen(false)}>
+      <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
+    </Button>
+  </>)
+}
+
+/** button to toggle between editor and typewriter */
+function InputModeButton({setNavOpen, isDropdown}) {
+  const {levelId} = React.useContext(WorldLevelIdContext)
+  const {typewriterMode, setTypewriterMode, lockInputMode} = React.useContext(InputModeContext)
+
+  /** toggle input mode if allowed */
+  function toggleInputMode(ev: React.MouseEvent) {
+    if (!lockInputMode){
+      setTypewriterMode(!typewriterMode)
+      setNavOpen(false)
     }
-          <Button className="btn btn-inverted toggle-width" disabled={levelId <= 0} inverted="true" to=""
-              onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-              title="toggle Editor mode">
-            <FontAwesomeIcon icon={commandLineMode ? faCode : faTerminal} />
+  }
+
+  return <Button
+      className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockInputMode}
+      inverted="true" to=""
+      onClick={(ev) => toggleInputMode(ev)}
+      title={lockInputMode ? "Editor mode is enforced!" : typewriterMode ? "Editor mode" : "Typewriter mode"}>
+    <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
+    {isDropdown && (typewriterMode ? <>&nbsp;Editor mode</> : <>&nbsp;Typewriter mode</>)}
   </Button>
-          <Button className="btn btn-inverted toggle-width" title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
-            <FontAwesomeIcon icon={impressum ? faXmark : faCircleInfo} />
+}
+
+/** button to toggle iimpressum popup */
+function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
+  return <Button className="btn btn-inverted toggle-width"
+    title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faCircleInfo} />
+    {isDropdown && <>&nbsp;Info &amp; Impressum</>}
   </Button>
+}
+
+/**  button to go back to welcome page */
+function HomeButton({isDropdown}) {
+  const gameId = React.useContext(GameIdContext)
+  return <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
+    <FontAwesomeIcon icon={faHome} />
+    {isDropdown && <>&nbsp;Home</>}
+  </Button>
+}
+
+/** button in mobile level to toggle inventory.
+ * only displays a button if `setPageNumber` is set.
+ */
+function InventoryButton({pageNumber, setPageNumber}) {
+  return (setPageNumber &&
+    <Button to="" className="btn btn-inverted toggle-width"
+      title={pageNumber ? "close inventory" : "show inventory"}
+      inverted="true" onClick={() => {setPageNumber(pageNumber ? 0 : 1)}}>
+      <FontAwesomeIcon icon={pageNumber ? faBookOpen : faBook} />
+    </Button>
+  )
+}
+
+/** the navigation bar on the welcome page */
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
+  pageNumber: number,
+  setPageNumber: any,
+  gameInfo: GameInfo,
+  toggleImpressum: any,
+  toggleEraseMenu: any,
+  toggleUploadMenu: any,
+  toggleInfo: any
+}) {
+  const gameId = React.useContext(GameIdContext)
+  const gameProgress = useAppSelector(selectProgress(gameId))
+  const {mobile} = React.useContext(MobileContext)
+  const [navOpen, setNavOpen] = React.useState(false)
+
+  return <div className="app-bar">
+    <div>
+      <Button inverted="false" title="back to games selection" to="/">
+        <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
+      </Button>
+      <span className="app-bar-title"></span>
+    </div>
+    <div>
+      {!mobile && <span className="app-bar-title">{gameInfo?.title}</span>}
+    </div>
+    <div className="nav-btns">
+      {mobile && <MobileNavButtons pageNumber={pageNumber} setPageNumber={setPageNumber} />}
+      <MenuButton navOpen={navOpen} setNavOpen={setNavOpen} />
+    </div>
+    <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
+      <Button title="Game Info & Credits" inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Game Info
+      </Button>
+      <Button title="Clear Progress" inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faEraser} />&nbsp;Erase
+      </Button>
+      <Button title="Download Progress" inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faDownload} />&nbsp;Download
+      </Button>
+      <Button title="Load Progress from JSON" inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faUpload} />&nbsp;Upload
+      </Button>
+      <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
+      </Button>
+    </div>
+  </div>
+}
+
+/** the navigation bar in a level */
+export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=undefined, setPageNumber=undefined} : {
+  isLoading: boolean,
+  levelTitle: string,
+  toggleImpressum: any,
+  pageNumber?: number,
+  setPageNumber?: any,
+}) {
+  const gameId = React.useContext(GameIdContext)
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  const {mobile} = React.useContext(MobileContext)
+  const [navOpen, setNavOpen] = React.useState(false)
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
+  const difficulty = useAppSelector(selectDifficulty(gameId))
+
+  let worldTitle = gameInfo.data?.worlds.nodes[worldId].title
+
+  return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
+    {mobile ?
+      <>
+        {/* MOBILE VERSION */}
+        <div>
+          <span className="app-bar-title">{levelTitle}</span>
+        </div>
+        <div className="nav-btns">
+          <InventoryButton pageNumber={pageNumber} setPageNumber={setPageNumber}/>
+          <MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
+        </div>
+        <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
+          <NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
+          <PreviousButton setNavOpen={setNavOpen} />
+          <HomeButton isDropdown={true} />
+          <InputModeButton setNavOpen={setNavOpen} isDropdown={true}/>
+          <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
+        </div>
+      </> :
+      <>
+        {/* DESKTOP VERSION */}
+        <div>
+          <HomeButton isDropdown={false} />
+          <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
+        </div>
+        <div>
+          <span className="app-bar-title">{levelTitle}</span>
+        </div>
+        <div className="nav-btns">
+          <PreviousButton setNavOpen={setNavOpen} />
+          <NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
+          <InputModeButton setNavOpen={setNavOpen} isDropdown={false}/>
+          <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={false} />
         </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

@@ -65,13 +65,9 @@ export const ProofStateContext = React.createContext<{
 export const MobileContext = React.createContext<{
   mobile : boolean,
   setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-  pageNumber: number,
-  setPageNumber: React.Dispatch<React.SetStateAction<Number>>
 }>({
   mobile : false,
   setMobile: () => {},
-  pageNumber: 0,
-  setPageNumber: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{
@@ -105,13 +101,17 @@ export const DeletedChatContext = React.createContext<{
 })
 
 export const InputModeContext = React.createContext<{
-  commandLineMode: boolean,
-  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
-  commandLineInput: string,
-  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
+  typewriterMode: boolean,
+  setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
+  typewriterInput: string,
+  setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
+  lockInputMode: boolean,
+  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
-  commandLineMode: true,
-  setCommandLineMode: () => {},
-  commandLineInput: "",
-  setCommandLineInput: () => {},
+  typewriterMode: true,
+  setTypewriterMode: () => {},
+  typewriterInput: "",
+  setTypewriterInput: () => {},
+  lockInputMode: false,
+  setLockInputMode: () => {},
 });

client/src/components/infoview/goals.tsx

@@ -124,7 +124,7 @@ interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
     showHints?: boolean
-    commandLine: boolean
+    typewriter: boolean
 }
 
 interface ProofDisplayProps {
@@ -136,7 +136,7 @@ interface ProofDisplayProps {
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter, showHints, commandLine } = props
+    const { goal, filter, showHints, typewriter } = props
 
     // TODO: Apparently `goal` can be `undefined`
     if (!goal) {return <></>}
@@ -163,18 +163,18 @@ export const Goal = React.memo((props: GoalProps) => {
     // const hints = <Hints hints={goal.hints} key={goal.mvarId} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
-    const {commandLineMode} = React.useContext(InputModeContext)
+    const {typewriterMode} = React.useContext(InputModeContext)
 
     return <div>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
-        {! commandLine && objectHyps.length > 0 &&
+        {! typewriter && objectHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {!commandLine && assumptionHyps.length > 0 &&
+        {!typewriter && assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {/* {commandLine && commandLineMode && <CommandLine />} */}
+        {/* {typewriter && typewriterMode && <Typewriter />} */}
         {!filter.reverse && goalLi}
         {/* {showHints && hints} */}
     </div>
@@ -229,7 +229,7 @@ export const OtherGoals = React.memo((props: GoalProps2) => {
             <summary>
               <InteractiveCode fmt={goal.type} />
             </summary>
-            <Goal commandLine={false} filter={filter} goal={goal} />
+            <Goal typewriter={false} filter={filter} goal={goal} />
           </details>)}
       </div>}
   </>
@@ -264,7 +264,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-          {goals.goals.map((g, i) => <Goal commandLine={false} key={i} goal={g} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
         </>
     }
 }

client/src/components/infoview/info.tsx

@@ -129,7 +129,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           </div>
           <div>
             { goals && (goals.goals.length > 0
-              ? <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
+              ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
               : <div className="goals-section-title">No Goals</div>
             )}
           </div>
@@ -156,7 +156,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     <div className="goals-section-title">Weitere Goals</div>
 
                     {goals.goals.slice(1).map((goal, i) =>
-                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal commandLine={false} filter={goalFilter} goal={goal} /></details>)}
+                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)}
                 </div>}
         </LocationsContext.Provider> */}
     </>

client/src/components/infoview/main.tsx

@@ -6,7 +6,7 @@ import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location,
 import 'tachyons/css/tachyons.css';
 import '@vscode/codicons/dist/codicon.css';
 import '../../../../node_modules/lean4-infoview/src/infoview/index.css';
-import './infoview.css'
+import '../../css/infoview.css'
 
 import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api';
 import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
@@ -21,39 +21,36 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
 import { LevelInfo } from '../../state/api';
-import { changedInventory, levelCompleted, selectCompleted, selectInventory } from '../../state/progress';
+import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
 import Markdown from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context';
-import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line';
+import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
+import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 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.
  */
 export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) {
   const ec = React.useContext(EditorContext)
-  const { commandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode } = React.useContext(InputModeContext)
   return <>
-    <div className={commandLineMode ? 'hidden' : ''}>
-      <ExerciseStatement data={level} />
+    <div className={typewriterMode ? 'hidden' : ''}>
+      <ExerciseStatement data={level} showLeanStatement={true} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
     {ec ?
       <DualEditorMain worldId={worldId} levelId={levelId} level={level} worldSize={worldSize} /> :
       // TODO: Style this if relevant.
-      <>
-        <p>Editor is starting up...</p>
-        <CircularProgress />
-      </>
+      <></>
     }
   </>
 }
@@ -62,7 +59,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
 function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: string, levelId: number, level: LevelInfo, worldSize: number }) {
   const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
-  const { commandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode } = React.useContext(InputModeContext)
 
   // Mark level as completed when server gives notification
   const dispatch = useAppDispatch()
@@ -80,6 +77,11 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
           ...level?.definitions
         ].filter((tile) => tile.new).map((tile) => tile.name)
 
+        // Add the proven statement to the local storage as well.
+        if (level?.statementName != null) {
+          newTiles.push(level?.statementName)
+        }
+
         let inv: string[] = selectInventory(gameId)(store.getState())
 
         // add new items and remove duplicates
@@ -108,10 +110,10 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
         <WithRpcSessions>
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
-              {commandLineMode ?
-                <CommandLineInterface world={worldId} level={levelId} data={level} worldSize={worldSize}/>
+              {typewriterMode ?
+                <TypewriterInterfaceWrapper world={worldId} level={levelId} data={level} worldSize={worldSize}/>
                 :
-                <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
+                <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} data={level} />
               }
             </ProgressContext.Provider>
           </WithLspDiagnosticsContext>
@@ -126,22 +128,45 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  * - Theorem xyz: description
  * - Theorem xyz
  * - Exercises: description
+ *
+ * If `showLeanStatement` is true, it will additionally display the lean code.
  */
-function ExerciseStatement({ data }) {
-  if (!data?.descrText) { return <></> }
-  return <div className="exercise-statement"><Markdown>
-    {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}`}
-  </Markdown></div>
+function ExerciseStatement({ data, showLeanStatement = false }) {
+  if (!(data?.descrText || data?.descrFormat)) { return <></> }
+  return <>
+    <div className="exercise-statement">
+      {data?.descrText &&
+        <Markdown>
+          {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + data?.descrText}
+        </Markdown>
+      }
+      {data?.descrFormat && showLeanStatement &&
+        <p><code className="lean-code">{data?.descrFormat}</code></p>
+      }
+    </div>
+  </>
 }
 
 // TODO: This is only used in `EditorInterface`
-// while `CommandLineInterface` has this copy-pasted in.
-export function Main(props: { world: string, level: number }) {
+// while `TypewriterInterface` has this copy-pasted in.
+export function Main(props: { world: string, level: number, data: LevelInfo}) {
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
 
   const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
 
+  console.debug(`template: ${props.data?.template}`)
+
+  // React.useEffect (() => {
+  //   if (props.data.template) {
+  //     let code: string = selectCode(gameId, worldId, levelId)(store.getState())
+  //     if (!code.length) {
+  //       //models.push(monaco.editor.createModel(code, 'lean4', uri))
+  //     }
+  //   }
+  // }, [props.data.template])
+
   /* Set up updates to the global infoview state on editor events. */
   const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
 
@@ -203,8 +228,8 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
   if (!command) { return <></> }
   return <div className="command">
     <div className="command-text">{command}</div>
-    <Button to="" className="undo-button btn btn-inverted" title="Delete this and future commands" onClick={deleteProof}>
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Delete
+    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
     </Button>
   </div>
 }
@@ -232,7 +257,7 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 //       message = diag.message
 //   }
 
-//   const { commandLineMode } = React.useContext(InputModeContext)
+//   const { typewriterMode } = React.useContext(InputModeContext)
 
 //   return (
 //   // <details open>
@@ -251,7 +276,7 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 //       //     </span>
 //       // </summary>
 //       <div className={severityClass + ' ml1 message'}>
-//           {!commandLineMode && <p className="mv2">{title}</p>}
+//           {!typewriterMode && <p className="mv2">{title}</p>}
 //           <pre className="font-code pre-wrap">
 //               <InteractiveMessage fmt={message} />
 //           </pre>
@@ -261,41 +286,80 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 // }, fastIsEqual)
 
 /** The tabs of goals that lean ahs after the command of this step has been processed */
-function GoalsTab({ proofStep, last}: { proofStep: ProofStep, last : boolean }) {
+function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: ProofStep, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+
   const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
-  if (!proofStep.goals.length) { return <></> }
-
-  return <div>
+  return <div className="goal-tabs" onClick={onClick}>
     <div className={`tab-bar ${last ? 'current' : ''}`}>
       {proofStep.goals.map((goal, i) => (
         // TODO: Should not use index as key.
-        <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { setSelectedGoal(i); ev.stopPropagation() }}>
+        <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}>
           {i ? `Goal ${i + 1}` : "Active Goal"}
         </div>
       ))}
     </div>
     <div className="goal-tab vscode-light">
-      <Goal commandLine={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
     </div>
   </div>
 }
 
-/** The interface in command line mode */
-export function CommandLineInterface(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
-
+// Splitting up Typewriter into two parts is a HACK
+export function TypewriterInterfaceWrapper(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
   const ec = React.useContext(EditorContext)
+  const gameId = React.useContext(GameIdContext)
+
+  useClientNotificationEffect(
+    'textDocument/didClose',
+    (params: DidCloseTextDocumentParams) => {
+      if (ec.events.changedCursorLocation.current &&
+        ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
+        ec.events.changedCursorLocation.fire(undefined)
+      }
+    }, []
+  )
+
+  const serverVersion =
+    useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
+  const serverStoppedResult = useEventResult(ec.events.serverStopped);
+  // NB: the cursor may temporarily become `undefined` when a file is closed. In this case
+  // it's important not to reconstruct the `WithBlah` wrappers below since they contain state
+  // that we want to persist.
+
+  if (!serverVersion) { return <></> }
+  if (serverStoppedResult) {
+    return <div>
+      <p>{serverStoppedResult.message}</p>
+      <p className="error">{serverStoppedResult.reason}</p>
+    </div>
+  }
+
+  return <TypewriterInterface props={props} />
+}
+
+/** The interface in command line mode */
+export function TypewriterInterface({props}) {
+  const ec = React.useContext(EditorContext)
+  const gameId = React.useContext(GameIdContext)
   const editor = React.useContext(MonacoEditorContext)
   const model = editor.getModel()
   const uri = model.uri.toString()
-  const gameId = React.useContext(GameIdContext)
-  const { proof } = React.useContext(ProofContext)
-  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
-  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
 
+  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)
+  const { setTypewriterInput } = React.useContext(InputModeContext)
+  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
+  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
+  // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
+  // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
+
+  const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
 
   /** Delete all proof lines starting from a given line.
   * Note that the first line (i.e. deleting everything) is `1`!
@@ -303,13 +367,13 @@ export function CommandLineInterface(props: { world: string, level: number, data
   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)
 
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           { lineNumber: line, column: 1 },
           editor.getModel().getFullModelRange().getEndPosition()
@@ -318,6 +382,7 @@ export function CommandLineInterface(props: { world: string, level: number, data
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
+      setTypewriterInput(proof[line].command)
       ev.stopPropagation()
     }
   }
@@ -342,6 +407,11 @@ export function CommandLineInterface(props: { world: string, level: number, data
     } else {
       proofPanelRef.current?.scrollTo(0,0)
     }
+    // also reenable the commandline when the proof changes
+
+    // BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there,
+    // the commandline is not displaying disabled even though it should.
+    setDisableInput(false)
   }, [proof])
 
   // Scroll to element if selection changes
@@ -353,37 +423,6 @@ export function CommandLineInterface(props: { world: string, level: number, data
     }
   }, [selectedStep])
 
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
-
-  const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
-
-  const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
-
-  useClientNotificationEffect(
-    'textDocument/didClose',
-    (params: DidCloseTextDocumentParams) => {
-      if (ec.events.changedCursorLocation.current &&
-        ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
-        ec.events.changedCursorLocation.fire(undefined)
-      }
-    }, []
-  )
-
-  const serverVersion =
-    useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
-  const serverStoppedResult = useEventResult(ec.events.serverStopped);
-  // NB: the cursor may temporarily become `undefined` when a file is closed. In this case
-  // it's important not to reconstruct the `WithBlah` wrappers below since they contain state
-  // that we want to persist.
-
-  if (!serverVersion) { return <p>Waiting for Lean server to start...</p> }
-  if (serverStoppedResult) {
-    return <div>
-      <p>{serverStoppedResult.message}</p>
-      <p className="error">{serverStoppedResult.reason}</p>
-    </div>
-  }
-
   // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
 
   // If the last step has errors, we want to treat it as if it is part of the second-to-last step
@@ -417,16 +456,21 @@ export function CommandLineInterface(props: { world: string, level: number, data
 
   let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
-  // TODO: does the position matter at all?
-  const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
 
-  return <div className="commandline-interface">
+  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">
       <div className="tmp-pusher">
-        {!proof.length &&
-          <CircularProgress />
-        }
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
@@ -438,12 +482,12 @@ export function CommandLineInterface(props: { world: string, level: number, data
                 // entered command as it is still present in the command line.
                 // TODO: Should not use index as key.
                 return <div key={`proof-step-${i}`}>
-                  <Errors errors={step.errors} commandLineMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                 </div>
               } else {
-                return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')} onClick={toggleSelectStep(i)}>
+                return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
                   <Command command={step.command} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} commandLineMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                   {mobile && i == 0 && props.data?.introduction &&
                     <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
                       <Markdown>{props.data?.introduction}</Markdown>
@@ -460,7 +504,7 @@ export function CommandLineInterface(props: { world: string, level: number, data
                     }
                   </>
                   }
-                  <GoalsTab proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} />
+                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
                   {/* Show a message that there are no goals left */}
                   {!step.goals.length && (
                     <div className="message information">
@@ -489,11 +533,11 @@ export function CommandLineInterface(props: { world: string, level: number, data
                 }
               </div>
             }
-          </> : <></>
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
         }
       </div>
     </div>
-    <CommandLine hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
+    <Typewriter hidden={!withErr && proof[proof.length - 1]?.goals.length == 0} disabled={disableInput || !proof.length}/>
     </RpcContext.Provider>
   </div>
 }

client/src/components/infoview/messages.tsx

@@ -18,7 +18,7 @@ interface MessageViewProps {
 }
 
 /** A list of messages (info/warning/error) that are produced after this command */
-function Error({error, commandLineMode} : {error : InteractiveDiagnostic, commandLineMode : boolean}) {
+function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) {
   // The first step will always have an empty command
 
   const severityClass = error.severity ? {
@@ -41,7 +41,7 @@ function Error({error, commandLineMode} : {error : InteractiveDiagnostic, comman
   }
 
   return <div className={severityClass + ' ml1 message'}>
-    {!commandLineMode && <p className="mv2">{title}</p>}
+    {!typewriterMode && <p className="mv2">{title}</p>}
     <pre className="font-code pre-wrap">
       <InteractiveMessage fmt={message} />
     </pre>
@@ -50,9 +50,9 @@ function Error({error, commandLineMode} : {error : InteractiveDiagnostic, comman
 
 // TODO: Should not use index as key.
 /** A list of messages (info/warning/error) that are produced after this command */
-export function Errors ({errors, commandLineMode} : {errors : InteractiveDiagnostic[], commandLineMode : boolean}) {
+export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) {
   return <div>
-    {errors.map((err, i) => (<Error key={`error-${i}`} error={err} commandLineMode={commandLineMode}/>))}
+    {errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))}
   </div>
 }
 
@@ -79,7 +79,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         message = diag.message
     }
 
-    const { commandLineMode } = React.useContext(InputModeContext)
+    const { typewriterMode } = React.useContext(InputModeContext)
 
     return (
     // <details open>
@@ -98,7 +98,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         //     </span>
         // </summary>
         <div className={severityClass + ' ml1 message'}>
-            {!commandLineMode && <p className="mv2">{title}</p>}
+            {!typewriterMode && <p className="mv2">{title}</p>}
             <pre className="font-code pre-wrap">
                 <InteractiveMessage fmt={message} />
             </pre>

client/src/components/infoview/typewriter.tsx

@@ -64,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function CommandLine({hidden}: {hidden?: boolean}) {
+export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -74,7 +74,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
-  const {commandLineInput, setCommandLineInput} = React.useContext(InputModeContext)
+  const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
 
   const inputRef = useRef()
 
@@ -100,7 +100,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
         rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
       )
       msgCalls.push(
-        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1})
+        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
       )
     }
 
@@ -178,8 +178,8 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
         })
         // Save the proof to the context
         setProof(tmpProof)
-      })
-    })
+      }).catch((error) => {console.debug("promise broken")})
+    }).catch((error) => {console.debug("promise broken")})
   }, [editor, rpcSess, uri, model])
 
   // Run the command
@@ -190,26 +190,33 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     setDeletedChat([])
 
     const pos = editor.getPosition()
-    if (commandLineInput) {
+    if (typewriterInput) {
       setProcessing(true)
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           pos,
           editor.getModel().getFullModelRange().getEndPosition()
         ),
-        text: commandLineInput.trim() + "\n",
+        text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
       }])
+      setTypewriterInput('')
     }
 
     editor.setPosition(pos)
-  }, [commandLineInput, editor])
+  }, [typewriterInput, editor])
 
   useEffect(() => {
-    if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
-      oneLineEditor.setValue(commandLineInput)
+    if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
+      oneLineEditor.setValue(typewriterInput)
     }
-  }, [commandLineInput])
+  }, [typewriterInput])
+
+  useEffect(() => {
+    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
+      setTypewriterInput(proof[proof.length - 1].command)
+    }
+  }, [proof])
 
   // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
@@ -217,7 +224,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
       setProcessing(false)
       loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
-        setCommandLineInput("")
+        //setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     } else {
@@ -231,7 +238,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
 
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
-      value: commandLineInput,
+      value: typewriterInput,
       language: "lean4cmd",
       quickSuggestions: false,
       lightbulb: {
@@ -274,14 +281,14 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     // Ensure that our one-line editor can only have a single line
     const l = oneLineEditor.getModel().onDidChangeContent((e) => {
       const value = oneLineEditor.getValue()
-      setCommandLineInput(value)
+      setTypewriterInput(value)
       const newValue = value.replace(/[\n\r]/g, '')
       if (value != newValue) {
         oneLineEditor.setValue(newValue)
       }
     })
     return () => { l.dispose() }
-  }, [oneLineEditor, setCommandLineInput])
+  }, [oneLineEditor, setTypewriterInput])
 
   useEffect(() => {
     if (!oneLineEditor) return
@@ -308,10 +315,10 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     runCommand()
   }
 
-  return <div className={`command-line${hidden ? ' hidden' : ''}`}>
+  return <div className={`typewriter${hidden ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
       <form onSubmit={handleSubmit}>
-        <div className="command-line-input-wrapper">
-          <div ref={inputRef} className="command-line-input" />
+        <div className="typewriter-input-wrapper">
+          <div ref={inputRef} className="typewriter-input" />
         </div>
         <button type="submit" disabled={processing} className="btn btn-inverted">
           <FontAwesomeIcon icon={faWandMagicSparkles} /> Execute

client/src/components/inventory.tsx

@@ -1,8 +1,8 @@
 import * as React from 'react';
 import { useState, useEffect } from 'react';
-import './inventory.css'
+import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons'
+import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
@@ -29,7 +29,7 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
       {levelInfo?.definitions &&
         <InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} enableAll={enableAll}/>
       }
-      <h2>Lemmas</h2>
+      <h2>Theorems</h2>
       {levelInfo?.lemmas &&
         <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
       }
@@ -86,7 +86,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
       {[...modifiedItems].sort(
           // For lemas, sort entries `available > disabled > locked`
           // otherwise alphabetically
-          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled)
+          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return <InventoryItem key={`${item.category}-${item.name}`}
               showDoc={() => {openDoc({name: item.name, type: docType})}}

client/src/components/landing_page.tsx

@@ -6,12 +6,13 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
-import './landing_page.css'
-import coverRobo from '../assets/covers/formaloversum.png'
+import '../css/landing_page.css'
 import bgImage from '../assets/bg.jpg'
 
 import Markdown from './markdown';
-import {PrivacyPolicyPopup} from './privacy_policy'
+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,44 @@ 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>
   </div>
 
@@ -86,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})`}}>
@@ -102,40 +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="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]}
           />
-
-      <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"
-        />
-
+        ))
+      }
     </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
@@ -149,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 direclty 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>
@@ -178,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

@@ -4,7 +4,7 @@ import { useSelector, useStore } from 'react-redux'
 import Split from 'react-split'
 import { useParams } from 'react-router-dom'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faBars, faBook, faCode, faXmark, faHome, faCircleInfo, faArrowRight, faArrowLeft, faTerminal } from '@fortawesome/free-solid-svg-icons'
+import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons'
 import { CircularProgress } from '@mui/material'
 import type { Location } from 'vscode-languageserver-protocol'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
@@ -22,18 +22,19 @@ import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
-  selectHelp, selectDifficulty, selectInventory } from '../state/progress'
+  selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
 import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
-import { hasInteractiveErrors } from './infoview/command_line'
+import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
   ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints } from './hints'
-import { Impressum } from './privacy_policy'
+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'
@@ -41,17 +42,25 @@ import '@fontsource/roboto/500.css'
 import '@fontsource/roboto/700.css'
 import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
-import './level.css'
+import '../css/level.css'
 import { LevelAppBar } from './app_bar'
 
 function Level() {
   const params = useParams()
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
-  // useLoadWorldFiles(worldId)
+
+  const [impressum, setImpressum] = React.useState(false)
+
+  const closeImpressum = () => {
+    setImpressum(false)
+  }
 
   return <WorldLevelIdContext.Provider value={{worldId, levelId}}>
-    {levelId == 0 ? <Introduction /> : <PlayableLevel key={`${worldId}/${levelId}`}/>}
+    {levelId == 0 ?
+      <Introduction impressum={impressum} setImpressum={setImpressum} /> :
+      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} />}
+    {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
   </WorldLevelIdContext.Provider>
 }
 
@@ -127,20 +136,26 @@ function ChatPanel({lastLevel}) {
   //   // chatRef.current!.scrollTo(0,0)
   // }, [gameId, worldId, levelId])
 
+  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">
-      {level?.data?.introduction &&
-        <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelection(0)}>
-          <Markdown>{level?.data?.introduction}</Markdown>
-        </div>
-      }
-      {proof.map((step, i) => {
+      {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)} />
+      ))}
+      {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}/>
         }
       })}
@@ -176,7 +191,7 @@ function ChatPanel({lastLevel}) {
   </div>
 }
 
-function ExercisePanel({codeviewRef, impressum, closeImpressum, visible=true}) {
+function ExercisePanel({codeviewRef, visible=true}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -185,21 +200,25 @@ function ExercisePanel({codeviewRef, impressum, closeImpressum, visible=true}) {
     <div className="exercise">
       <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} worldSize={gameInfo.data?.worldSize[worldId]}/>
     </div>
-    {impressum ? <Impressum handleClose={closeImpressum} /> : null}
   </div>
 }
 
-function PlayableLevel() {
+function PlayableLevel({impressum, setImpressum}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(MobileContext)
 
+  const dispatch = useAppDispatch()
+
   const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
   const inventory: Array<String> = useSelector(selectInventory(gameId))
 
+  const typewriterMode = useSelector(selectTypewriterMode(gameId))
+  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
@@ -212,14 +231,13 @@ function PlayableLevel() {
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
-  const [commandLineMode, setCommandLineMode] = useState(true)
-  const [commandLineInput, setCommandLineInput] = useState("")
+
+  // 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
-  const [impressum, setImpressum] = React.useState(false)
-  function closeImpressum() {setImpressum(false)}
   function toggleImpressum() {setImpressum(!impressum)}
 
   // When clicking on an inventory item, the inventory is overlayed by the item's doc.
@@ -246,7 +264,7 @@ function PlayableLevel() {
     useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
 
   /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
-   * `CommandLineInterface`.
+   * `TypewriterInterface`.
    */
   const handleUndo = () => {
     const endPos = editor.getModel().getFullModelRange().getEndPosition()
@@ -278,29 +296,63 @@ function PlayableLevel() {
   // if the user inventory changes, notify the server
   useEffect(() => {
     let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, checkEnabled: difficulty > 0})
+    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
   }, [inventory])
 
+  useEffect (() => {
+    // Lock editor mode
+    if (level?.data?.template) {
+      setTypewriterMode(false)
+
+      if (editor) {
+        let code = editor.getModel().getLinesContent()
+
+        // console.log(`insert. code: ${code}`)
+        // console.log(`insert. join: ${code.join('')}`)
+        // console.log(`insert. trim: ${code.join('').trim()}`)
+        // console.log(`insert. length: ${code.join('').trim().length}`)
+        // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
+
+
+        // TODO: It does seem that the template is always indented by spaces.
+        // This is a hack, assuming there are exactly two.
+        if (!code.join('').trim().length) {
+          console.debug(`inserting template:\n${level.data.template}`)
+          // TODO: This does not work! HERE
+          // Probably overwritten by a query to the server
+          editor.executeEdits("template-writer", [{
+            range: editor.getModel().getFullModelRange(),
+            text: level.data.template + `\n`,
+            forceMoveMarkers: true
+          }])
+        } else {
+          console.debug(`not inserting template.`)
+        }
+      }
+    }
+  }, [level, levelId, worldId, gameId, editor])
+
+
   useEffect(() => {
     // TODO: That's a problem if the saved proof contains an error
     // Reset command line input when loading a new level
-    setCommandLineInput("")
+    setTypewriterInput("")
 
     // Load the selected help steps from the store
     setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState())))
   }, [gameId, worldId, levelId])
 
   useEffect(() => {
-    if (!commandLineMode) {
+    if (!typewriterMode && editor) {
       // Delete last input attempt from command line
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: editor.getSelection(),
         text: "",
         forceMoveMarkers: false
       }]);
       editor.focus()
     }
-  }, [commandLineMode])
+  }, [typewriterMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -320,46 +372,50 @@ function PlayableLevel() {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (editor && commandLineMode) {
-      let endPos = editor.getModel().getFullModelRange().getEndPosition()
-      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-        editor.executeEdits("command-line", [{
-          range: monaco.Selection.fromPositions(endPos, endPos),
-          text: "\n",
+    if (editor && typewriterMode) {
+      let code = editor.getModel().getLinesContent().filter(line => line.trim())
+      editor.executeEdits("typewriter", [{
+        range: editor.getModel().getFullModelRange(),
+        text: code.length ? code.join('\n') + '\n' : '',
         forceMoveMarkers: true
       }]);
+
+      // let endPos = editor.getModel().getFullModelRange().getEndPosition()
+      // if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
+      //   editor.executeEdits("typewriter", [{
+      //     range: monaco.Selection.fromPositions(endPos, endPos),
+      //     text: "\n",
+      //     forceMoveMarkers: true
+      //   }]);
+      // }
+      // let endPos = editor.getModel().getFullModelRange().getEndPosition()
+      // let currPos = editor.getPosition()
+      // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
+      //   // This is not a position that would naturally occur from Typewriter, reset:
+      //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
+      // }
     }
-      endPos = editor.getModel().getFullModelRange().getEndPosition()
-      let currPos = editor.getPosition()
-      if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
-        // This is not a position that would naturally occur from CommandLine, reset:
-        editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
-      }
-    }
-  }, [editor, commandLineMode])
+  }, [editor, typewriterMode])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
           <ProofContext.Provider value={{proof, setProof}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>
                 <LevelAppBar
+                  pageNumber={pageNumber} setPageNumber={setPageNumber}
                   isLoading={level.isLoading}
                   levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
                     (level?.data?.title && ` : ${level?.data?.title}`)}
-                  impressum={impressum}
-                    toggleImpressum={toggleImpressum}
-                  pageNumber={pageNumber} setPageNumber={setPageNumber} />
+                  toggleImpressum={toggleImpressum} />
                 {mobile?
                   // TODO: This is copied from the `Split` component below...
                   <>
                     <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
                       <ExercisePanel
-                        impressum={impressum}
-                        closeImpressum={closeImpressum}
                         codeviewRef={codeviewRef}
                         visible={pageNumber == 0} />
                       <InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
@@ -369,8 +425,6 @@ function PlayableLevel() {
                   <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
                     <ChatPanel lastLevel={lastLevel}/>
                     <ExercisePanel
-                      impressum={impressum}
-                      closeImpressum={closeImpressum}
                       codeviewRef={codeviewRef} />
                     <InventoryPanel levelInfo={level?.data} />
                   </Split>
@@ -384,7 +438,7 @@ function PlayableLevel() {
   </>
 }
 
-function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
+function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
 
@@ -396,7 +450,6 @@ function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
-      {impressum ? <Impressum handleClose={closeImpressum} /> : null}
     </div>
     <div className="button-row">
       {gameInfo.data?.worldSize[worldId] == 0 ?
@@ -412,7 +465,7 @@ function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
 export default Level
 
 /** The site with the introduction text of a world */
-function Introduction() {
+function Introduction({impressum, setImpressum}) {
   const gameId = React.useContext(GameIdContext)
   const {mobile} = useContext(MobileContext)
 
@@ -420,26 +473,31 @@ function Introduction() {
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
-  const [impressum, setImpressum] = React.useState(false)
+  const {worldId} = useContext(WorldLevelIdContext)
+
+  let image: string = gameInfo.data?.worlds.nodes[worldId].image
 
-  const closeImpressum = () => {
-    setImpressum(false)
-  }
 
   const toggleImpressum = () => {
     setImpressum(!impressum)
   }
 
   return <>
-    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" impressum={impressum} toggleImpressum={toggleImpressum}/>
+    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" toggleImpressum={toggleImpressum}/>
     {gameInfo.isLoading ?
       <div className="app-content loading"><CircularProgress /></div>
     : mobile ?
-        <IntroductionPanel gameInfo={gameInfo} impressum={impressum} closeImpressum={closeImpressum} />
+        <IntroductionPanel gameInfo={gameInfo} />
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
-          <IntroductionPanel gameInfo={gameInfo} impressum={impressum} closeImpressum={closeImpressum} />
-          <div className="world-image-container empty"></div>
+          <IntroductionPanel gameInfo={gameInfo} />
+          <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>
       }
@@ -575,7 +633,8 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
       return () => {
         editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose(); }
+        model.dispose();
+      }
     }
   }, [editor, levelId, connection, leanClientStarted])
 
@@ -597,27 +656,3 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
   return {editor, infoProvider, editorConnection}
 }
-
-/** Open all files in this world on the server so that they will load faster when accessed */
-function useLoadWorldFiles(worldId) {
-  const gameId = React.useContext(GameIdContext)
-  const gameInfo = useGetGameInfoQuery({game: gameId})
-  const store = useStore()
-
-  useEffect(() => {
-    if (gameInfo.data) {
-      const models = []
-      for (let levelId = 1; levelId <= gameInfo.data.worldSize[worldId]; levelId++) {
-        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
-        let model = monaco.editor.getModel(uri)
-        if (model) {
-          models.push(model)
-        } else {
-          const code = selectCode(gameId, worldId, levelId)(store.getState())
-          models.push(monaco.editor.createModel(code, 'lean4', uri))
-        }
-      }
-      return () => { for (let model of models) { model.dispose() } }
-    }
-  }, [gameInfo.data, worldId])
-}

client/src/components/popup/erase.tsx

@@ -0,0 +1,59 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { useSelector } from 'react-redux'
+import { GameIdContext } from '../../app'
+import { useAppDispatch } from '../../hooks'
+import { deleteProgress, selectProgress } from '../../state/progress'
+import { downloadFile } from '../world_tree'
+import { Button } from '../button'
+
+/** download the current progress (i.e. what's saved in the browser store) */
+export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) {
+  ev.preventDefault()
+  downloadFile({
+    data: JSON.stringify(gameProgress, null, 2),
+    fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+    fileType: 'text/json',
+  })
+}
+
+/** Pop-up to delete game progress.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function ErasePopup ({handleClose}) {
+  const gameId = React.useContext(GameIdContext)
+  const gameProgress = useSelector(selectProgress(gameId))
+  const dispatch = useAppDispatch()
+
+  const eraseProgress = () => {
+    dispatch(deleteProgress({game: gameId}))
+    handleClose()
+  }
+
+  const downloadAndErase = (ev) => {
+    downloadProgress(gameId, gameProgress, ev)
+    eraseProgress()
+  }
+
+  return <div className="modal-wrapper">
+  <div className="modal-backdrop" onClick={handleClose} />
+  <div className="modal">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Delete Progress?</h2>
+
+    <p>Do you want to delete your saved progress irreversibly?</p>
+    <p>
+      (This deletes your proofs and your collected inventory.
+      Saves from other games are not deleted.)
+    </p>
+
+    <Button onClick={eraseProgress} to="">Delete</Button>
+    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
+    <Button onClick={handleClose} to="">Cancel</Button>
+  </div>
+</div>
+}

client/src/components/popup/game_info.tsx

@@ -0,0 +1,23 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { Typography } from '@mui/material'
+import Markdown from '../markdown'
+
+/** Pop-up that is displaying the Game Info.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
+  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="welcome-text">
+      <Markdown>{info}</Markdown>
+    </Typography>
+  </div>
+</div>
+}

client/src/components/popup/privacy_policy.tsx

@@ -11,7 +11,7 @@ import * as React from 'react'
  * controlled by the containing element.
  */
 export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
-  return <div className="modal-wrapper">
+  return <div className="privacy-policy modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
@@ -31,7 +31,7 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
     <p>Our server is located in Germany.</p>
     <p>
       <strong>Contact information:</strong><br />
-      Jon Eugster<br />
+      Alexander Bentkamp, Jon Eugster<br />
       Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
       Universitätsstr. 1<br />
       40225 Düsseldorf<br />
@@ -39,6 +39,21 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
       +49 211 81-12173<br />
       <a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
     </p>
+    <h2>Development &amp; Funding</h2>
+    <p>
+      The source code of this Lean game engine
+      is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
+      If you experience any problems, please
+      file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
+      get directly in contact.
+    </p>
+    <p>
+      The game engine has been developed as part of the
+      project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
+      Age of Mathematics</a> at
+      Heinrich-Heine-Universität Düsseldorf. It is funded by
+      the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
+    </p>
   </div>
 </div>
 }
@@ -58,49 +73,3 @@ export const PrivacyPolicy: React.FC = () => {
     </>
   )
 }
-
-export function Impressum({handleClose}) {
-  return <div className="impressum">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Funding</h2>
-    <p>
-      This Lean game engine has been developed as part of the
-      project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
-      Age of Mathematics</a> at
-      Heinrich-Heine-Universität Düsseldorf. It is funded by
-      the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
-    </p>
-
-    <h2>Development</h2>
-    <p>
-      The source code is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
-      If you experience any problems, please
-      file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
-      get directly in contact.
-    </p>
-    <h2>Privacy Policy &amp; Impressum</h2>
-    <p>
-      Our server collects metadata (such as IP address, browser, operating system)
-      and the data that the user enters into the editor. The data is used to
-      compute the Lean output and display it to the user. The information will be stored
-      as long as the user stays on our website and will be deleted immediately afterwards.
-      We keep logs to improve our software, but the contained data is anonymised.
-    </p>
-    <p>
-      We do not use cookies, but your game progress is stored in the browser storage
-      as site data. Your game progress is not saved on the server; if you delete
-      your browser storage, it is completely gone.
-    </p>
-    <p>Our server is located in Germany.</p>
-    <p>
-      <strong>Contact information:</strong><br />
-      Jon Eugster<br />
-      Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
-      Universitätsstr. 1<br />
-      40225 Düsseldorf<br />
-      Germany<br />
-      +49 211 81-12173<br />
-      <a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
-    </p>
-  </div>
-}

client/src/components/popup/rules_help.tsx

@@ -0,0 +1,55 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+
+/** Pop-up that is displayed when opening the help explaining the game rules.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
+  return <div className="privacy-policy modal-wrapper">
+  <div className="modal-backdrop" onClick={handleClose} />
+  <div className="modal">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Game Rules</h2>
+    <p>
+      Game rules determine if it is allowed to skip levels and if the games runs checks to only
+      allow unlocked tactics and theorems in proofs.
+    </p>
+    <p>
+      Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
+      tactics needed to solve a level, plus any tactics you unlocked in another level. That means
+      if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
+    </p>
+    <p>The options are:</p>
+    <table>
+      <thead>
+        <tr>
+          <th scope="col"></th>
+          <th scope="col">levels</th>
+          <th scope="col">tactics</th>
+        </tr>
+      </thead>
+      <tbody>
+        <tr>
+          <th scope="row">regular</th>
+          <td>🔐</td>
+          <td>🔐</td>
+        </tr>
+        <tr>
+          <th scope="row">relaxed</th>
+          <td>🔓</td>
+          <td>🔐</td>
+        </tr>
+        <tr>
+          <th scope="row">none</th>
+          <td>🔓</td>
+          <td>🔓</td>
+        </tr>
+      </tbody>
+    </table>
+  </div>
+</div>
+}

client/src/components/popup/upload.tsx

@@ -0,0 +1,70 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { useSelector } from 'react-redux'
+import { GameIdContext } from '../../app'
+import { useAppDispatch } from '../../hooks'
+import { GameProgressState, loadProgress, selectProgress } from '../../state/progress'
+import { downloadFile } from '../world_tree'
+import { Button } from '../button'
+
+/** Pop-up that is displaying the Game Info.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function UploadPopup ({handleClose}) {
+  const [file, setFile] = React.useState<File>();
+  const gameId = React.useContext(GameIdContext)
+  const gameProgress = useSelector(selectProgress(gameId))
+  const dispatch = useAppDispatch()
+
+  const handleFileChange = (e) => {
+    if (e.target.files) {
+      setFile(e.target.files[0])
+    }
+  }
+
+  /** Upload progress from a  */
+  const uploadProgress = (e) => {
+    if (!file) {return}
+    const fileReader = new FileReader()
+    fileReader.readAsText(file, "UTF-8")
+    fileReader.onload = (e) => {
+      const data = JSON.parse(e.target.result.toString()) as GameProgressState
+      console.debug("Json Data", data)
+      dispatch(loadProgress({game: gameId, data: data}))
+    }
+    handleClose()
+  }
+
+  /** Download the current progress (i.e. what's saved in the browser store) */
+  const downloadProgress = (e) => {
+    e.preventDefault()
+    downloadFile({
+      data: JSON.stringify(gameProgress, null, 2),
+      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+      fileType: 'text/json',
+    })
+  }
+
+
+  return <div className="modal-wrapper">
+  <div className="modal-backdrop" onClick={handleClose} />
+  <div className="modal">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Upload Saved Progress</h2>
+
+    <p>Select a JSON file with the saved game progress to load your progress.</p>
+
+    <p><b>Warning:</b> This will delete your current game progress!
+      Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
+    <p>
+      <input type="file" onChange={handleFileChange}/>
+    </p>
+
+    <Button to="" onClick={uploadProgress}>Load selected file</Button>
+  </div>
+</div>
+}

client/src/components/welcome.tsx

@@ -1,29 +1,32 @@
 import * as React from 'react'
-import { useState, useEffect } from 'react'
-import { useSelector } from 'react-redux'
+import { useEffect } from 'react'
 import Split from 'react-split'
-import { Box, Typography, CircularProgress } from '@mui/material'
+import { Box, CircularProgress } from '@mui/material'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faGlobe, faBook, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
+import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch } from '../hooks'
-import { GameProgressState, changedOpenedIntro, deleteProgress, loadProgress, selectOpenedIntro, selectProgress } from '../state/progress'
+import { useAppDispatch, useAppSelector } from '../hooks'
+import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { MobileContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
-import Markdown from './markdown'
-import {PrivacyPolicyPopup} from './privacy_policy'
-import { WorldTreePanel, downloadFile } from './world_tree'
+import { ErasePopup } from './popup/erase'
+import { InfoPopup } from './popup/game_info'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
+import { RulesHelpPopup } from './popup/rules_help'
+import { UploadPopup } from './popup/upload'
+import { WorldTreePanel } from './world_tree'
 
-import './welcome.css'
+import '../css/welcome.css'
 import { WelcomeAppBar } from './app_bar'
 import { Hint } from './hints'
 
-/** The panel showing the game's introduction text */
-function IntroductionPanel({introduction}: {introduction: string}) {
-  const {mobile, setPageNumber} = React.useContext(MobileContext)
+
+/** the panel showing the game's introduction text */
+function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
+  const {mobile} = React.useContext(MobileContext)
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
@@ -43,11 +46,6 @@ function IntroductionPanel({introduction}: {introduction: string}) {
         : <></>
       ))}
     </div>
-    {/* <Typography variant="body1" component="div" className="welcome-text">
-          <h1>{title}</h1>
-          <Markdown>{introduction}</Markdown>
-        </Typography>
-    */}
     {mobile &&
       <div className="button-row">
         <Button className="btn" to=""
@@ -62,142 +60,32 @@ function IntroductionPanel({introduction}: {introduction: string}) {
   </div>
 }
 
-export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
-  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="welcome-text">
-      <Markdown>{info}</Markdown>
-    </Typography>
-  </div>
-</div>
-}
-
-
-function ErasePopup ({handleClose}) {
-  const gameId = React.useContext(GameIdContext)
-  const gameProgress = useSelector(selectProgress(gameId))
-  const dispatch = useAppDispatch()
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-  const eraseProgress = () => {
-    dispatch(deleteProgress({game: gameId}))
-    handleClose()
-  }
-
-  const downloadAndErase = (e) => {
-    downloadProgress(e)
-    eraseProgress()
-  }
-
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Delete Progress?</h2>
-
-    <p>Do you want to delete your saved progress irreversibly?</p>
-    <p>
-      (This deletes your proofs and your collected inventory.
-      Saves from other games are not deleted.)
-    </p>
-
-    <Button onClick={eraseProgress} to="">Delete</Button>
-    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
-    <Button onClick={handleClose} to="">Cancel</Button>
-  </div>
-</div>
-}
-
-function UploadPopup ({handleClose}) {
-  const [file, setFile] = React.useState<File>();
-  const gameId = React.useContext(GameIdContext)
-  const gameProgress = useSelector(selectProgress(gameId))
-  const dispatch = useAppDispatch()
-
-  const handleFileChange = (e) => {
-    if (e.target.files) {
-      setFile(e.target.files[0])
-    }
-  }
-
-  /** Upload progress from a  */
-  const uploadProgress = (e) => {
-    if (!file) {return}
-    const fileReader = new FileReader()
-    fileReader.readAsText(file, "UTF-8")
-    fileReader.onload = (e) => {
-      const data = JSON.parse(e.target.result.toString()) as GameProgressState
-      console.debug("Json Data", data)
-      dispatch(loadProgress({game: gameId, data: data}))
-    }
-    handleClose()
-  }
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Upload Saved Progress</h2>
-
-    <p>Select a JSON file with the saved game progress to load your progress.</p>
-
-    <p><b>Warning:</b> This will delete your current game progress!
-      Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
-
-    <input type="file" onChange={handleFileChange}/>
-
-    <Button to="" onClick={uploadProgress}>Load selected file</Button>
-  </div>
-</div>
-}
-
-/** main page of the game showing amoung others the tree of worlds/levels */
+/** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
-  // impressum pop-up
+  // For mobile only
+  const openedIntro = useAppSelector(selectOpenedIntro(gameId))
+  const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+
+  // pop-ups
+  const [eraseMenu, setEraseMenu] = React.useState(false)
   const [impressum, setImpressum] = React.useState(false)
-  function closeImpressum() {setImpressum(false)}
-  function toggleImpressum() {setImpressum(!impressum)}
-
   const [info, setInfo] = React.useState(false)
+  const [rulesHelp, setRulesHelp] = React.useState(false)
+  const [uploadMenu, setUploadMenu] = React.useState(false)
+  function closeEraseMenu()   {setEraseMenu(false)}
+  function closeImpressum()   {setImpressum(false)}
   function closeInfo()        {setInfo(false)}
-  function toggleInfo() {setInfo(!impressum)}
-
-
-  /* state variables to toggle the pop-up menus */
-  const [eraseMenu, setEraseMenu] = React.useState(false);
-  const openEraseMenu = () => setEraseMenu(true);
-  const closeEraseMenu = () => setEraseMenu(false);
-  const [uploadMenu, setUploadMenu] = React.useState(false);
-  const openUploadMenu = () => setUploadMenu(true);
-  const closeUploadMenu = () => setUploadMenu(false);
-
+  function closeRulesHelp()   {setRulesHelp(false)}
+  function closeUploadMenu()  {setUploadMenu(false)}
+  function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
+  function toggleImpressum()  {setImpressum(!impressum)}
+  function toggleInfo()       {setInfo(!info)}
+  function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
 
   // set the window title
   useEffect(() => {
@@ -211,28 +99,32 @@ function Welcome() {
       <CircularProgress />
     </Box>
   : <>
-    <WelcomeAppBar gameInfo={gameInfo.data} toggleImpressum={toggleImpressum} openEraseMenu={openEraseMenu}
-      openUploadMenu={openUploadMenu} toggleInfo={toggleInfo} />
+    <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
+      toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
+      toggleInfo={toggleInfo} />
     <div className="app-content">
       { mobile ?
           <div className="welcome mobile">
             {(pageNumber == 0 ?
-              <IntroductionPanel introduction={gameInfo.data?.introduction} />
+              <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
             : pageNumber == 1 ?
-              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize} />
+              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
+                rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             :
               <InventoryPanel levelInfo={inventory?.data} />
             )}
           </div>
         :
           <Split className="welcome" minSize={0} snapOffset={200}  sizes={[25, 50, 25]}>
-            <IntroductionPanel introduction={gameInfo.data?.introduction} />
-            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize} />
+            <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
+            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
+              rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             <InventoryPanel levelInfo={inventory?.data} />
           </Split>
       }
     </div>
     {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
+    {rulesHelp ? <RulesHelpPopup handleClose={closeRulesHelp} /> : null}
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}

client/src/components/world_tree.tsx

@@ -8,16 +8,14 @@ import { Slider } from '@mui/material'
 import cytoscape, { LayoutOptions } from 'cytoscape'
 import klay from 'cytoscape-klay'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faDownload, faUpload, faEraser, faGlobe, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
+import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch } from '../hooks'
-import { deleteProgress, selectProgress, loadProgress, GameProgressState,
-  selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
+import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
-import { Button } from './button'
 
-import './world_tree.css'
+import '../css/world_tree.css'
 
 // Settings for the world tree
 cytoscape.use( klay )
@@ -28,8 +26,11 @@ const lineWidth = 10      //
 const ds = .75  // scale the resulting svg image
 
 const NMIN = 5   // min. worldsize
-const NLABEL = 9 // max. world size to display label below the world
+const NLABEL = 8 // max. world size to display label below the world
 const NMAX = 16  // max. world size. Level icons start spiraling out if the world has more levels.
+const NSPIRAL = 12 // world size if NMAX has been passed and need to spiral.
+
+const MINFONT = 12
 
 // colours
 const grey = '#999'
@@ -54,8 +55,9 @@ export function LevelIcon({ world, level, position, completed, unlocked, worldSi
 
   const N = Math.max(worldSize, NMIN)
 
-  // divide circle into `N+2` equal pieces
-  const beta = 2 * Math.PI / Math.min(N+2, (NMAX+1))
+  // divide circle into `N+2` equal pieces.
+  // only for non-spiraling case
+  const beta = 2 * Math.PI / Math.min(N+2, ((N < (NMAX+1) ? NMAX : NSPIRAL)+1))
 
   // We want distance between two level icons to be `2.2*r`, therefore:
   // Sinus-Satz: (1.1*r) / sin(β/2) = R / sin(π/2)
@@ -70,19 +72,19 @@ export function LevelIcon({ world, level, position, completed, unlocked, worldSi
    * works fine in tests up to `N=30`.
    */
   function betaSpiral(level) {
-    return 2 * Math.PI / ((NMAX+1) + Math.max(0, (level-2)) / (NMAX+1))
+    return 2 * Math.PI / ((NSPIRAL+1) + 2 * Math.max(0, (level-2)) / (NSPIRAL+1))
   }
 
   const x = N < (NMAX+1) ?
     // normal case
     s * position.x + Math.sin(level * beta) * R :
     // spiraling case
-    s * position.x + Math.sin(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NMAX+1))
+    s * position.x + Math.sin(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NSPIRAL+1))
   const y = N < (NMAX+1) ?
     // normal case
     s * position.y - Math.cos(level * beta) * R :
     // spiraling case
-    s * position.y - Math.cos(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NMAX+1))
+    s * position.y - Math.cos(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NSPIRAL+1))
 
   return (
     <Link to={levelDisabled ? '' : `/${gameId}/world/${world}/level/${level == 1 ? 0 : level}`}
@@ -112,9 +114,11 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
 
   // See level icons. Match radius computed there minus `1.2*r`
   const N = Math.max(worldSize, NMIN)
-  const betaHalf = Math.PI / Math.min(N+2, (NMAX + 1))
+  const betaHalf = Math.PI / Math.min(N+2, ((N < (NMAX+1) ? NMAX : NSPIRAL) + 1))
   let R = 1.1 * r / Math.sin(betaHalf) - 1.2 * r
 
+  let fontSize = Math.floor(R/4)
+
   // Offset for the labels for small worlds
   let labelOffset = R + 2.5 * r
 
@@ -137,12 +141,14 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
       className={playable ? '' : 'disabled'}>
     <circle className="world-circle" cx={s*position.x} cy={s*position.y} r={R}
         fill={completed ? green : unlocked ? blue : grey}/>
-    {worldSize > NLABEL ?
+    { false ? // fontSize >= MINFONT ?
+      // NOTE: This code would display the world names inside the bubble, but currently
+      //       it isn't used.
       // Label for large worlds
       <foreignObject className="world-title-wrapper" x={s*position.x} y={s*position.y}
           width={1.42*R} height={1.42*R} transform={"translate("+ -.71*R +","+ -.71*R +")"}>
         <div className={unlocked && !completed ? "playable-world" : ''}>
-          <p className="world-title" style={{fontSize: Math.floor(R/4) + "px"}}>
+          <p className="world-title" style={{fontSize: fontSize + "px"}}>
             {title ? title : world}
           </p>
         </div>
@@ -153,7 +159,7 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
           width='150px' height='2em' style={{overflow: 'visible'}}
           >
         <div className='world-label' style={{backgroundColor: completed ? darkgreen : unlocked ? darkblue : darkgrey}}>
-          <p className='world-title'>
+          <p className='world-title' style={{fontSize: MINFONT + "px"}}>
             {title ? title : world}
           </p>
         </div>
@@ -187,7 +193,7 @@ export const downloadFile = ({ data, fileName, fileType } :
 }
 
 /** The menu that is shown next to the world selection graph */
-export function WorldSelectionMenu() {
+export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
@@ -196,12 +202,15 @@ export function WorldSelectionMenu() {
     return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
   }
 
+
   return <nav className="world-selection-menu">
     <div className="slider-wrap">
-      <span className="difficulty-label">Game Rules</span>
+      <span className="difficulty-label">Rules
+        <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
+      </span>
       <Slider
         orientation="vertical"
-        title="Game Rules:&#10;- regular: 🔐 levels, 🔐 tactics&#10;- relaxed: 🔓 levels, 🔐 tactics&#10;- none: 🔓 levels, 🔓 tactics"
+        title="Game Rules"
         min={0} max={2}
         aria-label="Game Rules"
         defaultValue={difficulty}
@@ -256,9 +265,12 @@ export function computeWorldLayout(worlds) {
 }
 
 
-export function WorldTreePanel({worlds, worldSize}:
+export function WorldTreePanel({worlds, worldSize, rulesHelp, setRulesHelp}:
   { worlds: any,
-    worldSize: any}) {
+    worldSize: any,
+    rulesHelp: boolean,
+    setRulesHelp: any,
+  }) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const {nodes, bounds}: any = worlds ? computeWorldLayout(worlds) : {nodes: []}
@@ -342,7 +354,7 @@ export function WorldTreePanel({worlds, worldSize}:
   let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : null
 
   return <div className="column">
-      <WorldSelectionMenu />
+      <WorldSelectionMenu rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
       <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink"
           width={bounds ? `${ds * dx}` : ''}
           viewBox={bounds ? `${s*bounds.x1 - padding} ${s*bounds.y1 - padding} ${dx} ${s*(bounds.y2 - bounds.y1) + 2 * padding}` : ''}

client/src/css/app.css

@@ -42,12 +42,6 @@ body {
   border-radius: .3em;
 }
 
-
-/* Hide monaco editor notifications */
-.monaco-workbench > .notifications-toasts.visible {
-  display: none !important;
-}
-
 .loading {
   margin: auto;
   height: 100%;
@@ -108,6 +102,7 @@ em {
   flex: 0;
   background: var(--clr-primary);
   display: flex;
+  position: relative;
   flex-direction: row;
   justify-content: space-between;
   padding: 1.1em;
@@ -139,3 +134,7 @@ em {
 .markdown ul, .markdown ol {
 	margin:0 1.5em 1.5em 1.5em;
 }
+
+.privacy-policy {
+  z-index: 10;
+}

client/src/css/infoview.css

@@ -43,7 +43,7 @@
   font-weight: 500;
 }
 
-.command-line {
+.typewriter {
   background: var(--clr-primary);
   padding: 0.5em;
   font-family: var(--ff-primary);
@@ -51,17 +51,33 @@
   /* margin: 0.2em 0 0; */
 }
 
-.command-line form {
+.typewriter.disabled{
+  background: #bbb;
+}
+
+.typewriter.disabled .btn-inverted,
+.typewriter.disabled .mtk1 {
+  color: #777;
+}
+
+.typewriter.disabled .typewriter-input-wrapper,
+.typewriter.disabled .monaco-editor,
+.typewriter.disabled .monaco-editor-background,
+.typewriter.disabled .btn-inverted {
+  background-color: #eee;
+}
+
+.typewriter form {
   display: flex;
 }
 
-.command-line button, .undo-button {
+.typewriter button, .undo-button {
   display: block;
   white-space: nowrap;
   flex: 0;
 }
 
-.command-line .command-line-input-wrapper{
+.typewriter .typewriter-input-wrapper{
   min-width: 0;
   flex: 1;
   padding: 0.4em .6em 0;
@@ -71,15 +87,22 @@
   flex-direction: column;
 }
 
-.command-line .command-line-input {
+.typewriter-interface .proof .MuiCircularProgress-root {
+  left: 50%;
+  position: relative;
+  margin-left: -20px;
+  margin-bottom: 0.6em;
+}
+
+.typewriter .typewriter-input {
   flex: 1;
 }
 
 /* Turn off some monaco decorations: */
-.command-line-input .monaco-editor .view-overlays .current-line {
+.typewriter-input .monaco-editor .view-overlays .current-line {
   border: 0;
 }
-.command-line-input .monaco-editor .scroll-decoration {
+.typewriter-input .monaco-editor .scroll-decoration {
   box-shadow: none;
 }
 
@@ -138,7 +161,7 @@
 
 
 /* Push the goals to the bottom for now, until we insert the proof history above. */
-.commandline-interface .content {
+.typewriter-interface .content {
   display: flex;
   flex-direction: column;
   scroll-behavior: smooth;
@@ -149,7 +172,7 @@
   scroll-behavior: smooth;
 }
 
-.commandline-interface .content .tmp-pusher {
+.typewriter-interface .content .tmp-pusher {
   flex: 1;
 }
 
@@ -157,7 +180,10 @@
   background-color: #bbb;
   padding: .5em;
   border-radius: .2em;
-  margin-bottom: 2rem;
+  /* TODO: It seems my browsers merge the margings of the proof steps,
+  so that it only shows once 0.5rem instead of twice. Thus have 1.5 here now.
+  */
+  margin-bottom: 1.5rem;
   display: flex;
   flex-direction: row;
 }

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

@@ -41,6 +41,20 @@
   padding-right: .5em;
 }
 
+.exercise-statement {
+  padding-top: 1em;
+  padding-bottom: 1em;
+}
+
+.exercise-statement p {
+  margin: 0;
+}
+
+.exercise-statement .lean-code {
+  color: rgba(0, 32, 90, 0.87);
+  font-size: 12px; /* TODO: is the monaco font-size hardcoded? */
+}
+
 .conclusion {
   padding: 1em;
 }
@@ -218,17 +232,17 @@ td code  {
   height: 100%;
 } */
 
-.commandline-interface {
+.typewriter-interface {
   display: flex;
   flex-flow: column;
   height: 100%;
 }
 
-.command-line {
+.typewriter {
   flex: 0 1 auto;
 }
 
-.commandline-interface .content {
+.typewriter-interface .content {
   flex: 1 1 auto;
   overflow-y: scroll;
   padding: 0;
@@ -257,7 +271,7 @@ td code  {
   box-shadow: .0em .0em .4em .1em #8cbbe9;
 }
 
-.exercise .step.selected, .chat .selected {
+.exercise .step.selected .goal-tabs, .chat .selected {
   /* border: 3px solid #5191d1; */
   box-shadow: .0em .0em .4em .1em var(--clr-primary);
 }
@@ -318,11 +332,26 @@ td code  {
   justify-content: center;
 }
 
-.commandline-interface .content, .world-image-container.empty {
+.typewriter-interface .content, .world-image-container.empty {
   background-color: #eee;
 }
 
-.commandline-interface .proof {
+.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 {
-  padding: .5em 1em;
   position: absolute;
   right: 1em;
   top: 1em;
@@ -75,7 +74,7 @@ svg .disabled {
   /* width: 100%; */
   height: 7em;
   /* min-width: 16em; */
-  padding-bottom: .8em;
+  padding: .5em 1em 1.3em 1em;
   margin-left: auto;
   margin-right: auto;
 }
@@ -109,3 +108,10 @@ svg .disabled {
   padding: .2em;
   border-radius: .5em;
 }
+
+.world-selection-menu .helpButton {
+  position: absolute;
+  right: .5em;
+  top: .5em;
+  color: var(--clr-primary);
+}

client/src/index.tsx

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

client/src/index_local.tsx

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

client/src/state/api.ts

@@ -2,16 +2,29 @@
  * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
-import { Connection } from '../connection'
+
+
+export interface GameTile {
+  title: string
+  short: string
+  long: string
+  languages: Array<string>
+  prerequisites: Array<string>
+  worlds: number
+  levels: number
+  image: string
+}
 
 export interface GameInfo {
   title: null|string,
   introduction: null|string,
   info: null|string,
-  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]},
+  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string, image: string}}, edges: string[][]},
   worldSize: null|{[key: string]: number},
   authors: null|string[],
   conclusion: null|string,
+  tile: null|GameTile,
+  image: null|string
 }
 
 export interface InventoryTile {
@@ -36,7 +49,9 @@ export interface LevelInfo {
   descrFormat: null|string,
   lemmaTab: null|string,
   statementName: null|string,
-  template: null|string
+  displayName: null|string,
+  template: null|string,
+  image: null|string
 }
 
 /** Used to display the inventory on the welcome page */
@@ -56,40 +71,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/progress.ts

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

doc/DOCUMENTATION.md

@@ -1,6 +1,8 @@
+**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
+
 # Creating a game.
 
-Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
+Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
 
 ## Game Structure
 
@@ -8,9 +10,7 @@ A game consist of worlds which have multiple levels each. In the following we de
 
 ### Level
 
-#### Preample
-
-A level file is a lean file that imports at least `GameServer.Commands` and starts with the four lean commands
+A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
 
 ```lean
 Game "NNG"
@@ -19,12 +19,12 @@ Level 1
 Title "The rfl tactic"
 ```
 
-Note that the levels inside a world must have consequtive numbering starting with `1`. The `Game`
-and `World` strings can be anything.
+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:
+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$. -/
@@ -53,10 +53,12 @@ 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 alternativ tactic sequence, which
+- `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`: not implemented yet, but used to provide a sample proof template.
+- `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)
 
@@ -77,26 +79,27 @@ There are three places where the documentation comment appears:
   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 a `Introduction "some text"` and `Conclusion "some text"` to your level.
+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.
 
-#### Lemmas/Tactics/Definitions
+#### Theorems/Tactics/Definitions
 
-Only enabled lemmas/tactics/definitions (called "items" here) are available in a level.
+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
-NewDefinition Nat
+NewLemma MyNat.add_zero MyNat.add_succ
+NewDefinition Nat Pow Mul
 ```
 
 Once added, items will be available in all future levels/worlds,
@@ -107,7 +110,7 @@ DisabledTactic tauto
 DisabledLemma MyNat.add_zero
 ```
 
-or specify explicitely which items should be available with
+or specify explicitly which items should be available with
 
 ```lean
 OnlyTactic rw rfl apply
@@ -134,10 +137,9 @@ 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 and they **must not** be
-imported in another world's levels. (bug?)
+Note that all levels of a world should be imported by the world file.
 
-However, you can import an entire world in a different world's level: `import NNG.Levels.Addition`
+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
 
@@ -152,17 +154,18 @@ Game "NNG"
 Title "Natural Number Game"
 Introduction "some text"
 
-Path Addition → Multiplication → Power
-
 MakeGame
 ```
 
-There can be several `Path` statements to define the relation between the worlds. The worlds
-must form a directed acyclic graph, i.e. have no loops. The order of worlds influences which tactics and lemmas will be unlocked in a given level.
+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, lemma, or definition (all called items here) that is introduced in the game
+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
@@ -194,7 +197,7 @@ There will be features added to get automatic information from mathlib!
 
 Inside the doc comment you don't need to escape the backslashes:
 
-```
+```lean
 /-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
 Statement ...
 ```
@@ -203,11 +206,17 @@ However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclu
 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
 
@@ -217,7 +226,7 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
 
 1.  **Install Docker and Dev Containers** *(once)*:<br/>
     See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
-    Explicitely this means:
+    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
@@ -244,29 +253,30 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
   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
-  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  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):
-```
-git clone git@github.com:hhu-adam/NNG4.git
+```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
@@ -274,21 +284,23 @@ lake build
 ```
 
 Clone the game repository into a directory next to the game:
-```
+```bash
 cd ..
-git clone git@github.com:leanprover-community/lean4game.git
+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
 ```
 
+TODO: This is outdated!
 If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/server/index.mjs`:
-```
+code at the beginning of `lean4game/relay/index.mjs`:
+```typescript
 const games = {
     "g/hhu-adam/robo": {
         dir: "../../../../Robo",
@@ -302,7 +314,7 @@ const games = {
 ```
 
 Run the game:
-```
+```bash
 npm start
 ```
 
@@ -314,7 +326,7 @@ and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
 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

doc/create_game.md

@@ -0,0 +1,270 @@
+# Creating a new game
+
+This tutorial walks you through creating a new game for lean4. It covers from writing new levels, over testing the game locally, to publishing the game online.
+
+## 1. Create the project
+
+1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
+2. Clone the game repo.
+3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
+
+Note that you need to host your game's code on github to publish it online later on. If you only
+want to play it locally, you can simply clone the NNG repo and start modifying that one.
+
+
+## 2. Game.lean
+
+The file `Game.lean` is the backbone of the game putting everything together.
+
+1. `MakeGame`: This command is where the game gets built. If there are things to fix, they will be shown here as warnings or errors (orange/red squigglies in VSCode). Note that you might have to call "Lean: Restart File" (Ctrl+Shift+X) to reload the file and see changes made in other files.
+1. `Title`: Set the display title of your game.
+1. `Introduction`: This is the text displayed at the beginning next to the world selection tree.
+1. `Info`: This will be displayed in the game's menu as "Game Info". Use it for credits, funding and other meta information about the game.
+1. Imports: The file needs to import all world files, which we look at in a second. If you add a new world, remember to import it here!
+1. `Dependency`: (optional) This command adds another edge in the world tree. The game computes them automatically based on used tactics/theorems. However, sometimes you need a dependency the game can't compute, for example you explained `≠` in one world and in another world, the user is expected to know it already. The syntax is `Dependency World₁ → World₂ → World₃`.
+
+So the `Game.lean` has the following structure:
+
+```lean
+import GameServer.Commands
+
+-- import all worlds
+import Game.Levels.Tutorial
+
+Title "My Game"
+
+Introduction "
+Hi, nice you're here! Click on a world to start.
+"
+
+Info "
+This game has been developed by me.
+"
+
+-- Dependency World₁ → World₂ -- because of `≠`
+
+MakeGame
+```
+
+## 3. Creating a Level
+
+In this tutorial we first learn about Levels. A game consists of a tree of worlds, each world has
+a number of levels, enumerated 1 to n. Here we create level 1 of a world `MyWorld`. We add this world to the game in the next section.
+
+A minimal level file looks like the following. There are many options to add, which we will dive
+into in a later section
+
+```lean
+import GameServer.Commands
+
+World "MyWorld"
+Level 1
+Title "Hello World"
+
+Introduction "
+A message shown at the beginning of the level. Use it to explain any new concepts.
+"
+
+/-- The exercise statement in natural language using latex: $\iff$. -/
+Statement (n : Nat) : 0 + n = n := by
+  sorry
+
+Conclusion "
+The message shown when the level is completed
+"
+```
+
+1. Create a folder `Game/Levels/MyWorld`
+1. Create a file `Game/Levels/MyWorld/L01_hello.lean`
+1. Copy the above inside your first level.
+
+## 4. Creating a World
+
+Now we create a world. For that we create a file `MyWorld.lean` that imports all levels of this world:
+
+```lean
+import Game.Levels.MyWorld.L01_hello
+
+World "MyWorld"
+Title "My First World"
+
+Introduction
+"
+This introduction text is shown when one first enters a world.
+"
+```
+
+1. Create a file `Game/Levels/MyWorld.lean`
+1. Use the template above and make sure you import all levels of this world.
+1. In `Game.lean` import the world with `import Game.Levels.MyWorld`
+
+Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
+
+```text
+No world introducing sorry, but required by MyWorld
+```
+
+which means that the world `MyWorld` uses the tactic `sorry` in a proof, but `sorry` has not been
+introduced anywhere.
+
+## 5. Testing the Game Locally
+
+Now it's time to test the game locally and play it.
+
+There are multiple ways how you can start the game locally to test-play it described at [How to Run the Game Locally](running_locally.md). If you have problems getting one of the setups to work, please get in contact!
+
+
+## 6. Dive into Level creation
+
+Now that you have a running game, we have a closer look at the level files and all the options
+you have to design your game.
+
+### 6. a) Inventory
+
+The player has an inventory with tactics, theorems, and definitions that unlock during the game. You can unlock/introduce such items in a Level by adding one of the following below the `Statement`.
+
+```lean
+NewTactic induction simp
+NewLemma Nat.zero_mul
+NewDefinition Pow
+```
+
+#### 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.
+
+```lean
+LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
+"some description"
+
+TacticDoc simp
+"some description"
+
+DefinitionDoc Pow as "^"
+"some description"
+```
+
+(e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
+
+If you do not provide any content for the inventory, the game will try to find a docstring of that item and display that docstring.
+
+#### Inventory management
+
+You have a few options to disable inventory items that have been unlocked in previous levels:
+
+```lean
+DisableTactic, DisableLemma, OnlyTactic, OnlyLemma
+```
+
+have the same syntax as above. The former two disable items for this level, the latter two
+disable all items except the ones specified.
+
+#### Theorem Tab
+
+Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
+
+#### HiddenTactic
+
+`NewHiddenTactic` lets you add a tactic without adding it to the inventory. This can be useful for variants of tactics. E.g. you could do
+
+```lean
+NewTactic rw
+NewHiddenTactic rewrite nth_rewrite rwa
+```
+
+and only `rw` would show up in the inventory.
+
+### 6. b) Statement
+
+The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
+
+#### Name
+
+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.
+
+#### 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.
+
+```lean
+/-- The exercise statement in natural language using latex: $\iff$. -/
+Statement ...
+  sorry
+```
+
+#### Attributes
+
+You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
+
+```lean
+@[simp]
+Statement my_simp_lemma ...
+```
+
+### 6. c) 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.
+
+One thing to keep in mind is that the game will look at the main proof to figure out which tactics and theorems are needed, but it ignores any `Branch`es.
+
+### 6. d) Hints
+
+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.
+
+Read [More about Hints](doc/hints.md) for how they work and what the options are.
+
+### 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.
+
+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).
+
+NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
+
+## 7. Update your game
+
+In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
+
+## 8. Publish your game
+
+To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
+
+There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
+
+```lean
+Languages "English"
+CaptionShort "Game Template"
+CaptionLong "You should use this game as a template for your own game and add your own levels."
+Prerequisites "NNG"
+CoverImage "images/cover.png"
+```
+* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
+* `CaptionShort`: One catch phrase. Appears above the image.
+* `CaptionLong`: 2-4 sentences to describe the game.
+* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
+* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
+
+## Further Notes
+
+Here are some random further things you should consider designing a new game:
+
+* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
+  would write `Introduction "some latex here: $\\iff$."` but
+  `/-- some latex here: $\iff$. -/ Statement ...`
+* 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 starts getting out
+  of control.

doc/hints.md

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

doc/npm_scripts.md

@@ -0,0 +1,9 @@
+## NPM Scripts
+
+* `npm start`: Start the project in development mode. The browser will automatically reload when client files get changed. The Lean server will get recompiled and restarted when lean files get changed. The Lean server will be started without a container. The client and server can be started separately using the scripts `npm run start_client` and `npm run start_server`. The project can be accessed via `http://localhost:3000`.
+Internally, websocket requests to `ws://localhost:3000/websockets` will be forwarded to a Lean server running on port `8080`.
+
+* `npm run build`: Build the project in production mode. All assets of the client will be compiled into `client/dist`.
+On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
+
+* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specific port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.

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

@@ -0,0 +1,123 @@
+# Running Games Locally
+
+The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
+
+There are several options to play a game locally:
+
+1. VSCode Dev Container: needs `docker` installed on your machine
+2. Codespaces: Needs active internet connection and computing time is limited.
+3. Gitpod: does not work yet (Is that true?)
+4. Manual installation: Needs `npm` installed on your system
+
+The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup.
+
+The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) contains all the relevant files to make your local setup (dev container / gitpod / codespaces) work. You might need to update these files manually by copying them from there if you need any new improvements to the dev setup you're using in an existing game.
+
+## VSCode Dev Containers
+
+1.  **Install Docker and Dev Containers** *(once)*:<br/>
+    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). (Alternatively install it from the VSCode extensions).
+
+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-15 minutes. After the first
+      start this should be very quickly.
+    * Once built, you can open http://localhost:3000 in your browser. which should load the game.
+
+3.  **Editing Files** *(everytime)*:<br/>
+    After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
+
+### 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
+  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  container. (this will again take some time)
+* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
+
+## Codespaces
+
+You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
+
+Note: You have to wait until npm started properly, which might take a good while.
+
+As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
+
+## Gitpod
+
+TODO: Not sure this works yet!
+
+Open the game clicking on the gitpod link. Again you will need to wait until it is fully built and then enter `lake build` in the shell whenever you made changes.
+
+## Manual installation
+
+This installs the `lean4game` manually on your computer. (It is the same installation as one would
+use to setup a proper server online, only the run command (i.e. `npm start`) is different.)
+
+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. `GameSkeleton` here):
+```bash
+git clone https://github.com/hhu-adam/GameSkeleton.git
+# or: git clone git@github.com:hhu-adam/GameSkeleton.git
+```
+
+Download dependencies and build the game:
+```bash
+cd GameSkeleton
+lake update -R
+lake build
+```
+
+Clone the server repository into a directory next to the game:
+```bash
+cd ..
+git clone https://github.com/leanprover-community/lean4game.git
+# or: git clone git@github.com:leanprover-community/lean4game.git
+```
+The folders `GameSkeleton` and `lean4game` must be in the same directory!
+
+In `lean4game`, install dependencies:
+```bash
+cd lean4game
+npm install
+```
+
+Run the game:
+```bash
+npm start
+```
+
+This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.
+
+## Modifying the GameServer
+
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`:
+
+```bash
+cd NNG4
+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, you can the local copy of the edit `GameServer` in `../lean4game` and
+`lake build` will then directly use this modified copy to build your game.

doc/server.md

@@ -0,0 +1,28 @@
+
+# Notes for Server maintainer
+
+In order to set up the server to allow imports, one needs to create a
+[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public
+repos will suffice.
+
+You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
+with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if
+you're using `pm2`
+
+Then people can call:
+
+> https://{website}/import/trigger/{owner}/{repo}
+
+where you replace:
+- website: The website your server runs on, e.g. `localhost:3000`
+- owner, repo: The owner and repository name of the game you want to load from github.
+
+ will trigger to download the latest version of your game from github onto your server.
+ Once this import reports "Done", you should be able to play your game under:
+
+> https://{website}/#/g/{owner}/{repo}
+
+## data management
+Everything downloaded remains in the folder `lean4game/games`.
+the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
+The other folders should only contain the built lean-games, sorted by owner and repo.

doc/update_game.md

@@ -0,0 +1,52 @@
+# How to update your Game
+
+## New Lean version
+
+You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the
+new lean version `leanprover/lean4:v4.X.0`.
+
+Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags).
+
+Then, depending on the setup you use, do one of the following:
+
+* Dev Container: Rebuild the VSCode Devcontainer.
+* Local Setup: in your game's folder run the following:
+  ```
+  lake update -R
+  lake build
+  ```
+
+  * Additionally, if you have a local copy of the server `lean4game`,
+    you should update this one to the matching version. Run the following in the folder `lean4game/`:
+    ```
+    git fetch
+    git checkout {VERSION_TAG}
+    npm install
+    ```
+    where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
+* Gitpod/Codespaces: Create a fresh one
+
+This will update your game (and the mathlib version you might be using) to the new lean version.
+
+## Newest developing setup
+
+There are a few files in your game repository which are used for the developing setup
+(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
+anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
+
+The relevant files are:
+
+```
+.devcontainer/
+.docker/
+.github/
+.gitpod/
+.vscode/
+lakefile.lean
+```
+
+simply copy them from the `GameSkeleton` into your game and proceed as above,
+i.e. `lake update -R && lake build`.
+
+(Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
+where you need to add any dependencies of your game, or remove mathlib if you don't need it.)

ecosystem.config.cjs

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

env.d.ts

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

index.html

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

package.json

@@ -1,9 +1,11 @@
 {
   "name": "lean4-game",
   "version": "0.1.0",
+  "type": "module",
   "private": true,
   "homepage": ".",
   "dependencies": {
+    "@babel/plugin-transform-optional-chaining": "^7.23.0",
     "@emotion/react": "^11.10.5",
     "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",
@@ -14,6 +16,7 @@
     "@reduxjs/toolkit": "^1.9.1",
     "@types/cytoscape": "^3.19.9",
     "@types/react-router-dom": "^5.3.3",
+    "@vitejs/plugin-react-swc": "^3.4.0",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",
@@ -34,45 +37,39 @@
     "rehype-katex": "^6.0.2",
     "remark-gfm": "^3.0.1",
     "remark-math": "^5.1.1",
+    "request": "^2.88.2",
     "request-progress": "^3.0.0",
+    "vite": "^4.5.0",
+    "vite-plugin-static-copy": "^0.17.0",
+    "vite-plugin-svgr": "^4.1.0",
     "vscode-ws-jsonrpc": "^2.0.1",
     "web-worker": "^1.2.0",
     "ws": "^8.11.0"
   },
   "devDependencies": {
-    "@babel/cli": "^7.19.3",
-    "@babel/core": "^7.20.5",
-    "@babel/preset-env": "^7.20.2",
-    "@babel/preset-react": "^7.18.6",
-    "@babel/preset-typescript": "^7.18.6",
     "@pmmmwh/react-refresh-webpack-plugin": "^0.5.10",
     "@redux-devtools/core": "^3.13.1",
     "@testing-library/react": "^13.4.0",
     "@types/debounce": "^1.2.1",
-    "babel-loader": "^8.3.0",
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",
     "file-loader": "^6.2.0",
-    "nodemon": "^2.0.20",
+    "nodemon": "^3.0.1",
     "react-refresh": "^0.14.0",
     "style-loader": "^3.3.1",
     "ts-loader": "^9.4.2",
     "typescript": "^4.9.4",
-    "url-loader": "^4.1.1",
-    "webpack": "^5.75.0",
-    "webpack-cli": "^4.10.0",
-    "webpack-dev-server": "^4.11.1",
-    "webpack-shell-plugin-next": "^2.3.1"
+    "url-loader": "^4.1.1"
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "cd server && lake build && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
-    "start_client": "cross-env NODE_ENV=development webpack-dev-server --hot",
-    "build": "cross-env NODE_ENV=production webpack",
-    "production": "cross-env NODE_ENV=production node server/index.mjs",
-    "build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag g/hhu-adam/robo && rm -rf ./Robo",
-    "build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag g/hhu-adam/nng4 && rm -rf ./NNG4",
-    "update_lean": "./UPDATE_LEAN.sh"
+    "start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")",
+    "start_client": "cross-env NODE_ENV=development vite --host",
+    "build": "npm run build_server && npm run build_client",
+    "preview": "vite preview",
+    "build_server": "cd server && lake build",
+    "build_client": "cross-env NODE_ENV=production vite build",
+    "production": "cross-env NODE_ENV=production node relay/index.mjs"
   },
   "eslintConfig": {
     "extends": [

relay/bubblewrap.sh

@@ -2,11 +2,15 @@
 
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
+# $1 : the game directory
+# $2 : the lean4game folder
+# $3 : the gameserver executable
+
 (exec bwrap\
-  --ro-bind ../../lean4game /lean4game \
-  --ro-bind ../../$1 /game \
-  --ro-bind $ELAN_HOME /elan \
-  --ro-bind /usr /usr \
+  --bind $2 /lean4game \
+  --bind $1 /game \
+  --bind $ELAN_HOME /elan \
+  --bind /usr /usr \
   --dev /dev \
   --proc /proc \
   --symlink usr/lib /lib\
@@ -22,6 +26,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
   --unshare-uts  \
   --unshare-cgroup \
   --die-with-parent \
-  --chdir "/lean4game/server/build/bin/" \
+  --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
   ./gameserver --server /game
 )

relay/import.mjs

@@ -11,6 +11,7 @@ const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
+const USERNAME = process.env.LEAN4GAME_GITHUB_USER
 const octokit = new Octokit({
   auth: TOKEN
 })
@@ -41,9 +42,10 @@ async function download(id, url, dest) {
     requestProgress(request({
       url,
       headers: {
-        'User-Agent': 'abentkamp',
+        'accept': 'application/vnd.github+json',
+        'User-Agent': USERNAME,
         'X-GitHub-Api-Version': '2022-11-28',
-        'Authorization': 'Bearer '+TOKEN
+        'Authorization': 'Bearer ' + TOKEN
       }
     }))
     .on('progress', function (state) {
@@ -76,35 +78,44 @@ async function doImport (owner, repo, id) {
       .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc)
     artifactId = artifact.id
     const url = artifact.archive_download_url
-    if (!fs.existsSync("tmp")){
-      fs.mkdirSync("tmp");
+    // Make sure the download folder exists
+    if (!fs.existsSync(path.join(__dirname, "..", "games"))){
+      fs.mkdirSync(path.join(__dirname, "..", "games"));
+    }
+    if (!fs.existsSync(path.join(__dirname, "..", "games", "tmp"))){
+      fs.mkdirSync(path.join(__dirname, "..", "games", "tmp"));
     }
     progress[id].output += `Download from ${url}\n`
-    await download(id, url, `tmp/artifact_${artifactId}.zip`)
+    await download(id, url, path.join(__dirname, "..", "games", "tmp", `${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`))
     progress[id].output += `Download finished.\n`
-    await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId],".")
-    let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
-    manifest = JSON.parse(manifest);
-    if (manifest.length !== 1) {
-      throw `Unexpected manifest: ${JSON.stringify(manifest)}`
-    }
-    manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
-    fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
-    await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
-    await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
+
+    await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, ".."))
+
+
+    // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
+    // manifest = JSON.parse(manifest);
+    // if (manifest.length !== 1) {
+    //   throw `Unexpected manifest: ${JSON.stringify(manifest)}`
+    // }
+    // manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
+    // fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
+    // await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
+    // // await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
+
     progress[id].done = true
-    progress[id].output += `Done.\n`
+    progress[id].output += `Done!\n`
+    progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n`
   } catch (e) {
     progress[id].output += `Error: ${e.toString()}\n${e.stack}`
   } finally {
+    // clean-up temp. files
     if (artifactId) {
-      fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true});
-      fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true});
-      fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true});
-      fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true});
+      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}.zip`), {force: true, recursive: false});
+      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}`), {force: true, recursive: true});
     }
     progress[id].done = true
   }
+  await new Promise(resolve => setTimeout(resolve, 10000))
 }
 
 export const importTrigger = (req, res) => {

relay/index.mjs

@@ -0,0 +1,203 @@
+import { WebSocketServer } from 'ws';
+import express from 'express'
+import path from 'path'
+import * as cp from 'child_process';
+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 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 queueLength = {
+  "g/hhu-adam/robo": 2,
+  "g/hhu-adam/nng4": 5,
+  "g/djvelleman/stg4": 2,
+}
+
+const __filename = url.fileURLToPath(import.meta.url);
+const __dirname = url.fileURLToPath(new URL('.', import.meta.url));
+
+const app = express()
+
+const PORT = process.env.PORT || 8080;
+
+var router = express.Router();
+
+router.get('/import/status/:owner/:repo', importStatus)
+router.get('/import/trigger/:owner/:repo', importTrigger)
+
+const server = app
+  .use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
+  .use('/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}`));
+
+const wss = new WebSocketServer({ server })
+
+var socketCounter = 0
+
+const environment = process.env.NODE_ENV
+const isDevelopment = environment === 'development'
+
+/** We keep queues of started Lean Server processes to be ready when a user arrives */
+const queue = {}
+
+function getTag(owner, repo) {
+  return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
+}
+
+function getGameDir(owner, repo) {
+  owner = owner.toLowerCase()
+  if (owner == 'local') {
+    if(!isDevelopment) {
+      console.error(`No local games in production mode.`)
+      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 ""
+    }
+  }
+
+  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", 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, path.join(__dirname, '..')],
+      { cwd: __dirname })
+  }
+
+  serverProcess.on('error', error =>
+    console.error(`Launching Lean Server failed: ${error}`)
+  )
+  if (serverProcess.stderr !== null) {
+    serverProcess.stderr.on('data', data =>
+      console.error(`Lean Server: ${data}`)
+    )
+  }
+  return serverProcess
+}
+
+/** start Lean Server processes to refill the queue */
+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 queueLength) {
+//     queue[tag] = []
+//     fillQueue(tag)
+//   }
+// }
+
+const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
+
+wss.addListener("connection", function(ws, req) {
+    const reRes = urlRegEx.exec(req.url)
+    if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
+    const owner = reRes[1]
+    const repo = reRes[2]
+
+    const tag = getTag(owner, repo)
+
+    let ps
+    if (!queue[tag] || queue[tag].length == 0) {
+      ps = startServerProcess(owner, repo)
+    } else {
+        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;
+    const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
+    console.log(`[${new Date()}] Socket opened - ${ip}`)
+
+    const socket = {
+        onMessage: (cb) => { ws.on("message", cb) },
+        onError: (cb) => { ws.on("error", cb) },
+        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 socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
+    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;
+    });
+
+    console.log(`[${new Date()}] Number of open sockets - ${socketCounter}`)
+    console.log(`[${new Date()}] Free RAM - ${Math.round(os.freemem() / 1024 / 1024)} / ${Math.round(os.totalmem() / 1024 / 1024)} MB`)
+
+    ws.on('close', () => {
+      console.log(`[${new Date()}] Socket closed - ${ip}`)
+      socketCounter -= 1
+    })
+
+    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,9 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
+import GameServer.Commands
+
+-- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
+-- should we have a different solution?
 
 unsafe def main : List String → IO UInt32 := fun args => do
   let e ← IO.getStderr

server/GameServer/AbstractCtx.lean

@@ -1,4 +1,5 @@
 import Lean
+import GameServer.Utils
 
 section AbstractCtx
 open Lean

server/GameServer/Commands.lean

@@ -1,15 +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."
-}
-
 /-! # Game metadata -/
 
 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -38,31 +35,92 @@ 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
 
@@ -72,46 +130,6 @@ in the first level and get enabled during the game.
 
 /-! ## Doc entries -/
 
-/-- 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 =>
-      -- We just add a dummy entry
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else "" })
-      logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
-        m!"somewhere above this statement.")
-    -- 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:
 
 ```
@@ -121,12 +139,13 @@ 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:
 
@@ -140,16 +159,18 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 * The identifier after `in` is the category to group lemmas 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 requries
+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.
  -/
-elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
+elab doc:docComment ? "LemmaDoc" 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
 -- it but display the info that it wasn't found in `Statement`
@@ -168,58 +189,30 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The string following `as` is the displayed name (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 requries
+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.
  -/
-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 -/
 
--- namespace Lean.PrettyPrinter
--- def ppSignature' (c : Name) : MetaM String := do
---   let decl ← getConstInfo c
---   let e := .const c (decl.levelParams.map mkLevelParam)
---   let (stx, _) ← delabCore e (delab := Delaborator.delabConstWithSignature)
---   let f ← ppTerm stx
---   return toString f
--- end Lean.PrettyPrinter
-
-def getStatement (name : Name) : CommandElabM MessageData := do
-  -- let c := name.getId
-
-  let decl ← getConstInfo name
-  -- -- TODO: How to go between CommandElabM and MetaM
-
-  -- addCompletionInfo <| .id name c (danglingDot := false) {} none
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| ppExpr decl.type
-    -- PrettyPrinter.ppSignature' c
-    -- PrettyPrinter.ppSignature c
-    | 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`. -/
-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.
-
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
-  for name in ↑args do checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
+  for name in ↑args do
+    checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId)}}
 
-/-- Declare tactics that are introduced by this level. -/
+/-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
+  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)}}
@@ -227,6 +220,8 @@ elab "NewHiddenTactic" args:ident* : command => do
 /-- Declare lemmas that are introduced by this level. -/
 elab "NewLemma" args:ident* : command => do
   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)}}
@@ -283,54 +278,12 @@ elab "LemmaTab"  category:str : command =>
 
 /-! # 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 := {} })
@@ -409,13 +362,11 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   -- the namespace?
   let currNamespace ← getCurrNamespace
 
-  let st ← match statementName with
-  | some name => getStatementString <| currNamespace ++ name.getId
-  | none =>  getStatementString <| currNamespace ++ (defaultDeclName).getId
-
-  let head := match statementName with
-  | some name => Format.join ["theorem ", (currNamespace ++ name.getId).toString]
-  | none => "example"
+  -- Format theorem statement for displaying
+  let sigString := sig.raw.reprint.getD ""
+  let descrFormat : String := match statementName with
+  | some name =>  s!"theorem {name.getId} {sigString} := by"
+  | none => s!"example {sigString} := by"
 
   modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
@@ -425,7 +376,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     statementName := match statementName with
     | none => default
     | some name => currNamespace ++ name.getId
-    descrFormat := (Format.join [head, " ", st, " := by"]).pretty 10
+    descrFormat := descrFormat
     hints := hints
     tactics := {level.tactics with used := usedInventory.tactics.toArray}
     definitions := {level.definitions with used := usedInventory.definitions.toArray}
@@ -433,23 +384,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.
 -/
@@ -457,7 +391,7 @@ elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(t
   let mut strict := false
   let mut hidden := false
 
-  -- remove spaces at the beginngng of new lines
+  -- remove spaces at the beginning of new lines
   let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
     match m with
     | Syntax.node info k args =>
@@ -511,9 +445,9 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
   -- Show an info whether the branch proofs all remaining goals.
   let gs ← Tactic.getUnsolvedGoals
   if gs.isEmpty then
-    logInfo "This branch finishes the proof."
+    trace[debug] "This branch finishes the proof."
   else
-    logInfo "This branch leaves open goals."
+    trace[debug] "This branch leaves open goals."
 
   let msgs ← Core.getMessageLog
   b.restore
@@ -525,7 +459,7 @@ elab (name := GameServer.Tactic.Hole) "Hole" t:tacticSeq : tactic => do
 
 /--
 Iterate recursively through the Syntax, replace `Hole` with `sorry` and remove all
-`Hint`/`Branch` occurences.
+`Hint`/`Branch` occurrences.
 -/
 def replaceHoles (tacs : Syntax) : Syntax :=
   match tacs with
@@ -539,7 +473,7 @@ where filterArgs (args : List Syntax) : List Syntax :=
     -- replace `Hole` with `sorry`.
     | Syntax.node info `GameServer.Tactic.Hole _ :: r =>
       Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
-    -- delete all `Hint` and `Branch` occurences in the middle.
+    -- delete all `Hint` and `Branch` occurrences in the middle.
     | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
     | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
       filterArgs r
@@ -558,10 +492,11 @@ elab "Template" tacs:tacticSeq : tactic => do
   Tactic.evalTactic tacs
   let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨replaceHoles tacs.raw⟩
   let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
-  logInfo s!"Template:\n{template}"
+  trace[debug] s!"Template:\n{template}"
   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
@@ -580,157 +515,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}}
-
-/-- 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
-
-
-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₃`. -/
@@ -805,8 +589,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
@@ -845,9 +633,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
@@ -859,7 +650,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
@@ -910,14 +701,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
 
@@ -1047,18 +849,6 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
+    allItemsByType := allItemsByType.insert inventoryType allItems
 
-
-/-! # Debugging tools -/
-
--- /-- 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

server/GameServer/EnvExtensions.lean

@@ -67,7 +67,7 @@ structure InventoryTemplate where
   /-- Depends on the type:
   * Tactic: the tactic's name
   * Lemma: fully qualified lemma name
-  * Definition: no restrictions (preferrably the definions fully qualified name)
+  * Definition: no restrictions (preferably the definitions fully qualified name)
   -/
   name: Name
   /-- Only for Lemmas. To sort them into tabs -/
@@ -108,6 +108,12 @@ structure InventoryTile where
   hidden := false
 deriving ToJson, FromJson, Repr, Inhabited
 
+def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
+      name := item.name,
+      displayName := item.displayName
+      category := item.category
+}
+
 /-- The extension that stores the doc templates. Note that you can only add, but never modify
 entries! -/
 initialize inventoryTemplateExt :
@@ -135,7 +141,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 +271,61 @@ 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
+  displayName : Option String
+  statementName : Option String
+  template : Option String
+  image: Option String
+deriving ToJson, FromJson
+
+def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
+  { index := lvl.index,
+    title := lvl.title,
+    tactics := lvl.tactics.tiles,
+    lemmas := lvl.lemmas.tiles,
+    definitions := lvl.definitions.tiles,
+    descrText := lvl.descrText,
+    descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
+    introduction := lvl.introduction
+    conclusion := lvl.conclusion
+    lemmaTab := match lvl.lemmaTab with
+    | some tab => tab
+    | none =>
+      -- Try to set the lemma tab to the category of the first added lemma
+      match lvl.lemmas.tiles.find? (·.new) with
+      | some tile => tile.category
+      | none => none
+    statementName := lvl.statementName.toString
+    displayName := match lvl.statementName with
+      | .anonymous => none
+      | name => match (inventoryExt.getState env).find?
+          (fun x => x.name == name && x.type == .Lemma) with
+        | some n => n.displayName
+        | none => name.toString
+        -- Note: we could call `.find!` because we check in `Statement` that the
+        -- lemma doc must exist.
+    template := lvl.template
+    image := lvl.image
+  }
 
 /-! ## World -/
 
@@ -271,17 +341,46 @@ structure World where
   conclusion : String := default
   /-- The levels of the world. -/
   levels: HashMap Nat GameLevel := default
+  /-- The introduction image of the world. -/
+  image: String := default
 deriving Inhabited
 
 instance : ToJson World := ⟨
   fun world => Json.mkObj [
     ("name", toJson world.name),
     ("title", world.title),
-    ("introduction", world.introduction)]
+    ("introduction", world.introduction),
+    ("image", world.image)]
 ⟩
 
 /-! ## Game -/
 
+/-- A tile as they are displayed on the servers landing page. -/
+structure GameTile where
+  /-- The title of the game -/
+  title: String
+  /-- One catch phrase about the game -/
+  short: String := default
+  /-- One paragraph description what the game is about -/
+  long: String := default
+  /-- List of languages the game supports
+
+  TODO: What's the expectected format
+  TODO: Must be a list with a single language currently
+   -/
+  languages: List String := default
+  /-- A list of games which this one builds upon -/
+  prerequisites: List String := default
+  /-- Number of worlds in the game -/
+  worlds: Nat := default
+  /-- Number of levels in the game -/
+  levels: Nat := default
+  /-- A cover image of the game
+
+  TODO: What's the format? -/
+  image: String := default
+deriving Inhabited, ToJson
+
 structure Game where
   /-- Internal name of the game. -/
   name : Name
@@ -296,8 +395,19 @@ structure Game where
   /-- TODO: currently unused. -/
   authors : List String := default
   worlds : Graph Name World := default
+  /-- The tile displayed on the server's landing page. -/
+  tile : GameTile := default
+  /-- The path to the background image of the world. -/
+  image : String := default
 deriving Inhabited, ToJson
 
+def getGameJson (game : «Game») : Json := Id.run do
+  let gameJson : Json := toJson game
+  -- Add world sizes to Json object
+  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
+  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
+  return gameJson
+
 /-! ## Game environment extension -/
 
 def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :
@@ -386,6 +496,11 @@ def modifyCurWorld (fn : World → m World) [MonadError m] : m Unit := do
     return {game with worlds := {game.worlds with nodes := game.worlds.nodes.insert world.name (← fn world) }}
 
 def addLevel (level : GameLevel) [MonadError m] : m Unit := do
+  let worldId ← getCurWorldId
+  match ← getLevel? ⟨← getCurGameId, worldId, level.index⟩ with
+  | some _existingLevel =>
+    throwError m!"Level {level.index} already exists for world {worldId}!"
+  | none =>
     modifyCurWorld fun world => do
       return {world with levels := world.levels.insert level.index level}
 

server/GameServer/FileWorker.lean

@@ -1,6 +1,7 @@
 /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
+import GameServer.ImportModules
 
 namespace MyModule
 open Lean
@@ -57,6 +58,17 @@ open JsonRpc
 
 section Elab
 
+def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
+    Elab.Command.CommandElabM Unit := do
+  modify fun st => { st with
+      messages := st.messages.add {
+        fileName := inputCtx.fileName
+        severity := MessageSeverity.error
+        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+        data     := s
+      }
+    }
+
 -- TODO: use HashSet for allowed tactics?
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
@@ -65,7 +77,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
     Elab.Command.CommandElabM Unit := do
   match stx with
   | .missing => return ()
-  | .node info kind args =>
+  | .node _info _kind args =>
     for arg in args do
       findForbiddenTactics inputCtx levelParams arg
   | .atom info val =>
@@ -89,13 +101,17 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           | some _ => pure () -- tactic is in the inventory, allow it.
         else if tac.disabled then
           addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
-  | .ident info rawVal val preresolved =>
+  | .ident info _rawVal val _preresolved =>
       let ns ←
         try resolveGlobalConst (mkIdent val)
         catch | _ => pure [] -- catch "unknown constant" error
       for n in ns do
         let some (.thmInfo ..) := (← getEnv).find? n
-          | return () -- not a theroem -> ignore
+          | return () -- not a theorem -> ignore
+        -- Forbid the theorem we are proving currently
+        if n = levelParams.statementName then
+          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+
         let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
         match lemmasAndDefs.find? (fun l => l.name == n) with
         | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
@@ -105,14 +121,19 @@ 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
+  if difficulty > 0 then
     modify fun st => { st with
       messages := st.messages.add {
         fileName := inputCtx.fileName
-      severity := MessageSeverity.warning
+        severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning
         pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
         data     := s
       }
     }
+  else pure ()
+-- where addErrorMessage (info : SourceInfo) (s : MessageData) :=
+--   pure ()
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
@@ -170,7 +191,6 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          if levelParams.checkEnabled then
           findForbiddenTactics inputCtx levelParams tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
@@ -273,7 +293,7 @@ where
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
     /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while prefering newer versions over old ones. The former is necessary because we do
+      while preferring newer versions over old ones. The former is necessary because we do
       not explicitly clear older diagnostics, while the latter is necessary because we do
       not guarantee that diagnostics are emitted in order. Specifically, it may happen that
       we interrupted this elaboration task right at this point and a newer elaboration task
@@ -281,7 +301,7 @@ where
       the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
       because we cannot guarantee that no further diagnostics are emitted after clearing
       them. -/
-    -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
+    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
     -- because empty diagnostics clear existing error/information squiggles. Therefore we always
     -- want to publish in case there was previously a message at this position.
     publishDiagnostics m snap.diagnostics.toArray ctx.hOut
@@ -393,7 +413,7 @@ section Initialization
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules [{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
+    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
     -- return (env, paths)
 
     -- use empty header
@@ -477,7 +497,7 @@ section NotificationHandling
       IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
     else if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
 
@@ -533,7 +553,7 @@ section MainLoop
 
       set {s with levelParams := {s.levelParams with
         inventory := p.inventory,
-        checkEnabled := p.checkEnabled}}
+        difficulty := p.difficulty}}
       mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
@@ -554,7 +574,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
     This is because LSP always refers to characters by (line, column),
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try

server/GameServer/Game.lean

@@ -7,7 +7,7 @@ structure GameServerState :=
 (game : Name)
 (gameDir : String)
 (inventory : Array String)
-(checkEnabled : Bool)
+(difficulty : Nat)
 
 abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
 
@@ -25,52 +25,6 @@ open Lsp
 open JsonRpc
 open IO
 
-def getGame (game : Name): GameServerM Json := do
-  let some game ← getGame? game
-    | throwServerError "Game not found"
-  let gameJson : Json := toJson game
-  -- Add world sizes to Json object
-  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
-  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
-  return gameJson
-
-/--
-Fields:
-- description: Lemma in mathematical language.
-- descriptionGoal: Lemma printed as Lean-Code.
--/
-structure LevelInfo where
-  index : Nat
-  title : String
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  introduction : String
-  conclusion : String
-  descrText : Option String := none
-  descrFormat : String := ""
-  lemmaTab : Option String
-  statementName : Option String
-  template : Option String
-deriving ToJson, FromJson
-
-structure InventoryOverview where
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  lemmaTab : Option String
-deriving ToJson, FromJson
-
-structure LoadLevelParams where
-  world : Name
-  level : Nat
-  deriving ToJson, FromJson
-
--- structure LoadTemplateParams where
---   world : Name
---   level : Nat
---   deriving ToJson, FromJson
-
 structure DidOpenLevelParams where
   uri : String
   gameDir : String
@@ -79,18 +33,20 @@ structure DidOpenLevelParams where
   lemmas : Array InventoryTile
   definitions : Array InventoryTile
   inventory : Array String
-  /-- if true the server gives warnings for used tactics/lemmas that are not unlocked. -/
-  checkEnabled : Bool
+  /--
+  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
 
-structure LoadDocParams where
-  name : Name
-  type : InventoryType
-deriving ToJson, FromJson
-
 structure SetInventoryParams where
   inventory : Array String
-  checkEnabled : Bool
+  difficulty : Nat
 deriving ToJson, FromJson
 
 def handleDidOpenLevel (params : Json) : GameServerM Unit := do
@@ -117,125 +73,26 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
       lemmas := lvl.lemmas.tiles
       definitions := lvl.definitions.tiles
       inventory := s.inventory
-      checkEnabled := s.checkEnabled
+      difficulty := s.difficulty
+      statementName := lvl.statementName
       : DidOpenLevelParams
     }
   }
 
-
 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 := 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 s ← get
-      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, checkEnabled := p.checkEnabled}
+      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
 

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

@@ -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,65 @@
+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
+
+
+-- TODO: I'm not sure this should be happening here...
+#eval IO.FS.createDirAll ".lake/gamedata/"
+
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
+  let game ← getCurGame
+  let env ← getEnv
+  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+
+  if ← path.isDir then
+    IO.FS.removeDirAll path
+  IO.FS.createDirAll path
+
+  -- copy the images folder
+  copyImages
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    for (levelId, level) in world.levels.toArray do
+      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+
+  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+
+  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
+    for name in allItemsByType.findD inventoryType {} do
+      let some item ← getInventoryItem? name inventoryType
+        | throwError "Expected item to exist: {name}"
+      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := ← getTiles .Lemma
+    tactics := ← getTiles .Tactic
+    definitions := ← getTiles .Definition
+    lemmaTab := none
+  }
+  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))

server/GameServer/Utils.lean

@@ -0,0 +1,50 @@
+import Lean
+
+open Lean Meta Elab Tactic Command
+
+syntax showOptArg := atomic(" (" (&"strict" <|> &"verbose") " := " withoutPosition(term) ")")
+
+/--
+Lists all available options that can be used with `set_option`.
+
+Use `set_option (verbose := true)` to display more than just the option names.
+The form `#show_option id` will show only options that begin with `id`.
+
+Copied from `#help option` from mathlib.
+-/
+elab "#show_option" verbose:(ppSpace showOptArg)? id:(ppSpace Parser.rawIdent)? : command => do
+  let id := id.map (·.raw.getId.toString false)
+  let mut decls : Lean.RBMap _ _ compare := {}
+  for (name, decl) in show Lean.RBMap .. from ← getOptionDecls do
+    let name := name.toString false
+    if let some id := id then
+      if !id.isPrefixOf name then
+        continue
+    decls := decls.insert name decl
+  let mut msg := Format.nil
+  let opts ← getOptions
+  if decls.isEmpty then
+    match id with
+    | some id => throwError "no options start with {id}"
+    | none => throwError "no options found (!)"
+  for (name, decl) in decls do
+    let mut msg1 := match decl.defValue with
+    | .ofString val => s!"String := {repr val}"
+    | .ofBool val => s!"Bool := {repr val}"
+    | .ofName val => s!"Name := {repr val}"
+    | .ofNat val => s!"Nat := {repr val}"
+    | .ofInt val => s!"Int := {repr val}"
+    | .ofSyntax val => s!"Syntax := {repr val}"
+    if let some val := opts.find name then
+      msg1 := s!"{msg1}  (currently: {val})"
+    msg := match verbose with
+    | some opt =>
+      match opt with
+      | `(showOptArg| (verbose := true)) =>
+        msg ++ .nest 2 (f!"option {name} : {msg1}" ++ .line ++ decl.descr) ++ .line ++ .line
+      | _ =>
+        msg ++ (f!"{name}" ++ .line )
+    | none =>
+      msg ++ (f!"{name}" ++ .line )
+
+  logInfo msg

server/GameServer/Watchdog.lean

@@ -91,7 +91,7 @@ def createEnv (gameDir : String) (module : String) : IO Environment := do
   -- Set the search path
   Lean.searchPathRef.set paths
 
-  let env ← importModules [{ module := `Init : Import }, { module := module : Import }] {} 0
+  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
@@ -114,7 +114,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
     game := gameName,
     gameDir := gameDir,
     inventory := #[]
-    checkEnabled := false
+    difficulty := 0
     }
   let initRequest ← i.readLspRequestAs "initialize" InitializeParams
   -- We misuse the `rootUri` field to the gameName

server/index.mjs

@@ -1,164 +0,0 @@
-import { WebSocketServer } from 'ws';
-import express from 'express'
-import path from 'path'
-import * as cp from 'child_process';
-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 anonymize from 'ip-anonymize';
-// import { importTrigger, importStatus } from './import.mjs'
-
-/** Preloaded games. The keys refer to the docker tags of the virtual machines.
- * The number `queueLength` determines how many instances of the docker container
- * get started before any user shows up to have them up and running immediately.
- * The values `name`, `module`, and `dir` are just used for development where we
- * use a project directory instead of a docker container.
-*/
-const games = {
-    "g/hhu-adam/robo": {
-        // module: "Game",  // The lean module's name. Defaults to "Game"
-        // name: "Adam",    // For the `Game "Adam"` tag in the games. Defaults to "MyGame"
-        dir: "Robo",
-        queueLength: 5
-    },
-    "g/hhu-adam/nng4": {
-        // module: "Game",
-        // name: "NNG",
-        dir: "NNG4",
-        queueLength: 5
-    },
-    "g/local/game": {
-        dir: "game",
-        queueLength: 0
-    }
-}
-
-const __filename = url.fileURLToPath(import.meta.url);
-const __dirname = url.fileURLToPath(new URL('.', import.meta.url));
-
-const app = express()
-
-const PORT = process.env.PORT || 8080;
-
-var router = express.Router();
-
-// 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('/', router)
-  .listen(PORT, () => console.log(`Listening on ${PORT}`));
-
-const wss = new WebSocketServer({ server })
-
-var socketCounter = 0
-
-const environment = process.env.NODE_ENV
-const isDevelopment = environment === 'development'
-
-/** We keep queues of started Lean Server processes to be ready when a user arrives */
-const queue = {}
-
-function startServerProcess(tag) {
-    if (! games[tag]?.dir) {
-        console.error(`Unknown game: ${tag}`)
-        return
-    }
-
-    let serverProcess
-    if (isDevelopment) {
-        let args = ["--server", path.join("../../../../", games[tag].dir)]
-        if (games[tag].module) {
-            args.push(games[tag].module)
-            if (games[tag].name) { args.push(games[tag].name) }
-        }
-        serverProcess = cp.spawn("./gameserver", args,
-            { cwd: path.join(__dirname, "./build/bin/") })
-    } else {
-        serverProcess =  cp.spawn("./bubblewrap.sh",
-            [games[tag].dir],
-            { cwd: __dirname })
-    }
-    serverProcess.on('error', error =>
-        console.error(`Launching Lean Server failed: ${error}`)
-    );
-    if (serverProcess.stderr !== null) {
-        serverProcess.stderr.on('data', data =>
-            console.error(`Lean Server: ${data}`)
-        );
-    }
-    return serverProcess
-}
-
-/** start Lean Server processes to refill the queue */
-function fillQueue(tag) {
-    while (queue[tag].length < games[tag].queueLength) {
-        const serverProcess = startServerProcess(tag)
-        queue[tag].push(serverProcess)
-    }
-}
-
-if (!isDevelopment) { // Don't use queue in development
-    for (let tag in games) {
-        queue[tag] = []
-        fillQueue(tag)
-    }
-}
-
-const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
-
-wss.addListener("connection", function(ws, req) {
-    const reRes = urlRegEx.exec(req.url)
-    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()}`
-
-    if (isDevelopment && process.env.DEV_CONTAINER) {
-        tag = `g/local/game`
-    }
-
-    let ps;
-    if (!queue[tag] || queue[tag].length == 0) {
-        ps = startServerProcess(tag)
-    } else {
-        ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
-        fillQueue(tag)
-    }
-
-    socketCounter += 1;
-    const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
-    console.log(`[${new Date()}] Socket opened - ${ip}`)
-
-    const socket = {
-        onMessage: (cb) => { ws.on("message", cb) },
-        onError: (cb) => { ws.on("error", cb) },
-        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 socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
-    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;
-    });
-
-    console.log(`[${new Date()}] Number of open sockets - ${socketCounter}`)
-    console.log(`[${new Date()}] Free RAM - ${Math.round(os.freemem() / 1024 / 1024)} / ${Math.round(os.totalmem() / 1024 / 1024)} MB`)
-
-    ws.on('close', () => {
-      console.log(`[${new Date()}] Socket closed - ${ip}`)
-      socketCounter -= 1;
-    })
-
-    socketConnection.onClose(() => serverConnection.dispose());
-    serverConnection.onClose(() => socketConnection.dispose());
-})

server/lake-manifest.json

@@ -1 +1,14 @@
-{"version": 5, "packagesDir": "lake-packages", "packages": []}
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "GameServer",
+ "lakeDir": ".lake"}

server/lakefile.lean

@@ -3,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.0.0
+leanprover/lean4:v4.3.0

server/test/test_statement.lean

@@ -13,13 +13,16 @@ Level 1
 Statement foo.bar : 5 ≤ 7 := by
   simp
 
--- Shows warning on `foo.bar₂`:
+Game "Test"
+World "TestW"
+Level 2 -- should warn if set to `1`
 
+-- Shows warning on `foo.bar₂`:
 Statement foo.bar2 : 3 ≤ 7 := by
   simp
 
 
-NewLemma foo.baz
+NewLemma foo.bar
 DisabledTactic tauto
 
 

server/unpack.sh

@@ -1,13 +0,0 @@
-#/bin/bash
-
-ARTIFACT_ID=$1
-
-echo "Unpacking ZIP."
-unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID}
-echo "Unpacking TAR."
-for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file
-do
-  echo "Unpacking $f"
-  mkdir tmp/artifact_${ARTIFACT_ID}_inner
-  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
-done

tsconfig.json

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

vite.config.ts

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

webpack.config.js

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