ac9a60d137
Provides flake.nix with nix run, nix develop, and nix build commands. Automatically sets up lean4game platform and starts game server at http://localhost:3000. See FLAKE_USAGE.md for complete documentation. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
43 lines
1.9 KiB
Markdown
43 lines
1.9 KiB
Markdown
# NNG4
|
|
|
|
This is the lean4 version of the classical *Natural Number Game*. It uses
|
|
the [Lean4 Game Engine](https://github.com/leanprover-community/lean4game) and is
|
|
running live at [adam.math.hhu.de](https://adam.math.hhu.de).
|
|
|
|
The game was initially designed for lean3 and has been adapted for lean4. [See lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/).
|
|
|
|
## Getting Started
|
|
|
|
You can develop the game as any lean project and use `lake build` to build it.
|
|
|
|
Moreover, there are multiple ways to run the game while developing it, which are described in
|
|
[Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
|
|
|
|
### Nix Flake
|
|
|
|
If you use Nix, you can run the game locally without Docker or VSCode:
|
|
|
|
```bash
|
|
nix run # Start the game server at http://localhost:3000
|
|
```
|
|
|
|
See [FLAKE_USAGE.md](./FLAKE_USAGE.md) for complete documentation.
|
|
|
|
## Contributing
|
|
|
|
PRs/Issues fixing typos, inconsistencies, missing hints, etc. are very welcome!
|
|
|
|
### Translations
|
|
We happily accept translations of the game into different languages! You can use `.i18n/en/Game.pot` and translate it into `.i18n/{lang}/Game.po` where `{lang}` is the ISO language code like `fr` or `en_UK`, using for example POEdit.
|
|
|
|
We would like the following requirements for a translation PR:
|
|
|
|
- One independent person from the community, who understands the language, gives a review on the PR. You could for example look at the [Lean Community Map](https://leanprover-community.github.io/meet.html) or ask on Zulip. Such a review can be quite generic and does not have to be super detailed.
|
|
- In the credits (i.e. in the string translating them), ideally you should add yourself as a translator for this language.
|
|
|
|
## Documentation
|
|
|
|
See [Creating a Game](https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md) at
|
|
the [lean4game repo](https://github.com/leanprover-community/lean4game) for a detailed
|
|
explanation.
|