leanprover-community · RexWzh · Oct 4, 2025 · Oct 6, 2025 · Oct 7, 2025 · Oct 7, 2025
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -0,0 +1,64 @@
+name: Documentation
+
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
+# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  # Build job
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+
+    - name: Set up Python
+      uses: actions/setup-python@v4
+      with:
+        python-version: '3.11'
+
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        pip install mkdocs>=1.4.0
+        pip install mkdocs-material>=9.0.0
+        pip install mkdocs-static-i18n>=0.5.0
+
+    - name: Setup Pages
+      uses: actions/configure-pages@v4
+
+    - name: Build documentation
+      run: |
+        # Build MkDocs site for all languages
+        mkdocs build --verbose
+
+    - name: Upload artifact
+      uses: actions/upload-pages-artifact@v3
+      with:
+        path: ./site
+
+  # Deployment job
+  deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    if: github.ref == 'refs/heads/main'
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
diff --git a/.gitignore b/.gitignore
@@ -9,3 +9,4 @@ relay/prev_cpu_metric
 test.ecosystem.config.cjs
 prod.ecosystem.config.cjs
 cypress/screenshots
+/site/
diff --git a/README.md b/README.md
@@ -4,12 +4,12 @@ This is the source code for a Lean game platform hosted at [adam.math.hhu.de](ht
 
 ## Creating a Game
 
-Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
+Please follow the tutorial [Creating a Game](docs/en/game-development/create_game.md). In particular, the following steps might be of interest:
 
-* Step 6: [How to Run Games Locally](doc/running_locally.md)
-* Step 8: [How to Update an existing Game](doc/update_game.md)
-* Step 10: [How to Publish a Game](doc/publish_game.md)
-* [Troubleshooting](doc/troubleshoot.md)
+* Step 6: [How to Run Games Locally](docs/en/getting-started/running_locally.md)
+* Step 8: [How to Update an existing Game](docs/en/getting-started/update_game.md)
+* Step 10: [How to Publish a Game](docs/en/getting-started/publish_game.md)
+* [Troubleshooting](docs/en/getting-started/troubleshoot.md)
 
 ## Documentation
 
@@ -18,20 +18,20 @@ should be up-to-date:
 
 ### Game creation API
 
-- [Creating a Game](doc/create_game.md): **the main document to consult**.
-- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
+- [Creating a Game](docs/en/game-development/create_game.md): **the main document to consult**.
+- [More about Hints](docs/en/game-development/hints.md): describes the `Hint` and `Branch` tactic.
 
 ### Frontend API
 
-* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
-* [How to Update an existing Game](doc/update_game.md): update to a new lean version
-* [How to Publish a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
+* [How to Run Games Locally](docs/en/getting-started/running_locally.md): play a game on your computer
+* [How to Update an existing Game](docs/en/getting-started/update_game.md): update to a new lean version
+* [How to Publish a Game](docs/en/getting-started/publish_game.md): load your game to adam.math.hhu.de for others to play
 
 ### Backend
 
 not fully written yet.
 
-* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
+* [Server](docs/en/server-deployment/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
 
 ## Contributing
 
@@ -46,7 +46,7 @@ The interface can be translated to various languages. For adding a translation,
 3. Add all translations.
 4. Commit the changes you made to `config.json` together with the new `translation.json`.
 
-For translating games, see [Translating a game](doc/translate.md).
+For translating games, see [Translating a game](docs/en/game-development/translate.md).
 
 ## Security
 

diff --git a/doc/changelog.md → docs/en/changelog.md b/doc/changelog.md → docs/en/changelog.md
diff --git a/doc/create_game.md → docs/en/game-development/create_game.md b/doc/create_game.md → docs/en/game-development/create_game.md
@@ -171,7 +171,7 @@ at the end.
 
 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!
+There are multiple ways how you can start the game locally to test-play it described at [How to Run the Game Locally](../getting-started/running_locally.md). If you have problems getting one of the setups to work, please get in contact!
 
 
 ## 7. Dive into Level creation
@@ -254,15 +254,15 @@ You can but a `Statement` inside namespaces like you would with `theorem`.
 
 #### Doc String / Exercise statement
 
-Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. See [LaTeX in Games](latex.md) for more details on formatting.
+Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. See [LaTeX in Games](../game-development/latex.md) for more details on formatting.
 
 ```lean
 /-- The exercise statement in natural language using latex: $\iff$. -/
 Statement ...
   sorry
 ```
 
-For more details and features, read [Writing Exercises](writing_exercises.md)
+For more details and features, read [Writing Exercises](../game-development/writing_exercises.md)
 
 ### 7. c) Proof
 
@@ -288,7 +288,7 @@ 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](hints.md) for how they work and what the options are.
+Read [More about Hints](../game-development/hints.md) for how they work and what the options are.
 
 ### 7. 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.
@@ -298,19 +298,19 @@ 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.
 
-You can also embed images in the text as descriped in [Markdown](markdown.md).
+You can also embed images in the text as descriped in [Markdown](../game-development/markdown.md).
 
 ## 8. 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](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](../getting-started/update_game.md).
 
 ## 9. Add translation
 
-See [Translating a game](translate.md).
+See [Translating a game](../game-development/translate.md).
 
 ## 10. Publish your game
 
-To publish your game on the official server, see [Publishing a game](publish_game.md)
+To publish your game on the official server, see [Publishing a game](../getting-started/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:
 
@@ -348,7 +348,7 @@ Currently existing options are:
 ### Markdown
 
 Texts should generally support markdown. For some tips on how to use markdown, see
-[Markdown styling](markdown.md).
+[Markdown styling](../game-development/markdown.md).
 
 In particular, you can embed images in texts, see the specific instructions in that file.
 
@@ -357,7 +357,7 @@ In particular, you can embed images in texts, see the specific instructions in t
 ### Markdown
 
 Texts should generally support markdown. For some tips on how to use markdown, see
-[Markdown styling](markdown.md).
+[Markdown styling](../game-development/markdown.md).
 
 In particular, you can embed images in texts, see the specific instructions in that file.
 
@@ -372,7 +372,7 @@ Inside strings, you need to escape backslashes, but not inside doc-strings, ther
 ### LaTeX support
 
 LaTeX is rendered using the [KaTeX library](https://katex.org/),
-see [Using LaTeX in the Game](latex.md) for details.
+see [Using LaTeX in the Game](../game-development/latex.md) for details.
 
 ### Number Of Levels Limit
 

diff --git a/doc/environment.md → docs/en/game-development/environment.md b/doc/environment.md → docs/en/game-development/environment.md
diff --git a/doc/hints.md → docs/en/game-development/hints.md b/doc/hints.md → docs/en/game-development/hints.md
diff --git a/doc/latex.md → docs/en/game-development/latex.md b/doc/latex.md → docs/en/game-development/latex.md
diff --git a/doc/markdown.md → docs/en/game-development/markdown.md b/doc/markdown.md → docs/en/game-development/markdown.md
@@ -20,4 +20,4 @@ For external images, you can add them using a full URL:
 ```
 
 Note: the `images/` folder is the same folder used for introduction images for worlds.
-See [Creating a Game > 6e](create_game.md#6-e-extra-images)
+See [Creating a Game > 6e](../game-development/create_game.md#6-e-extra-images)
diff --git a/doc/translate.md → docs/en/game-development/translate.md b/doc/translate.md → docs/en/game-development/translate.md
@@ -7,7 +7,7 @@ The intended workflow currently is the following:
 1. When you call `lake build` in your game, it should automatically create a template file `.i18n/en/Game.pot`. Alternatively you can call `lake exe i18n --template` to recreate it.
 2. Open the file `Game.pot` (the "t" stands for "template") with [Poedit](https://poedit.net/) (or a similar software) and translate all strings. Save your work as `.i18n/{language}/Game.po`.
 4. Call `lake exe i18n --export-json` to create all Json files `.i18n/{language}/Game.json` which the server needs.
-5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](publish_game.md).
+5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](../getting-started/publish_game.md).
 
 If you choose the correct language in the "Preferences" of the game, you should see your translations.
 

diff --git a/doc/writing_exercises.md → .../en/game-development/writing_exercises.md b/doc/writing_exercises.md → .../en/game-development/writing_exercises.md
diff --git a/doc/publish_game.md → docs/en/getting-started/publish_game.md b/doc/publish_game.md → docs/en/getting-started/publish_game.md
diff --git a/doc/running_locally.md → docs/en/getting-started/running_locally.md b/doc/running_locally.md → docs/en/getting-started/running_locally.md
diff --git a/doc/troubleshoot.md → docs/en/getting-started/troubleshoot.md b/doc/troubleshoot.md → docs/en/getting-started/troubleshoot.md
diff --git a/doc/update_game.md → docs/en/getting-started/update_game.md b/doc/update_game.md → docs/en/getting-started/update_game.md
diff --git a/docs/en/index.md b/docs/en/index.md
@@ -0,0 +1,65 @@
+# Lean 4 Game
+
+This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
+
+## Creating a Game
+
+Please follow the tutorial [Creating a Game](game-development/create_game.md). In particular, the following steps might be of interest:
+
+* Step 6: [How to Run Games Locally](getting-started/running_locally.md)
+* Step 8: [How to Update an existing Game](getting-started/update_game.md)
+* Step 10: [How to Publish a Game](getting-started/publish_game.md)
+* [Troubleshooting](getting-started/troubleshoot.md)
+
+## Documentation
+
+The documentation is very much work in progress but the linked documentation here
+should be up-to-date:
+
+### Game creation API
+
+- [Creating a Game](game-development/create_game.md): **the main document to consult**.
+- [More about Hints](game-development/hints.md): describes the `Hint` and `Branch` tactic.
+
+### Frontend API
+
+* [How to Run Games Locally](getting-started/running_locally.md): play a game on your computer
+* [How to Update an existing Game](getting-started/update_game.md): update to a new lean version
+* [How to Publish a Game](getting-started/publish_game.md): load your game to adam.math.hhu.de for others to play
+
+### Backend
+
+not fully written yet.
+
+* [Server](server-deployment/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
+
+## Contributing
+
+Contributions to `lean4game` are always welcome!
+
+### Translation
+
+The interface can be translated to various languages. For adding a translation, one needs to do the following:
+
+1. In `client/src/config.json`, add your new language. The "iso" key is the ISO language code, i.e. it should be accepted by "i18next" and "GNU gettext"; the "flag" key is once accepted by [react-country-flag](https://www.npmjs.com/package/react-country-flag).
+2. Run `npm run translate`. This should create a new file `client/public/locales/{language}/translation.json`. (alternatively you can copy-paste `client/public/locales/en/translation.json`)
+3. Add all translations.
+4. Commit the changes you made to `config.json` together with the new `translation.json`.
+
+For translating games, see [Translating a game](game-development/translate.md).
+
+## Security
+
+Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
+
+## Contact
+
+In case of technical problems with ```adam.math.hhu.de``` please contact us via <a href="mailto:[email protected]?subject=Lean4Game: <Your%20Question>">e-mail</a>.
+
+## Credits
+
+The project has primarily been developed by Alexander Bentkamp and Jon Eugster.
+
+It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
+by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
diff --git a/doc/DOCUMENTATION.md → docs/en/server-deployment/DOCUMENTATION.md b/doc/DOCUMENTATION.md → docs/en/server-deployment/DOCUMENTATION.md
@@ -34,8 +34,7 @@ Currently, this happens through a lake-post-update-hook when calling `lake updat
 
 ### Starting the server
 
-When using the [manual installation](running_locally.md#manual-installation) you can run the server
-using
+When using [manual installation](../getting-started/running_locally.md#manual-installation), you can run the server with
 
 ```
 npm start

diff --git a/doc/client.md → docs/en/server-deployment/client.md b/doc/client.md → docs/en/server-deployment/client.md
diff --git a/doc/npm_scripts.md → docs/en/server-deployment/npm_scripts.md b/doc/npm_scripts.md → docs/en/server-deployment/npm_scripts.md
diff --git a/doc/server.md → docs/en/server-deployment/server.md b/doc/server.md → docs/en/server-deployment/server.md
diff --git a/docs/zh/changelog.md b/docs/zh/changelog.md
@@ -0,0 +1,9 @@
+# 更新日志
+
+## v4.5.0
+
+### 重大修改
+
+* 修复 (#183)：本地存储接受不区分大小写的 URL。旧版的游戏进度保存在区分大小写的 URL 下。您可能需要从浏览器存储中恢复旧进度。
+
+## 其他