Merge branch 'dev'

.gitignore

@@ -1,7 +1,6 @@
 node_modules
+games/
 client/dist
-server/build
-server/tmp
-server/lakefile.olean
-**/lake-packages/
+games/
+server/.lake
 **/.DS_Store

README.md

@@ -8,6 +8,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 
 * Step 5: [How to Run Games Locally](doc/running_locally.md)
 * Step 7: [How to Update an existing Game](doc/update_game.md)
+* Step 8: [How to Publishing a Game](doc/publish_game.md)
 
 ### Publishing a Game
 

client/src/app.tsx

@@ -10,6 +10,7 @@ import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
 import { useWindowDimensions } from './window_width';
+import { connection } from './connection';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
@@ -19,6 +20,10 @@ function App() {
   const {width, height} = useWindowDimensions()
   const [mobile, setMobile] = React.useState(width < 800)
 
+  React.useEffect(() => {
+    connection.startLeanClient(gameId);
+  }, [gameId])
+
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>

client/src/components/infoview/main.tsx

@@ -347,6 +347,7 @@ export function TypewriterInterface({props}) {
   const uri = model.uri.toString()
 
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
+  const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(MobileContext)
   const { proof } = React.useContext(ProofContext)
@@ -455,6 +456,17 @@ export function TypewriterInterface({props}) {
 
   let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
+
+  useServerNotificationEffect("$/game/loading", (params : any) => {
+    if (params.kind == "loadConstants") {
+      setLoadingProgress(params.counter/100*50)
+    } else if (params.kind == "finalizeExtensions") {
+      setLoadingProgress(50 + params.counter/150*50)
+    } else {
+      console.error(`Unknown loading kind: ${params.kind}`)
+    }
+  })
+
   return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
@@ -521,7 +533,7 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress />
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
         }
       </div>
     </div>

client/src/components/level.tsx

@@ -48,7 +48,6 @@ function Level() {
   const params = useParams()
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
-  // useLoadWorldFiles(worldId)
 
   const [impressum, setImpressum] = React.useState(false)
 
@@ -615,6 +614,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
       return () => {
         editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
+        model.dispose();
       }
     }
   }, [editor, levelId, connection, leanClientStarted])
@@ -637,27 +637,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/index.tsx

@@ -34,6 +34,11 @@ const router = createHashRouter([
     path: "/game/nng",
     loader: () => redirect("/g/hhu-adam/NNG4")
   },
+  {
+    // For backwards compatibility
+    path: "/g/hhu-adam/NNG4",
+    loader: () => redirect("/g/leanprover-community/NNG4")
+  },
   {
     path: "/g/:owner/:repo",
     element: <App />,

client/src/state/api.ts

@@ -2,7 +2,6 @@
  * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
-import { Connection } from '../connection'
 
 export interface GameInfo {
   title: null|string,
@@ -57,40 +56,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 + "/api" }),
   endpoints: (builder) => ({
     getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: ({game}) => {return {game, method: 'info', params: {}}},
+      query: ({game}) => `${game}/game`,
     }),
     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}`,
     }),
     loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
-      query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}},
+      query: ({game}) => `${game}/inventory`,
     }),
     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}`,
     }),
   }),
 })

doc/create_game.md

@@ -245,7 +245,11 @@ That way, the game will replace it with the actual name the assumption has in th
 
 ## 7. Update your game
 
-In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md).
+In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
+
+## 8. Publish your game
+
+To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
 
 ## Further Notes
 

doc/publish_game.md

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

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

@@ -10,10 +10,24 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
 Then, depending on the setup you use, do one of the following:
 
 * Dev Container: Rebuild the VSCode Devcontainer.
-* Local Setup: run `lake update -R` (followed by `lake exe cache get` if you depend on mathlib.)
+* Local Setup: run
+  ```
+  lake update -R
+  lake build
+  ```
+  in your game folder.
+
+  * Additionally, if you have a local copy of the server `lean4game`,
+    you should update this one to the matching version, too:
+    ```
+    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 `lean4game` and `mathlib` in your project to the new lean version.
+This will your game (and the mathlib version you might be using) to the new lean version.
 
 ## Newest developing setup
 
@@ -24,14 +38,16 @@ anymore, you will need to copy the relevant files from the [GameSkeleton](https:
 The relevant files are:
 
 ```
+.devcontainer/
+.docker/
+.github/
+.gitpod/
+.vscode/
 lakefile.lean
-.devcontainer/**
-.docker/**
-.gitpod
-.vscode/**
 ```
 
-simply copy them from the `GameSkeleton` into your game.
+simply copy them from the `GameSkeleton` into your game and proceed as above,
+i.e. `lake update -R && lake build`.
 
 (Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
-where you need to add any dependencies of your game.)
+where you need to add any dependencies of your game, or remove mathlib if you don't need it.)

ecosystem.config.js → ecosystem.config.cjs

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

server/.gitignore

@@ -1,3 +1,3 @@
-build
-adam
-nng
+build/
+games/
+.lake

server/GameServer/Commands.lean

@@ -644,6 +644,44 @@ elab "Template" tacs:tacticSeq : tactic => do
 
 /-! # Make Game -/
 
+#eval IO.FS.createDirAll ".lake/gamedata/"
+
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit:= do
+  let game ← getCurGame
+  let env ← getEnv
+  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+
+  if ← path.isDir then
+    IO.FS.removeDirAll path
+  IO.FS.createDirAll path
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    for (levelId, level) in world.levels.toArray do
+      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+
+  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+
+  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
+    for name in allItemsByType.findD inventoryType {} do
+      let some item ← getInventoryItem? name inventoryType
+        | throwError "Expected item to exist: {name}"
+      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := ← getTiles .Lemma
+    tactics := ← getTiles .Tactic
+    definitions := ← getTiles .Definition
+    lemmaTab := none
+  }
+  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
+
+
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
@@ -923,6 +961,7 @@ elab "MakeGame" : command => do
   -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
   let game ← getCurGame
 
+  let mut allItemsByType : HashMap InventoryType (HashSet Name) := {}
   -- Compute which inventory items are available in which level:
   for inventoryType in #[.Tactic, .Definition, .Lemma] do
 
@@ -1052,6 +1091,9 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
+    allItemsByType := allItemsByType.insert inventoryType allItems
+
+  saveGameData allItemsByType
 
 /-! # Debugging tools -/