diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml new file mode 100644 index 00000000..cc445bfc --- /dev/null +++ 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 index ec00daa8..f03cc86f 100644 --- 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 index 868ba1c3..7e57e1a8 100644 --- 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 b/docs/en/changelog.md similarity index 100% rename from doc/changelog.md rename to docs/en/changelog.md diff --git a/doc/create_game.md b/docs/en/game-development/create_game.md similarity index 93% rename from doc/create_game.md rename to docs/en/game-development/create_game.md index 4ddc1fa0..4ab79d32 100644 --- a/doc/create_game.md +++ b/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,7 +254,7 @@ 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$. -/ @@ -262,7 +262,7 @@ 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 b/docs/en/game-development/environment.md similarity index 100% rename from doc/environment.md rename to docs/en/game-development/environment.md diff --git a/doc/hints.md b/docs/en/game-development/hints.md similarity index 100% rename from doc/hints.md rename to docs/en/game-development/hints.md diff --git a/doc/latex.md b/docs/en/game-development/latex.md similarity index 100% rename from doc/latex.md rename to docs/en/game-development/latex.md diff --git a/doc/markdown.md b/docs/en/game-development/markdown.md similarity index 87% rename from doc/markdown.md rename to docs/en/game-development/markdown.md index 23e40cb1..546cb27b 100644 --- a/doc/markdown.md +++ b/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 b/docs/en/game-development/translate.md similarity index 97% rename from doc/translate.md rename to docs/en/game-development/translate.md index 57a67acc..14ba8322 100644 --- a/doc/translate.md +++ b/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 b/docs/en/game-development/writing_exercises.md similarity index 100% rename from doc/writing_exercises.md rename to docs/en/game-development/writing_exercises.md diff --git a/doc/publish_game.md b/docs/en/getting-started/publish_game.md similarity index 100% rename from doc/publish_game.md rename to docs/en/getting-started/publish_game.md diff --git a/doc/running_locally.md b/docs/en/getting-started/running_locally.md similarity index 100% rename from doc/running_locally.md rename to docs/en/getting-started/running_locally.md diff --git a/doc/troubleshoot.md b/docs/en/getting-started/troubleshoot.md similarity index 100% rename from doc/troubleshoot.md rename to docs/en/getting-started/troubleshoot.md diff --git a/doc/update_game.md b/docs/en/getting-started/update_game.md similarity index 100% rename from doc/update_game.md rename to docs/en/getting-started/update_game.md diff --git a/docs/en/index.md b/docs/en/index.md new file mode 100644 index 00000000..b3cd5123 --- /dev/null +++ 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 e-mail. + +## 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 b/docs/en/server-deployment/DOCUMENTATION.md similarity index 95% rename from doc/DOCUMENTATION.md rename to docs/en/server-deployment/DOCUMENTATION.md index 10869252..bc7ca0cd 100644 --- a/doc/DOCUMENTATION.md +++ b/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 b/docs/en/server-deployment/client.md similarity index 100% rename from doc/client.md rename to docs/en/server-deployment/client.md diff --git a/doc/npm_scripts.md b/docs/en/server-deployment/npm_scripts.md similarity index 100% rename from doc/npm_scripts.md rename to docs/en/server-deployment/npm_scripts.md diff --git a/doc/server.md b/docs/en/server-deployment/server.md similarity index 100% rename from doc/server.md rename to docs/en/server-deployment/server.md diff --git a/docs/zh/changelog.md b/docs/zh/changelog.md new file mode 100644 index 00000000..e62cfc7a --- /dev/null +++ b/docs/zh/changelog.md @@ -0,0 +1,9 @@ +# 更新日志 + +## v4.5.0 + +### 重大修改 + +* 修复 (#183)：本地存储接受不区分大小写的 URL。旧版的游戏进度保存在区分大小写的 URL 下。您可能需要从浏览器存储中恢复旧进度。 + +## 其他 diff --git a/docs/zh/game-development/create_game.md b/docs/zh/game-development/create_game.md new file mode 100644 index 00000000..6a31f438 --- /dev/null +++ b/docs/zh/game-development/create_game.md @@ -0,0 +1,339 @@ +# 创建新游戏 + +本教程将指导您为 lean4 创建新游戏。内容涵盖从编写新关卡、本地测试游戏到在线发布游戏的全过程。 + +## 1. 创建项目 + +1. 使用 [GameSkeleton 模板](https://github.com/hhu-adam/GameSkeleton) 为您的游戏创建新的 github 仓库：在 github 上，点击 "Use this template" > "Create a new repository"。 +2. 克隆游戏仓库。 +3. 运行 `lake update -R && lake build` 来构建 Lean 项目。 + +### 运行游戏 + +现在您可以在 VSCode 中打开游戏（`cd YourGame/` 然后 `code .`），并像常规 Lean 项目一样开始修改它。要运行游戏，请参考下面的"**6. 本地测试游戏**"部分。 + +## 2. Game.lean + +文件 `Game.lean` 是游戏的骨干，将所有内容整合在一起。 + +1. `MakeGame`：这个命令是游戏构建的地方。如果有需要修复的问题，它们将在这里显示为警告或错误（VSCode 中的橙色/红色波浪线）。注意您可能需要调用 "Lean: Restart File"（Ctrl+Shift+X）来重新加载文件并查看在其他文件中所做的更改。 +2. `Title`：设置游戏的显示标题。 +3. `Introduction`：这是在世界选择树旁边开始时显示的文本。 +4. `Info`：这将在游戏菜单中显示为"游戏信息"。用它来显示制作人员、资助和其他关于游戏的元信息。 +5. 导入：文件需要导入所有世界文件，我们稍后会看到。如果您添加新世界，记得在这里导入它！ +6. `Dependency`：（可选）这个命令在世界树中添加另一条边。游戏会根据使用的策略/定理自动计算它们。但是，有时您需要游戏无法计算的依赖关系，例如您在一个世界中解释了 `≠`，而在另一个世界中，用户应该已经知道它。语法是 `Dependency World₁ → World₂ → World₃`。 + +所以 `Game.lean` 具有以下结构： + +```lean +import GameServer + +-- 导入所有世界 +import Game.Levels.Tutorial + +Title "我的游戏" + +Introduction " +嗨，很高兴您来到这里！点击一个世界开始。 +" + +Info " +这个游戏由我开发。 +" + +-- Dependency World₁ → World₂ -- 因为 `≠` + +MakeGame +``` + +### 局部记号 + +**重要**：如果您在游戏中使用任何局部记号，您需要在 `MakeGame` 之前手动打开这些命名空间，以便在清单中看到记号。 + +例如（使用 mathlib），写 + +``` +open BigOperators + +MakeGame +``` + +以便看到 `∑ x in s, f x` 而不是 `Finset.sum s fun x => f x`。 + +## 3. 创建关卡 + +在本教程中，我们首先学习关卡。游戏由世界树组成，每个世界有若干关卡，编号从 1 到 n。这里我们创建世界 `MyWorld` 的第 1 关。我们在下一节将这个世界添加到游戏中。 + +最小的关卡文件如下所示。有许多选项可以添加，我们将在后面的部分深入探讨 + +```lean +import GameServer + +World "MyWorld" +Level 1 +Title "Hello World" + +Introduction " +在关卡开始时显示的消息。用它来解释任何新概念。 +" + +/-- 使用 latex 的自然语言练习陈述：$\iff$。 -/ +Statement (n : Nat) : 0 + n = n := by + sorry + +Conclusion " +关卡完成时显示的消息 +" +``` + +1. 创建文件夹 `Game/Levels/MyWorld` +2. 创建文件 `Game/Levels/MyWorld/L01_hello.lean` +3. 将上述内容复制到您的第一个关卡中。 + +## 4. 创建世界 + +现在我们创建一个世界。为此，我们创建一个文件 `MyWorld.lean`，它导入这个世界的所有关卡： + +```lean +import Game.Levels.MyWorld.L01_hello + +World "MyWorld" +Title "我的第一个世界" + +Introduction +" +这个介绍文本在首次进入世界时显示。 +" +``` + +1. 创建文件 `Game/Levels/MyWorld.lean` +2. 使用上面的模板，确保您导入这个世界的所有关卡。 +3. 在 `Game.lean` 中用 `import Game.Levels.MyWorld` 导入世界 + +现在您创建了一个有一个关卡的世界并添加了它🎉 `Game.lean` 中的命令 `MakeGame` 会显示您可能需要修复的任何问题。目前，它显示 + +```text +No world introducing sorry, but required by MyWorld +``` + +这意味着世界 `MyWorld` 在证明中使用了策略 `sorry`，但 `sorry` 还没有在任何地方被介绍。 + +## 5. 重构现有世界 + +[GameSkeleton 模板](https://github.com/hhu-adam/GameSkeleton) 包含一个 bash 脚本 `sofi.sh` +（`s`ort `o`ut `f`ilenames and `i`mports）， +它可以帮助重构现有世界，例如如果您想重新排序或重命名现有关卡，或在中间添加额外的关卡。例如，假设您在文件夹中有一个"算术世界" + + Game/Levels/Arithmetic + +由下表左列中列出的三个关卡组成。假设您想切换乘法和加法的顺序，并在中间插入一个关于减法的额外关卡。然后您可以简单地编辑*文件名*如第二列所示，并为减法关卡添加额外的文件，使文件按字母顺序排序时处于预期的顺序（如第三列所示）。 + +| 现有关卡 | 手动更改 | 按字母顺序排列的文件 | 最终结果 | +|--------------------|--------------------------|-----------------------------|---------------------| +| L01\_hello.lean | L01\_hello.lean | L01\_hello.lean | L01\_hello.lean | +| L02\_multiply.lean | **L03**\_multiply.lean | L02a\_add.lean | L02\_add.lean | +| L03\_add.lean | **L02a**\_add.lean | L02b\_substract.lean | L03\_substract.lean | +| | **L02b\_substract.lean** | L03\_multiply.lean | L04\_multiply.lean | + +调用 + + ./sofi.sh Game/Levels/Arithmetic + +然后将 + +- 重命名文件如最后一列所示， +- 更新每个文件中的关卡编号， +- 合理地尝试更新每个关卡文件中的 `import` 语句，以及 +- 更新基础文件 `Game/Levels/Arithmetic.lean` 中的导入。 + +更多详细信息记录在脚本本身中。 + +最后不要忘记用以下命令将所有新/重命名的文件添加到 git： + + git add Game/Levels/Arithmetic/ + +## 6. 本地测试游戏 + +现在是时候本地测试游戏并玩它了。 + +有多种方法可以在本地启动游戏进行测试，详见[如何本地运行游戏](../getting-started/running_locally.md)。如果您在设置任何一种方法时遇到问题，请联系我们！ + +## 7. 深入关卡创建 + +现在您有了一个运行的游戏，我们更仔细地看看关卡文件以及您设计游戏的所有选项。 + +### 7. a) 清单 + +玩家有一个包含策略、定理和定义的清单，这些在游戏过程中解锁。您可以通过在 `Statement` 下面添加以下内容之一来在关卡中解锁/介绍这些项目。 + +```lean +NewTactic induction simp +NewTheorem Nat.zero_mul +NewDefinition Pow +``` + +**重要：** 本节 6a) 中的所有命令都期望它们作为输入的 `Name` 是**完全限定的**。例如 `NewTheorem Nat.zero_mul` 而不是 `NewTheorem zero_mul`。 + +#### 文档条目 + +您会看到关于缺少定理文档的警告。您可以通过在它上面某处添加如下的文档条目来修复它。 + +```lean +/-- +一些描述 +-/ +TheoremDoc Nat.zero_mul as "zero_mul" in "Mul" + +/-- +一些描述 +-/ +TacticDoc simp + +/-- +一些描述 +-/ +DefinitionDoc Pow as "^" +``` + +（例如，您也可以创建文件 `Game/Doc/MyTheorems.lean`，在那里添加您的文档并导入它） + +如果您不为清单提供任何内容，游戏将尝试找到该选项的文档字符串并显示该文档字符串。 + +#### 清单管理 + +您有几个选项来禁用在之前关卡中已解锁的清单选项： + +```lean +DisabledTactic, DisabledTheorem, OnlyTactic, OnlyTheorem +``` + +具有与上面相同的语法。前两个为此关卡禁用选项，后两个禁用除指定选项之外的所有选项。 + +#### 定理标签 + +定理被分类到标签中。用 `TheoremTab "Mul"` 您指定在此关卡中默认应该打开哪个标签。 + +#### 隐藏策略 + +`NewHiddenTactic` 让您添加策略而不将其添加到清单中。这对策略的变体很有用。例如，您可以这样做 + +```lean +NewTactic rw +NewHiddenTactic rewrite nth_rewrite rwa +``` + +只有 `rw` 会出现在清单中。 + +### 7. b) 陈述 + +陈述是关卡的练习。基础工作与在 `example` 或 `theorem` 中的工作相同。但是请注意，您**必须**进行策略证明，即 `:= by` 是语法的硬编码部分 + +#### 名称 + +您可以给您的练习一个名称：`Statement my_first_exercise (n : Nat) …`。如果您这样做，它将被添加到清单中并在未来的关卡中可用。 +您可以像使用 `theorem` 一样将 `Statement` 放在命名空间内。 + +#### 文档字符串 / 练习陈述 + +添加包含自然语言练习陈述的文档字符串。如果您这样做，它将出现在练习的顶部。有关格式的更多详细信息，请参见[游戏中的 LaTeX](../game-development/latex.md)。 + +```lean +/-- 使用 latex 的自然语言练习陈述：$\iff$。 -/ +Statement ... + sorry +``` + +有关更多详细信息和功能，请阅读[编写练习](../game-development/writing_exercises.md) + +### 7. c) 证明 + +证明必须始终是策略证明，即 `:= by` 是语法的强制部分。 + +有一些额外的策略可以帮助您构建证明： + +- `Hint`：您可以使用 `Hint "text"` 在游戏中的目标状态与放置 `Hint` 的位置匹配时显示文本。有关提示的更多选项，请参见下文。 +- `Branch`：在证明中您可以添加运行替代策略序列的 `Branch`，这有助于在不同位置设置 `Hints`。`Branch` 不影响主证明，不需要完成任何目标。 +- `Template`/`Hole`：用于提供示例证明模板。`Template` 内的任何内容都将被复制到编辑器中，所有 `Hole` 都被替换为 `sorry`。注意，拥有 `Template` 将强制用户为此关卡使用编辑器模式。 + +要记住的一点是，游戏将查看主证明来确定需要哪些策略和定理，但它忽略任何 `Branch`。 + +### 7. d) 提示 + +对于游戏开发来说，最重要的可能是 `Hints`。 + +每当玩家的当前目标与提示在示例证明中放置的目标匹配时，提示就会显示。您可以使用 `Branch` 在死胡同或替代证明分支中放置提示。 + +阅读[更多关于提示](../game-development/hints.md)了解它们如何工作以及有哪些选项。 + +### 7. e) 额外：图像 +您可以在游戏的任何层级（即游戏/世界/关卡）添加图像。这些将在您的游戏中显示。 + +图像需要放在 `images/` 中，您需要在 2)、3) 或 4) 中创建的文件之一（即游戏/世界/关卡）中添加像 `Image "images/path/to/myWorldImage.png"` 这样的命令。 + +注意：目前，只显示世界的图像。它们出现在世界的介绍中。 + +您也可以在文本中嵌入图像，如[Markdown](../game-development/markdown.md)中所述。 + +## 8. 更新您的游戏 + +原则上，更新您的游戏到新的 Lean 版本就像修改 `lean-toolchain` 一样简单。但是，您应该阅读[更新现有游戏](../getting-started/update_game.md)中的详细信息。 + +## 9. 添加翻译 + +参见[翻译游戏](../game-development/translate.md)。 + +## 10. 发布您的游戏 + +要在官方服务器上发布您的游戏，请参见[发布游戏](../getting-started/publish_game.md) + +在 `MakeGame` 命令之前，您可以在 `Game.lean` 中添加一些更多选项，这些选项描述在服务器登录页面上可见的磁贴： + +```lean +Languages "English" +CaptionShort "游戏模板" +CaptionLong "您应该使用这个游戏作为您自己游戏的模板并添加您自己的关卡。" +Prerequisites "NNG" +CoverImage "images/cover.png" +``` +* `Languages`：目前只有一种语言（大写英文名称）。磁贴将显示相应的旗帜。 +* `CaptionShort`：一个标语。出现在图像上方。 +* `CaptionLong`：2-4 句话来描述游戏。 +* `Prerequisites` 您在玩这个游戏之前应该玩的其他游戏列表，例如 `Prerequisites "NNG" "STG"`。游戏名称是自由文本。 +* `CoverImage`：您可以创建文件夹 `images/` 并在那里放置游戏使用的图像。最大比例约为 500x200（宽 x 高），但在窄屏幕上可能会水平裁剪。 + +## 11. 高级主题 + +### 自定义游戏 UI + +有一些选项可以自定义游戏内容的显示方式。这些可以使用 `Game.lean` 内的以下命令进行配置 + +``` +Settings + (unbundleHyps := true) + (anotherOption := false) +``` + +目前存在的选项有： + +* `unbundleHyps`（默认：`false`）：如果启用，显示两行 `A : Prop` 和 `B : Prop` 而不是单行 `A B : Prop`。 + +### Markdown + +文本通常应该支持 markdown。有关如何使用 markdown 的一些提示，请参见 +[Markdown 样式](../game-development/markdown.md)。 + +特别是，您可以在文本中嵌入图像，请参见该文件中的具体说明。 + +### 转义 + +在字符串内，您需要转义反斜杠，但在文档字符串内不需要，因此您会写 `Introduction "这里有一些 latex：$\\iff$。"` 但 + `/-- 这里有一些 latex：$\iff$。 -/ Statement ...` + +### LaTeX 支持 + +LaTeX 使用 [KaTeX 库](https://katex.org/) 渲染， +有关详细信息，请参见[在游戏中使用 LaTeX](../game-development/latex.md)。 + +### 关卡数量限制 + +超过 16 个关卡的世界将显示为关卡向外螺旋，最好保持在该界限以下。超过 22 个关卡，螺旋开始失控。 diff --git a/docs/zh/game-development/environment.md b/docs/zh/game-development/environment.md new file mode 100644 index 00000000..373f7654 --- /dev/null +++ b/docs/zh/game-development/environment.md @@ -0,0 +1,26 @@ +# 每个 lean 文件/关卡的设置 +在模板给出的示例中，`Metadata.lean` 将包含所有文件/关卡共同的设置，应该在每个 lean 文件的开头导入。 + +`Metadata.lean` 可以包含 `Mathlib`/`Lean` 导入、`theorem`、`axiom`。此外，`Metadata.lean` 可以分成多个具有类似设置的文件，其中 `Metadata.lean` 只是导入这些文件。这可以用来组织和隔离相关的内容。例如，一个文件包含 mathlib 导入，另一个包含定理、公理等。 + +# 公理 +在 `Metadata.lean` 中有公理，可以通过 `open namespace` 在 lean 文件中使用，其中 `namespace` 是声明公理的地方。但是，您需要执行 `NewTheorem namespace.axiom` 才能将其作为定理引入。 + +## 示例 +假设您在 `Metadata.lean` 中有以下内容， +``` +import Mathlib +namespace setup +axiom important_theorem : 2=2 +end setup +``` + +在关卡对应的 lean 文件中，您会有 +``` +... +-- 允许在 lean 文件中使用 +open setup + +-- 将其添加到游戏中 +NewTheorem setup.important_theorem +``` diff --git a/docs/zh/game-development/hints.md b/docs/zh/game-development/hints.md new file mode 100644 index 00000000..48ee0058 --- /dev/null +++ b/docs/zh/game-development/hints.md @@ -0,0 +1,100 @@ +# 提示 + +对于游戏开发来说，最重要的可能是"提示"。您可以使用 `Hint` 策略在证明的任何地方添加提示 + +``` +Statement .... := by + Hint "开始时显示的提示" + rw [h] + Hint "使用 rw 后的一些提示" + ... +``` + +注意提示只是**上下文感知但不是历史感知**。特别是，它们只查看假设和当前目标。如果玩家决定采用独特的证明思路，他们可能会以不同的顺序遇到提示 - 或者根本不会遇到。`Branch` 策略有助于在示例解决方案的证明之外放置提示。 + +## 1. 提示何时显示？ + +如果玩家的目标与示例解决方案中放置提示的目标匹配，并且示例解决方案的整个上下文都存在于玩家的上下文中，则会显示提示。玩家的上下文可能包含额外的证明。 + +这意味着如果您有多个相同的子目标，您应该只在其中一个中放置单个提示，它将在所有子目标中显示。 + +但是，在前一步中已经存在的相同（非隐藏）提示会被省略。这是为了允许玩家给证明添加新假设，例如使用 `have`，而不会一遍又一遍地看到相同的提示。隐藏提示不会被过滤。 + +## 2. 替代证明 / `Branch` + +您可以使用 `Branch` 在死胡同或替代证明分支中放置提示。 + +`Branch` 块内的证明通常由 lean 评估，但在最后被丢弃，因此在证明目标方面没有取得进展。 + +``` +Statement .... := by + Hint "使用 `rw` 或 `rewrite`。" + Branch + rewrite [h] + Hint "现在您仍然需要 `rfl`" + rw [h] +``` + +## 3. 变量名 + +将提示文本中的变量放在括号内，如：`{h}`！这样服务器可以将变量名替换为用户实际使用的名称。 + +*注意*：这意味着您需要转义任何其他**开放**大括号的使用（即 `\{`）。另请参见[游戏中的 LaTeX](latex.md) 的示例。 + +例如，如果示例证明包含 + +``` +have h : True := trivial +Hint "现在使用 `rw [{h}]` 来使用您的假设 `{h}`。" +``` + +但玩家写 `have g : True := trivial`，他们将看到提示说 +"现在使用 `rw [g]` 来使用您的假设 `g`。" + +## 4. 隐藏提示 + +一些提示可以被隐藏，只有在用户点击按钮获取额外帮助后才显示。您用 `(hidden := true)` 标记提示为隐藏： + +``` +Hint (hidden := true) "一些隐藏提示" +``` + +## 5. 严格上下文匹配 + +如果您使用属性 `(strict := true)`，只有当整个上下文与放置提示的位置完全匹配时才显示提示。使用 `(hint := false)`（这是默认值），玩家上下文中是否存在额外假设并不重要。 + +``` +Hint (strict := true) "现在使用 `have` 创建新假设。" +``` + +如果您想给出关于像 `have` 这样的策略的细粒度详细信息，您可能应该使用 `(strict := true)`，这些策略不修改目标或任何现有假设，只创建新假设。 + +## 6. 格式化 + +您可以使用 Markdown 格式化您的提示，也可以使用 LaTeX。有关更多详细信息，请参见[游戏中的 LaTeX](latex.md)。 + +### 图像 + +提示和介绍/结论也可以包含图像。 + +对于远程图像，只需添加： + +``` + +``` + +参见 https://www.jmilne.org/not/Mamscd.pdf + +### 图像 + +提示和介绍/结论也可以包含图像。 + +对于远程图像，只需添加： + +``` + +``` + +本地图像目前只能通过一个方法包含： + +游戏 `images/` 文件夹中的图像将在 `data/g/[user]/[repo]/[image].[png|jpg|…]` 处可访问，因此可以像外部图像一样包含它们。 diff --git a/docs/zh/game-development/latex.md b/docs/zh/game-development/latex.md new file mode 100644 index 00000000..bcb63357 --- /dev/null +++ b/docs/zh/game-development/latex.md @@ -0,0 +1,75 @@ +有多种方式可以格式化您游戏的文本内容。特别是使用 KaTeX 的 Markdown。 + +# 转义 +通常，如果您在引号 `" "` 内添加文本（例如在 `Hint` 中），您需要转义反斜杠，但如果您在文档注释 `/-- -/` 内提供文本（例如在 `Statement` 描述中），则不需要！ + +这意味着例如您会写 `"$\\iff$"` 而不是 `/-- $\iff$ -/`。 + +此外，在 `Hint` 内您需要将所有开放的大括号转义为 `\{`，因为 `{h}` 是插入变量名 `h` 的语法。 + +# KaTeX + +LaTeX 语法通过 [KaTeX 库](https://katex.org) 提供。KateX 支持大部分但不是全部的 latex 及其包。 +参见[支持的功能](https://katex.org/docs/supported.html)。 + +## 示例 + +### 交换图 + +以下是如何在 KaTeX 中编写交换图的示例： + +$$ +\begin{CD} + A @>{f}>> B @<{g}<< C \\ + @V{h}VV @V{i}VV @V{j}VV \\ + D @<{k}<< E @>{l}>> F \\ + @A{m}AA @A{n}AA @V{p}VV \\ + G @<{q}<< H @>{r}>> I +\end{CD} +$$ + +``` +$$ +\begin{CD} + A @>{f}>> B @<{g}<< C \\ + @V{h}VV @V{i}VV @V{j}VV \\ + D @<{k}<< E @>{l}>> F \\ + @A{m}AA @A{n}AA @V{p}VV \\ + G @<{q}<< H @>{r}>> I +\end{CD} +$$ +``` + +再次注意，在像 `Hint`/`Introduction`/`Conclusion`/等字符串内，您需要转义 `\` 和可能的 `{`。 + +例如 `\begin` 作为 `\\begin`，`\\` 作为 `\\\\`，在 `Hint` 内，`@>{f}>>` 作为 `@>\{f}>>`。 + +参见 https://www.jmilne.org/not/Mamscd.pdf + +### 真值表 + +KaTeX 不支持 tabular 环境。您可以使用 array 环境代替。 + +$$ +\begin{array}{|c|c|} + \hline + P & ¬P \\ + \hline + T & F \\ + F & T \\ + \hline +\end{array} +$$ + +``` +$$ +\begin{array}{|c|c|} + \hline + P & ¬P \\ + \hline + T & F \\ + F & T \\ + \hline +\end{array} +$$ +``` diff --git a/docs/zh/game-development/markdown.md b/docs/zh/game-development/markdown.md new file mode 100644 index 00000000..436065d7 --- /dev/null +++ b/docs/zh/game-development/markdown.md @@ -0,0 +1,22 @@ +# 游戏样式 + +您可以在所有文本中使用 Markdown 来应用样式。 + +## 图像 + +您可以通过将图像添加到游戏中的 `images/` 文件夹，然后使用以下方式添加图像到游戏中 + +``` +![alt_text](images/my_image.png) +``` + +（游戏服务器将自动为以 `images/` 开头的 URL 添加正确的 URL 前缀。） + +对于外部图像，您可以使用完整的 URL 添加它们： + +``` +![alt_text](https://www.example.com/path/to/my_image.png) +``` + +注意：`images/` 文件夹与用于世界介绍图像的文件夹相同。 +参见[创建游戏 > 6e](../game-development/create_game.md#6-e-额外图像) diff --git a/docs/zh/game-development/translate.md b/docs/zh/game-development/translate.md new file mode 100644 index 00000000..b2244226 --- /dev/null +++ b/docs/zh/game-development/translate.md @@ -0,0 +1,56 @@ +# 翻译 + +游戏服务器使用 [lean-i18n](https://github.com/hhu-adam/lean-i18n) 和 [i18next](https://www.npmjs.com/package/i18next) 支持国际化（"i18n"）。 + +目前预期的工作流程如下： + +1. 当您在游戏中调用 `lake build` 时，它应该自动创建模板文件 `.i18n/en/Game.pot`。或者您可以调用 `lake exe i18n --template` 来重新创建它。 +2. 使用 [Poedit](https://poedit.net/)（或类似软件）打开文件 `Game.pot`（"t" 代表 "template"）并翻译所有字符串。将您的工作保存为 `.i18n/{language}/Game.po`。 +4. 调用 `lake exe i18n --export-json` 创建服务器需要的所有 Json 文件 `.i18n/{language}/Game.json`。 +5. 添加您的翻译（即 `.po` 和 `.json`，但不包括 `.mo` 文件）并推送您的结果，然后[发布游戏](../getting-started/publish_game.md)。 + +如果您在游戏的"首选项"中选择正确的语言，应该能看到您的翻译。 + +## 详细信息（待合并） + +对于翻译，代码块（以一个或多个反引号（\`）开头）和 latex 块（以一个或两个 `$` 开头）将被占位符 `§n` 替换，您可以在注释中看到这些内容。 +此外，单个换行符（`\n`）将从翻译字符串中删除。 + +这些预处理步骤旨在改善与自动翻译工具的交互。 + +## 替代方案：避免 .po + +注意：此工作流程可能会发生变化，将来服务器可能能够直接读取 `.po` 文件。在那之前，您也可以选择另一种工作流程： + +0. 在 `.i18n/config.json` 中添加 `useJson: true` +1. `lake build` 或 `lake exe i18n --template` 现在将创建 Json：`.i18n/en/Game.json`。 +2. 将翻译添加到此 Json 的副本中并将其保存为 `.i18n/{language}/Game.json` + +## 非英语游戏 + +对于用英语以外的语言编写的游戏，您应该在 `.i18n/config.json` 中设置正确的源语言（`sourceLang`）。之后，在 `lake build` 时，模板应该出现在所选语言下，并可以如上所述进行翻译（例如翻译成英语）。 + +注意像 `pomerge` 这样的工具可能很有用：它允许您执行类似以下操作 + +``` +pomerge de-en.po en-fr.po -o de-fr.po +``` + +例如，您可以首先创建英语翻译，然后让人们将其翻译成他们自己的语言，最后使用 `pomerge` 从源语言到目标语言创建正确的 PO 文件。 + +## 新语言 + +服务器有一组可选择的语言。如果您的游戏已被翻译成不可选择的语言，请[在 lean4game 提问题](https://github.com/leanprover-community/lean4game/issues)请求这种新语言。 +或者，更好的是，创建 PR 将[服务器界面](https://github.com/leanprover-community/lean4game/tree/main/client/public/locales)翻译成那种新语言。 + +## 审查 + +由于此仓库（或游戏）的维护者可能不了解大多数语言，建议您从 Lean 社区中找到任何人来审查您的翻译并在 PR 上留下积极评论。 + +拥有来自社区的二级审查员的主要目的是防止错误翻译以及冒犯性或不当语言。 + +一些建议： + +1. JSON 文件是从 PO 文件自动生成的，因此可以进行表面审查。 +2. 翻译期间应保持格式。虽然代码片段有占位符，但审查员可能会注意标点符号等细节。 +3. [POEdit](https://poedit.net/) 是专门为翻译和审查过程设计的绝佳工具！除其他功能外，它允许您专门审查给定范围的句子，例如一次 50-100 句，并允许更容易地分配工作。 diff --git a/docs/zh/game-development/writing_exercises.md b/docs/zh/game-development/writing_exercises.md new file mode 100644 index 00000000..33e0d963 --- /dev/null +++ b/docs/zh/game-development/writing_exercises.md @@ -0,0 +1,70 @@ +# 编写练习 + +本页面更详细地介绍 `Statement` 命令以及您编写更好练习/关卡的所有选项。 + +## 描述性文本 +您可以编写一些在策略模式下出现在证明状态上方的文本： +``` +/-- 一些描述性文本 -/ +Statement my_statement ... +``` + +## 局部 `let` 定义 +如果您想创建一个仅对此练习有效的局部定义/记号（例如函数 `f : ℤ → ℤ := fun x ↦ 2 * x`），推荐的方法是使用 `let` 语句： + +```lean +Statement (a : ℤ) (h : 0 < a) : + let f : ℤ → ℤ := fun x ↦ 2 * x + 0 < f a := by + sorry +``` + +游戏会自动 `intros` 这样的 `let` 语句，这样您和玩家将看到以下初始证明状态： + +``` +a: ℤ +h: 0 < a +f: ℤ → ℤ := fun x => 2 * x +⊢ 0 < f a +``` + +## "前言" 和非 `Prop` 值练习 + +您可以使用以下语法 `(preamble := tac)`，其中 `tac` 是策略序列。 + +``` +Statement my_statement (preamble := dsimp) (a : ℤ) (h : 0 < a) : + 0 < f a := by + sorry +``` + +这个策略序列将在练习交给玩家之前执行。 + +例如，如果您的练习是构造一个结构，您可以使用 `preamble` 正确填充所有数据字段，将结构的所有 `Prop` 值字段作为单独的目标留给玩家证明。 + +注意：`(preamble := tac)` 总是必须写在可选名称和第一个假设之间。尽管如此，您可以在策略序列中使用所有假设，因为它只在证明开始时评估。 + +## 属性 + +您可以像对 `theorem` 一样添加属性。最值得注意的是，您可以使您的命名练习成为 `simp` 定理： + +```lean +@[simp] +Statement my_simp_theorem ... +``` + +## 格式化 + +您可以在引号内使用 markdown 进行格式化，如 `Hint ""`。也支持 Latex，请参见 latex.md。 + +## 将命名语句添加为定理 +可以这样做： +``` +Statement my_statement ... + +NewTheorem my_statement +``` +要在未来的关卡中使用 `my_statement`，您必须导入引入 `my_statement` 的关卡。 +`my_statement` 甚至在完成关卡之前就可以使用，但游戏足够智能，不允许您使用它来轻易解决关卡。它在关卡后可用，但确实作为定理出现在您的清单中。 + +您也可以避免使用命名语句，只创建一个普通的 `theorem` 并在下一关卡中使用 `NewTheorem`。 diff --git a/docs/zh/getting-started/publish_game.md b/docs/zh/getting-started/publish_game.md new file mode 100644 index 00000000..b046cca3 --- /dev/null +++ b/docs/zh/getting-started/publish_game.md @@ -0,0 +1,32 @@ +# 发布游戏 + +您可以通过几个简单的步骤在官方 [Lean 游戏服务器](https://adam.math.hhu.de) 上发布您的游戏。 + +## 1. 将游戏上传到 github + +首先，您需要将游戏放在公共 Github 仓库中，并确保 github action 已运行。 +可以通过在首页看到绿色勾号，或查看"Actions"标签来检查这一点。 + +## 2. 导入游戏 + +查看最新 action 日志，其中 "What's Next?" 标签列出的 URL。具体地说，调用形式为 + +> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY} + +其中 `{USER}` 和 `{REPOSITORY}` 替换为 github 用户和仓库名称。 + +打开网页应该会看到一个白色屏幕，显示导入更新并最终报告"Done." + +## 3. 玩游戏 + +现在您可以立即在 `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}` 玩游戏！ + +## 4. 更新 + +要上传游戏的新版本，每当您想发布更新版本时，您都必须重复步骤 1. 和 2.。 + +## 5. 主页 + +将游戏添加到主页由服务器维护者手动完成。如果您希望将游戏添加到主页中，请告诉我们！ + +例如，您可以[在 Zulip 上联系 Jon](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster)。 diff --git a/docs/zh/getting-started/running_locally.md b/docs/zh/getting-started/running_locally.md new file mode 100644 index 00000000..fe811e94 --- /dev/null +++ b/docs/zh/getting-started/running_locally.md @@ -0,0 +1,134 @@ +# 本地运行游戏 + +安装说明尚未在 Mac/Windows 上测试。非常欢迎您的意见反馈！ + +请同时参考[故障排除集合](troubleshoot.md)，其中收集了一些已知的问题。 + +有几种在本地运行游戏的选项： + +1. VSCode 开发容器：需要在您的机器上安装 `docker` +2. Codespaces：需要活跃的互联网连接，计算时间有限 +3. Gitpod：目前还不能正常运行（尚未确认？） +4. 手动安装：需要在您的系统上安装 `npm` + +推荐的选项是"VSCode 开发容器"，但您可以根据个人喜好选择上述任何选项。 + +模板游戏 [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) 包含所有相关文件，可以让您的本地设置（开发容器 / gitpod / codespaces）正常工作。如果您需要在已有游戏中开发新改进，您可以从这个仓库复制文件来手动更新。 + +## VSCode 开发容器 + +1. **安装 Docker 和开发容器** *(一次性)*：
+ 参见[官方说明](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started)。 + 具体来说，这意味着： + * 如果您还没有安装 docker 引擎：[安装说明](https://docs.docker.com/engine/install/)。 + 我在 linux 上遵循了"服务器"说明。 + * 注意在 Linux 上您需要将您的用户添加到 `docker` 组 + ([参见说明](https://docs.docker.com/engine/install/linux-postinstall/)) 并可能需要重启 shell。 + * 在 VSCode 中打开游戏文件夹：`cd NNG4 && code .` 或在 VSCode 中"打开文件夹" + * 会出现一条消息提示您安装"Dev Containers"扩展（由 Microsoft 提供）。（或者从 VSCode 扩展中安装它）。 + +2. **在开发容器中打开项目** *(每次)*：
+ 一旦您安装了开发容器扩展，在 VSCode 中（重新）打开您的游戏项目文件夹。会出现一条消息询问您是否"在容器中重新打开"。 + + * 第一次启动会花费一些时间，大约 2-15 分钟。第一次启动后，这应该会很快。 + * 构建完成后，您可以在浏览器中打开 http://localhost:3000，这应该会加载游戏。 + +3. **编辑文件** *(每次)*：
+ 在 VSCode 中编辑一些 Lean 文件后，打开 VSCode 的终端（视图 > 终端）并运行 `lake build`。现在您可以重新加载浏览器以查看更改。 + +## Codespaces + +您可以使用 Github codespaces 来处理您的游戏（点击仓库绿色按钮"Code"，然后"Codespaces"，然后"在 main 上创建 codespace"）。它应该在后台本地运行游戏。您可以在"Ports"下打开它，然后点击"在浏览器中打开"。 + +注意：您必须等到 npm 正确启动，这可能需要很长时间。 + +与开发容器一样，在更改任何 lean 文件后，您需要在运行 `lake build`，然后重新加载浏览器。 + +## Gitpod + +TODO：不确定这是否还能工作！ + +点击 gitpod 链接打开游戏。同样，您需要等到它完全构建完成，然后在您进行更改时在 shell 中输入 `lake build`。 + +## 手动安装 + +这会在您的计算机上手动安装 `lean4game`。（这与设置在线服务器的安装方式相同，只是运行命令（即 `npm start`）不同。） + +安装 `nvm`： +```bash +curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash +``` +然后重新打开 bash 并使用 `command -v nvm` 测试它是否可用（应该打印"nvm"）。 + +现在安装 node： +```bash +nvm install node +``` + +克隆游戏（例如这里的 `GameSkeleton`）： +```bash +git clone https://github.com/hhu-adam/GameSkeleton.git +# 或者：git clone git@github.com:hhu-adam/GameSkeleton.git +``` + +下载依赖项并构建游戏： +```bash +cd GameSkeleton +lake update -R +lake build +``` + +将服务器仓库克隆到游戏同级的目录中： +```bash +cd .. +git clone https://github.com/leanprover-community/lean4game.git +# 或者：git clone git@github.com:leanprover-community/lean4game.git +``` +文件夹 `GameSkeleton` 和 `lean4game` 必须在同一个目录中！ + +在 `lean4game` 中，安装依赖项： +```bash +cd lean4game +npm install +``` + +运行游戏： +```bash +npm start +``` + +您应该看到类似这样的消息： +```bash +[server] > lean4-game@0.1.0 start:server +[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs") +[server] +[client] +[client] > lean4-game@0.1.0 start:client +[client] > cross-env NODE_ENV=development vite --host +[client] +[server] [nodemon] 3.0.# +[server] [nodemon] to restart at any time, enter `rs` +[server] [nodemon] watching path(s): *.* +[server] [nodemon] watching extensions: mjs +[server] [nodemon] starting `node ./index.mjs` +[client] +[client] VITE v4.5.1 ready in \#\#\# ms +[client] +[client] ➜ Local: http://localhost:3000/ +[client] ➜ Network: http://###.###.###.##:3000/ +[client] [vite-plugin-static-copy] Collected 7 items. +[server] (node:#####) [DEP0040] [server] Listening on 8080 +``` + +这需要一点时间。最终，游戏将在 http://localhost:3000/#/g/local/GameSkeleton 上可用。将 `GameSkeleton` 替换为您本地游戏的文件夹名称。 + +## 修改 GameServer + +当修改游戏引擎本身（特别是 `lean4game/server` 中的内容）时，您可以使用与上述相同的设置（手动安装）通过使用 `lake update -R -Klean4game.local` 来实时测试它： + +```bash +cd NNG4 +lake update -R -Klean4game.local +lake build +``` +这可以让 lake 在本地搜索 `GameServer` 包，而不是使用 github 上的版本。因此，您可以编辑 `../lean4game` 中的本地 `GameServer` 副本，然后 `lake build` 将直接使用这个修改后的副本来构建您的游戏。 diff --git a/docs/zh/getting-started/troubleshoot.md b/docs/zh/getting-started/troubleshoot.md new file mode 100644 index 00000000..354c683e --- /dev/null +++ b/docs/zh/getting-started/troubleshoot.md @@ -0,0 +1,32 @@ +# 故障排除 + +以下是用户遇到的一些问题。 + +- 您可以使用以下命令重置涉及的 lake 项目（即这里的 `server/` 文件夹以及您的[游戏文件夹](https://github.com/hhu-adam/GameSkeleton)）： + ``` + cd [项目目录] + rm -rf .lake/ + lake update -R + lake build + ``` + 如果您遇到与 Lean 或 lake 相关的问题，您应该首先尝试以这种方式重置它。 + +# VSCode 开发容器 +* 如果您没有收到弹出窗口，您可能已经禁用了它们，您可以通过在 vscode 中运行 `remote-containers.showReopenInContainerNotificationReset` 命令来重新启用它。 +* 如果启动容器失败，特别是出现消息 `Error: network xyz not found`，您可能通过 shell 从 docker 中删除了一些内容。尝试在 VSCode 中明确删除容器和镜像（左侧，"Docker" 图标）。然后重新打开 vscode 并让它重建容器。（这将再次花费一些时间） +* 在正常工作的开发容器设置中，http://localhost:3000 应该直接重定向您到 http://localhost:3000/#/g/local/game，尝试看看后者是否可访问。 + +# 手动安装 +以下是使用 `npm` 进行本地设置的已知问题/陷阱。 + +* 如果在您的 mac/linux 系统上设置了 `CDPATH`，它可能会导致 `npm start` 出现问题，导致服务器崩溃或空白屏幕。特别是 `npm start` 将显示 + ``` + [server] sh: line 0: cd: server: No such file or directory + [server] npm run start:server exited with code 1 + ``` + 作为修复，您可能需要删除手动设置的 `CDPATH` 环境变量。 + +# 发布 +关于上传到服务器的错误。 + +* 您的游戏概览加载了，但服务器在加载关卡时崩溃：请检查您游戏的 github action 是否和 [GameSkeleton 的](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml) 雷同，特别是确保有一个关于构建 "`gameserver`-executable" 的步骤。 diff --git a/docs/zh/getting-started/update_game.md b/docs/zh/getting-started/update_game.md new file mode 100644 index 00000000..b4494db3 --- /dev/null +++ b/docs/zh/getting-started/update_game.md @@ -0,0 +1,49 @@ +# 如何更新您的游戏 + +## 新的 Lean 版本 + +您可以通过简单地编辑游戏仓库中的 `lean-toolchain` 来将游戏更新到任何 Lean 版本，使其包含新的 lean 版本 `leanprover/lean4:v4.X.0`。 + +在继续之前，请确保[此仓库中存在 `v4.X.0` 标签](https://github.com/leanprover-community/lean4game/tags)。 + +然后，根据您使用的设置，执行以下操作之一： + +* **Dev Container**：重建 VSCode Devcontainer（不使用缓存！）。 +* **本地设置**：在您的游戏文件夹中运行以下命令： + ``` + lake update -R + lake build + ``` + + * 此外，如果您有服务器 `lean4game` 的本地副本， + 您应该将其更新到匹配的版本。在文件夹 `lean4game/` 中运行以下命令： + ``` + git fetch + git checkout {VERSION_TAG} + npm install + ``` + 其中 `{VERSION_TAG}` 是上面形式为 `v4.X.0` 的标签 +* **Gitpod/Codespaces**：创建一个新的空间 + +这些操作可以把您的游戏（以及您可能使用的 mathlib 版本）更新到新的 lean 版本。 + +## 新的开发设置 + +您的游戏仓库中有一些用于开发设置的文件（dev container/codespaces/gitpod）。如果您需要更新这些设置，比如它不能正常运行，您需要将相关文件从 [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) 模板复制到您的游戏仓库中。 + +相关文件包括： + +``` +.devcontainer/ +.docker/ +.github/ +.gitpod/ +.vscode/ +lakefile.lean +``` + +只需将它们从 `GameSkeleton` 复制到您的游戏中，然后按上述方式进行， +即 `lake update -R && lake build`。 + +（注意：您不应该需要修改这些文件中的任何一个，除了 `lakefile.lean`， +您需要在其中添加游戏的任何依赖项，或者如果不需要 mathlib 则删除它。） diff --git a/docs/zh/index.md b/docs/zh/index.md new file mode 100644 index 00000000..73442648 --- /dev/null +++ b/docs/zh/index.md @@ -0,0 +1,62 @@ +# Lean 4 Game + +这是托管在 [adam.math.hhu.de](https://adam.math.hhu.de) 的 Lean 游戏平台的源代码。 + +## 创建游戏 + +请按照教程 [创建游戏](game-development/create_game.md) 进行操作。特别地，这几个步骤您可能会感兴趣： + +* 步骤 6：[如何在本地运行游戏](getting-started/running_locally.md) +* 步骤 8：[如何更新现有游戏](getting-started/update_game.md) +* 步骤 10：[如何发布游戏](getting-started/publish_game.md) +* [故障排除](getting-started/troubleshoot.md) + +## 文档 + +本文档仍在更新中，但这里链接的文档应该是最新的： + +### 游戏创建 API + +- [创建游戏](game-development/create_game.md)：**主要参考文档**。 +- [更多关于提示的信息](game-development/hints.md)：描述 `Hint` 和 `Branch` 策略。 + +### 前端 API + +* [如何在本地运行游戏](getting-started/running_locally.md)：在您的计算机上玩游戏 +* [如何更新现有游戏](getting-started/update_game.md)：更新到新的 lean 版本 +* [如何发布游戏](getting-started/publish_game.md)：将您的游戏加载到 adam.math.hhu.de 供其他人玩 + +### 后端 + +尚未完全编写。 + +* [服务器](server-deployment/DOCUMENTATION.md)：描述服务器部分（即 `server/` 和 `relay/` 的内容）。 + +## 贡献 + +欢迎对 `lean4game` 做出贡献！ + +### 翻译 + +游戏支持翻译成各种语言。如果要添加翻译，需执行以下操作： + +1. 在 `client/src/config.json` 中，添加您的新语言。"iso" 键是 ISO 语言代码，取值为 "i18next" 或 "GNU gettext"；"flag" 键应该符合 [react-country-flag](https://www.npmjs.com/package/react-country-flag) 的格式。 +2. 运行 `npm run translate`。这将创建一个新文件 `client/public/locales/{language}/translation.json`。（或者您可以复制粘贴 `client/public/locales/en/translation.json`） +3. 添加所有翻译内容。 +4. 提交您对 `config.json` 所做的更改以及新的 `translation.json`。 + +有关翻译游戏，请参阅 [翻译游戏](game-development/translate.md)。 + +## 安全性 + +为用户提供对服务器上运行的 Lean 实例的访问是一个严重的安全风险。这就是为什么我们使用 bubblewrap 启动 Lean 服务器的原因。 + +## 联系方式 + +如果在使用 ```adam.math.hhu.de``` 时遇到技术问题，请通过 电子邮件 联系我们。 + +## 致谢 + +该项目主要由 Alexander Bentkamp 和 Jon Eugster 开发。 + +它基于 [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) 和 [Natural Number Game (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) 的想法，后者由 Kevin Buzzard 和 Mohammad Pedramfar 开发，以及 Patrick Massot 的原型：[NNG4](https://github.com/PatrickMassot/NNG4)。 diff --git a/docs/zh/server-deployment/DOCUMENTATION.md b/docs/zh/server-deployment/DOCUMENTATION.md new file mode 100644 index 00000000..0523979c --- /dev/null +++ b/docs/zh/server-deployment/DOCUMENTATION.md @@ -0,0 +1,47 @@ +# 服务器 + +服务器由两个部分组成，分别命名为 "relay" 和 "server"。 + +前者 "relay" 是负责与客户端建立 socket 连接、启动 lean 服务器处理文件并在 lean 服务器和客户端之间中继消息的服务器。`index.mjs` 是需要运行的文件，例如使用 `pm2` 或调用 `npm run start:server` 或 `npm run production`，稍后会详细介绍。 + +后者 "server" 是 lean 服务器，有两个职责。首先，它生成 "gameserver" 可执行文件，这是处理玩家游玩文件的 lean 服务器。第二个职责是提供创建游戏时使用的 lean 命令。这些命令位于 `Commands.lean` 中。 + + +## 集成到游戏中 + +游戏需要将 "server" 作为 lake 依赖项，这主要添加在游戏的 lakefile 文件。 + +游戏导入 `GameServer`，它提供创建游戏所需的所有 API。 + +特别是 lean 命令 `MakeGame` 编译整个游戏。静态信息作为 JSON 文件存储在 `.lake/gamedata` 中以便更快加载，而其他数据仅保存到 lean env-extensions 中，lean 服务器在加载 lean 文件后可以访问这些数据。 + +为了成功运行游戏，关键是构建游戏仓库 `.lake` 文件夹内的 "gameserver" 可执行文件。目前，这通过在调用 `lake update -R`（在游戏文件夹中）时的 lake-post-update-hook 实现，但如果失败，您总是可以通过调用 `lake build gameserver` 手动构建它。（两个命令都要在游戏目录中执行！） + +## 修改服务器 + +### 启动服务器 + +当使用[手动安装](../getting-started/running_locally.md#manual-installation)时，您可以使用以下命令运行服务器： + +``` +npm start +``` + +这样，对 `client/` 或 `relay/` 中文件的任何更改都会导致服务器自动重启。 + +或者，您可以运行 `npm run build` 然后运行以下命令： + +``` +npm run start:client +npm run production +``` + +（在两个单独的终端中）来测试服务器的生产模式。这样它只会在您构建和重启服务器时发生更改。 + +### 修改 lean 服务器 + +要测试修改的 lean 服务器（即 `server/` 的内容），您可以使用本地开发设置并在您的游戏中调用 `lake update -R -Klean4game.local`，然后调用 `lake build`。这将使得 lake 寻找本地 lean 包作为依赖项，而不是从 git 下载的版本。 + +您可以在 https://localhost:3000/#/g/local/{FolderName} 玩本地游戏，其中您将 `{FolderName}` 替换为游戏文件夹名称。 + +在 `server/` 中修改后，您需要调用 `lake build gameserver`（在 `server/` 或游戏文件夹中调用）来重建 gameserver 可执行文件，并调用 `lake build`（在游戏文件夹中调用）来重建游戏。 diff --git a/docs/zh/server-deployment/client.md b/docs/zh/server-deployment/client.md new file mode 100644 index 00000000..d7d7792b --- /dev/null +++ b/docs/zh/server-deployment/client.md @@ -0,0 +1,7 @@ +# 客户端 + +本文档描述前端/客户端的功能。 + +## URL + +您可以在 URL 末尾添加 `?lang=de` 来指定应该设置的语言。这将把用户的首选语言更改为指定的语言。 diff --git a/docs/zh/server-deployment/npm_scripts.md b/docs/zh/server-deployment/npm_scripts.md new file mode 100644 index 00000000..8048e972 --- /dev/null +++ b/docs/zh/server-deployment/npm_scripts.md @@ -0,0 +1,17 @@ +## NPM 脚本 + +* `npm start`：以开发模式启动项目。当客户端文件发生更改时，浏览器将自动重新加载。当 lean 文件发生更改时，Lean 服务器将被重新编译和重启。此时 Lean 服务器的启动将不依赖容器。客户端和服务器分别使用脚本 `npm run start:client` 和 `npm run start:server` 启动，并通过 `http://localhost:3000` 访问项目。在内部，到 `ws://localhost:3000/websockets` 的 websocket 请求将被转发到运行在端口 `8080` 上的 Lean 服务器。 + +* `npm run build`：以生产模式构建项目。对于客户端，所有文件将被编译到 `client/dist` 中。对于服务器端，该命令将设置一个包含 Lean 服务器的 docker 镜像。这两个部分可以使用 `npm run build:client` 和 `npm run build:server` 分别构建。 + +* `npm run production`：以生产模式启动项目。这需要先运行构建脚本。它将在 `PORT` 环境变量指定的端口上启动服务器，或默认在 `8080` 上启动。您可以通过运行 `PORT=80 npm run production` 在特定端口上运行。服务器将通过 http 提供 `client/dist` 中的文件，并通过 web socket 协议提供对 bubblewrapped Lean 服务器的访问。 + +### 环境变量 + +客户端和服务器端口以及默认语言可以使用环境变量配置： + +* `PORT`：设置后端服务器的端口（默认：`8080`）。 +* `CLIENT_PORT`：设置客户端服务器的端口（默认：`3000`）。 +* `VITE_CLIENT_DEFAULT_LANGUAGE`：设置应用程序的默认语言（默认：`en`）。 + +确保在您的环境中适当设置这些环境变量，以根据需要配置项目。 diff --git a/docs/zh/server-deployment/server.md b/docs/zh/server-deployment/server.md new file mode 100644 index 00000000..6cf115b0 --- /dev/null +++ b/docs/zh/server-deployment/server.md @@ -0,0 +1,38 @@ +# 服务器维护者注意事项 + +为了设置服务器以允许导入，需要创建一个 +[Github 访问令牌](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens)。一个仅具有公共仓库读取权限的细粒度访问令牌就足够了。 + +您需要设置环境变量 `LEAN4GAME_GITHUB_USER` 和 `LEAN4GAME_GITHUB_TOKEN`，包含您的用户名和访问令牌。例如，如果您使用 `pm2`，可以在 `ecosystem.config.cjs` 中设置这些。 + +然后人们可以调用： + +> https://{website}/import/trigger/{owner}/{repo} + +其中您需要替换： +- website：您的服务器运行的网站，例如 `localhost:3000` +- owner, repo：您想从 github 加载的游戏的所有者和仓库名称。 + +这将触发从 github 下载您游戏的最新版本到您的服务器。一旦此导入报告"Done"，您应该能够在以下位置玩您的游戏： + +> https://{website}/#/g/{owner}/{repo} + +## 数据管理 +所有下载的内容都保留在文件夹 `lean4game/games` 中。子文件夹 `tmp` 包含下载的工件，可以放心删除。其他文件夹应该只包含构建的 lean 游戏，按所有者和仓库排序。 + +## 服务器容量 + +如果您想在首页显示服务器容量，您可以创建一个形式如下的文件 `lean4game/games/stats.csv`： + +``` +CPU,MEM +0.1,0.8 +``` + +这些数字将显示在首页（"CPU: 10 % used" 和 "RAM: 80 % used"）。 + +如果您只想要其中一个数字，请将您不想要的数字替换为 `nan`（或任何其他不能解析为数字的内容）。 + +如果您不想显示任何一个，只需不创建 `stats.csv` + +使用您自己的脚本或 cronjob 根据需要更新 CSV 文件。 diff --git a/mkdocs.yml b/mkdocs.yml new file mode 100644 index 00000000..fe8426dd --- /dev/null +++ b/mkdocs.yml @@ -0,0 +1,134 @@ +site_name: Lean4Game Documentation +site_description: Interactive Lean 4 Game Platform - Create and Play Mathematical Proof Games +site_author: Lean Community +site_url: https://leanprover-community.github.io/lean4game/ + +repo_name: leanprover-community/lean4game +repo_url: https://github.com/leanprover-community/lean4game +edit_uri: edit/main/docs/ + +docs_dir: docs/ + +theme: + name: material + palette: + - scheme: default + primary: indigo # 换个主题 + accent: indigo + toggle: + icon: material/brightness-7 + name: Switch to dark mode + - scheme: slate + primary: indigo + accent: indigo + toggle: + icon: material/brightness-4 + name: Switch to light mode + features: + - navigation.tabs + - navigation.sections + - navigation.expand + - navigation.top + - navigation.prune + - search.highlight + - search.share + - content.code.copy + - content.code.annotate + - content.action.edit + - content.action.view + language: en + +plugins: + - search + - i18n: + docs_structure: folder + fallback_to_default: true + reconfigure_material: true + reconfigure_search: true + languages: + - locale: en + default: true + name: English + build: true + site_name: "Lean4Game Documentation" + - locale: zh + name: 中文 + build: true + site_name: "Lean4Game 文档" + nav_translations: + Home: 首页 + Getting Started: 快速开始 + Game Development: 游戏开发 + Server & Deployment: 服务器与部署 + Reference: 参考文档 + Running Locally: 本地运行 + Creating a Game: 游戏创建 + Troubleshooting: 故障排除 + Writing Exercises: 编写练习 + Hints System: 提示系统 + Environment Setup: 环境设置 + LaTeX Support: LaTeX 支持 + Markdown Features: Markdown 功能 + Translation: 翻译 + Server Architecture: 服务器架构 + Server Configuration: 服务器配置 + Client Features: 客户端功能 + Publishing Games: 发布游戏 + Updating Games: 更新游戏 + NPM Scripts: NPM 脚本 + Changelog: 变更日志 + +markdown_extensions: + - pymdownx.highlight: + anchor_linenums: true + - pymdownx.superfences: + custom_fences: + - name: mermaid + class: mermaid + format: !!python/name:pymdownx.superfences.fence_code_format + - pymdownx.tabbed: + alternate_style: true + - admonition + - pymdownx.details + - pymdownx.snippets + - attr_list + - md_in_html + - tables + - pymdownx.emoji: + emoji_index: !!python/name:material.extensions.emoji.twemoji + emoji_generator: !!python/name:material.extensions.emoji.to_svg + - pymdownx.tasklist: + custom_checkbox: true + +extra: + alternate: + - name: English + link: /lean4game/ + lang: en + - name: 中文 + link: /lean4game/zh/ + lang: zh + social: + - icon: fontawesome/brands/github + link: https://github.com/leanprover-community/lean4game +nav: + - Home: index.md + - Getting Started: + - Running Locally: getting-started/running_locally.md + - Updating Games: getting-started/update_game.md + - Publishing Games: getting-started/publish_game.md + - Troubleshooting: getting-started/troubleshoot.md + - Changelog: changelog.md + - Game Development: + - Creating a Game: game-development/create_game.md + - Writing Exercises: game-development/writing_exercises.md + - Hints System: game-development/hints.md + - Environment Setup: game-development/environment.md + - LaTeX Support: game-development/latex.md + - Markdown Features: game-development/markdown.md + - Translation: game-development/translate.md + - Server & Deployment: + - Server Architecture: server-deployment/DOCUMENTATION.md + - Server Configuration: server-deployment/server.md + - Client Features: server-deployment/client.md + - NPM Scripts: server-deployment/npm_scripts.md