update doc

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
 

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

@@ -1,26 +1,30 @@
-# Importing games
+# Publishing games
 
-There is an mechanism to import games into your server. In order to use this mechanism, you need
+You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
-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
+steps.
-repos will suffice.
 
-You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
+## 1. Upload Game to github
-with your user name and access token.
 
-Then you can call:
+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.
 
-> https://{website}/import/trigger/{owner}/{repo}
+## 2. Import the game
 
-where you replace:
+You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
-- website: The website your server runs on, e.g. `localhost:3000`
+the URL of the form
-- 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.
+> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
- Once this import reports "Done", you should be able to play your game under:
 
-> https://{website}/#/g/{owner}/{repo}
+where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name.
 
-## data management
+You should see a white screen which shows import updates and eventually reports "Done."
-Everything downloaded remains in the folder `lean4game/games`.
+
-the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
+## 3. Play the game
-The other folders should only contain the built lean-games, sorted by owner and repo.
+
+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,7 +10,11 @@ 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
+  ```
+  npm install
+  lake update -R
+  ```
 * Gitpod/Codespaces: Create a fresh one
 
 This will update `lean4game` and `mathlib` in your project to the new lean version.