phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update DOCUMENTATION.md #111

Browse Source
This commit is contained in:
Jon Eugster
2023-10-09 11:23:47 +02:00
committed by joneugster
parent b2936e0200
commit 0b1fe3baf1
1 changed files with 15 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files
DOCUMENTATION.md
+15 -13
View File
@@ -194,7 +194,7 @@ There will be features added to get automatic information from mathlib!
Inside the doc comment you don't need to escape the backslashes: Inside the doc comment you don't need to escape the backslashes:
``` ```lean
/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/ /-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
Statement ... Statement ...
``` ```
@@ -203,7 +203,7 @@ However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclu
you do need to escape backslashes you do need to escape backslashes
with `\\` and `{` with `\{`: with `\\` and `{` with `\{`:
``` ```lean
Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}. Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
Notation for naturals is `\\N`." Notation for naturals is `\\N`."
``` ```
@@ -250,23 +250,24 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
## Without Dev Containers ## Without Dev Containers
Install `nvm`: Install `nvm`:
``` ```bash
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
``` ```
then reopen bash and test with `command -v nvm` if it is available (Should print "nvm"). then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
Now install node: Now install node:
``` ```bash
nvm install node nvm install node
``` ```
Clone the game (e.g. `NNG4` here): Clone the game (e.g. `NNG4` here):
``` ```bash
git clone git@github.com:hhu-adam/NNG4.git git clone https://github.com/hhu-adam/NNG4.git
# or: git clone git@github.com:hhu-adam/NNG4.git
``` ```
Download dependencies and build the game: Download dependencies and build the game:
``` ```bash
cd NNG4 cd NNG4
lake update lake update
lake exe cache get # if your game depends on mathlib lake exe cache get # if your game depends on mathlib
@@ -274,21 +275,22 @@ lake build
``` ```
Clone the game repository into a directory next to the game: Clone the game repository into a directory next to the game:
``` ```bash
cd .. cd ..
git clone git@github.com:leanprover-community/lean4game.git git clone hhttps://github.com/leanprover-community/lean4game.git
# or: git clone git@github.com:leanprover-community/lean4game.git
``` ```
The folders `NNG4` and `lean4game` must be in the same directory! The folders `NNG4` and `lean4game` must be in the same directory!
In `lean4game`, install dependencies: In `lean4game`, install dependencies:
``` ```bash
cd lean4game cd lean4game
npm install npm install
``` ```
If you are developing a game other than `Robo` or `NNG4`, adapt the If you are developing a game other than `Robo` or `NNG4`, adapt the
code at the beginning of `lean4game/server/index.mjs`: code at the beginning of `lean4game/server/index.mjs`:
``` ```typescript
const games = { const games = {
"g/hhu-adam/robo": { "g/hhu-adam/robo": {
dir: "../../../../Robo", dir: "../../../../Robo",
@@ -302,7 +304,7 @@ const games = {
``` ```
Run the game: Run the game:
``` ```bash
npm start npm start
``` ```
@@ -314,7 +316,7 @@ and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
setup by setting `export NODE_ENV=development` inside your local game before building it: setup by setting `export NODE_ENV=development` inside your local game before building it:
``` ```bash
cd NNG4 cd NNG4
export NODE_ENV=development export NODE_ENV=development
lake update lake update