From 892c70165a9ac03f8a099f4527cd055dbb58540c Mon Sep 17 00:00:00 2001 From: Luke Naylor Date: Fri, 12 Jan 2024 21:07:19 +0000 Subject: [PATCH 01/12] Minor: correct error in markdown --- doc/publish_game.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/publish_game.md b/doc/publish_game.md index 1afd3d9..368d299 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -1,6 +1,6 @@ # Publishing games -You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple +You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple steps. ## 1. Upload Game to github From 7114a8c4cb297b169adb499dd730312ea4ebb025 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 15 Jan 2024 12:15:03 +0100 Subject: [PATCH 02/12] fix: remove tmp files after import --- relay/unpack.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/relay/unpack.sh b/relay/unpack.sh index b475847..83b3b2e 100755 --- a/relay/unpack.sh +++ b/relay/unpack.sh @@ -28,3 +28,7 @@ do #tar -xvzf $f -C games/${OWNER}/${REPO} unzip -q -o $f -d ${OWNER}/${REPO} done + +# Delete temporary files +rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip +rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID} From c533a635c2469007f745caef1a063c5f1012beb6 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Jan 2024 13:47:08 +0100 Subject: [PATCH 03/12] Update docs --- doc/running_locally.md | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/doc/running_locally.md b/doc/running_locally.md index 5ab890f..5b73b8f 100644 --- a/doc/running_locally.md +++ b/doc/running_locally.md @@ -2,6 +2,8 @@ The installation instructions are not yet tested on Mac/Windows. Comments very welcome! +Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected. + There are several options to play a game locally: 1. VSCode Dev Container: needs `docker` installed on your machine @@ -36,16 +38,6 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta 3. **Editing Files** *(everytime)*:
After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes. -### Errors - -* If you don't get the pop-up, you might have disabled them and you can reenable it by - running the `remote-containers.showReopenInContainerNotificationReset` command in vscode. -* If the starting the container fails, in particular with a message `Error: network xyz not found`, - you might have deleted stuff from docker via your shell. Try deleting the container and image - explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the - container. (this will again take some time) -* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible. - ## Codespaces You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser". From cc89e78e4c173b8e9e387d3c6ed848b8a05f1595 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Jan 2024 13:47:16 +0100 Subject: [PATCH 04/12] Create troubleshoot.md --- doc/troubleshoot.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 doc/troubleshoot.md diff --git a/doc/troubleshoot.md b/doc/troubleshoot.md new file mode 100644 index 0000000..4044759 --- /dev/null +++ b/doc/troubleshoot.md @@ -0,0 +1,23 @@ +# Troubleshooting + +Here are some issues experienced by users. + +# VSCode Dev-Container +* If you don't get the pop-up, you might have disabled them and you can reenable it by + running the `remote-containers.showReopenInContainerNotificationReset` command in vscode. +* If the starting the container fails, in particular with a message `Error: network xyz not found`, + you might have deleted stuff from docker via your shell. Try deleting the container and image + explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the + container. (this will again take some time) +* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible. + + +# Manual Installation +Here are known issues/pitfalls with the local setup using `npm`. + +* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display + ``` + [server] sh: line 0: cd: server: No such file or directory + [server] npm run start_server exited with code 1 + ``` + As a fix you might need to delete your manually set `CDPATH` environment variable. From 20ca385e143b15f5f822cc851ae638526a281214 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Jan 2024 13:48:43 +0100 Subject: [PATCH 05/12] Update README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index db97d97..2661d9f 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,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) +* [Troubleshooting](doc/troubleshoot.md) ## Documentation From 16ff7015187c5508bdabc5ab0d9a0ffa72a892f5 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Jan 2024 13:51:33 +0100 Subject: [PATCH 06/12] Update troubleshoot.md --- doc/troubleshoot.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/doc/troubleshoot.md b/doc/troubleshoot.md index 4044759..5171a75 100644 --- a/doc/troubleshoot.md +++ b/doc/troubleshoot.md @@ -21,3 +21,8 @@ Here are known issues/pitfalls with the local setup using `npm`. [server] npm run start_server exited with code 1 ``` As a fix you might need to delete your manually set `CDPATH` environment variable. + +# Publication +Errors concerning uploads to the server. + +* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable". From bfb60ffeddf3bdb076c30c20dc9f055e5a3f6ed4 Mon Sep 17 00:00:00 2001 From: geo Date: Fri, 19 Jan 2024 10:41:20 -0500 Subject: [PATCH 07/12] Updated "Doc entries" --- doc/create_game.md | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/doc/create_game.md b/doc/create_game.md index 31d34d9..0b32f57 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -98,7 +98,7 @@ This introduction text is shown when one first enters a world. 1. Use the template above and make sure you import all levels of this world. 1. In `Game.lean` import the world with `import Game.Levels.MyWorld` -Now you created a world with one level and added itπŸŽ‰ The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows +Now you created a world with one level and added itπŸŽ‰ The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently, it shows ```text No world introducing sorry, but required by MyWorld @@ -125,26 +125,32 @@ The player has an inventory with tactics, theorems, and definitions that unlock ```lean NewTactic induction simp -NewLemma Nat.zero_mul +NewTheorem Nat.zero_mul NewDefinition Pow ``` **Important:** All commands in this section 6a) expect the `Name` they take as input -to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`. +to be **fully qualified**. For example `NewTheorem Nat.zero_mul` and not `NewTheorem zero_mul`. #### Doc entries -You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it. +You'll see a warning about a missing Theorem documentation. You can fix it by adding doc-entries like the following somewhere above it. ```lean -LemmaDoc Nat.zero_mul as "zero_mul" in "Mul" -"some description" - +/-- +some description +-/ +TheoremDoc Nat.zero_mul as "zero_mul" in "Mul" + +/-- +some description +-/ TacticDoc simp -"some description" +/-- +some description +-/ DefinitionDoc Pow as "^" -"some description" ``` (e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it) @@ -156,7 +162,7 @@ If you do not provide any content for the inventory, the game will try to find a You have a few options to disable inventory items that have been unlocked in previous levels: ```lean -DisableTactic, DisableLemma, OnlyTactic, OnlyLemma +DisabledTactic, DisabledTheorem, OnlyTactic, OnlyTheorem ``` have the same syntax as above. The former two disable items for this level, the latter two @@ -164,7 +170,7 @@ disable all items except the ones specified. #### Theorem Tab -Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level. +Theorems are sorted into tabs. With `TheoremTab "Mul"` you specify which tab should be open by default in this level. #### HiddenTactic @@ -179,7 +185,7 @@ and only `rw` would show up in the inventory. ### 6. b) Statement -The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax +The statement is the exercise of the level. The basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax #### Name @@ -210,7 +216,7 @@ Statement my_simp_lemma ... The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax. -There are a few extra tactics that help you structuring the proof: +There are a few extra tactics that help you with structuring the proof: - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches the one where `Hint` is placed. For more options about hints, see below. From 03076b01614d7c605cd14913913ad5551e9787e3 Mon Sep 17 00:00:00 2001 From: geo Date: Fri, 19 Jan 2024 10:52:26 -0500 Subject: [PATCH 08/12] Add example `npm start` message --- doc/running_locally.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/doc/running_locally.md b/doc/running_locally.md index 5b73b8f..390a025 100644 --- a/doc/running_locally.md +++ b/doc/running_locally.md @@ -100,6 +100,29 @@ Run the game: npm start ``` +You should see a message like this: +```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 +``` + This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game. ## Modifying the GameServer From 49379a0930e85b9661936ccdc69da14690f97e5a Mon Sep 17 00:00:00 2001 From: geo Date: Sat, 20 Jan 2024 16:02:46 -0500 Subject: [PATCH 09/12] Fix link references --- doc/create_game.md | 6 +++--- doc/running_locally.md | 6 +++--- doc/server.md | 4 ++-- doc/troubleshoot.md | 4 ++-- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/doc/create_game.md b/doc/create_game.md index 0b32f57..e3caf07 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -236,7 +236,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](doc/hints.md) for how they work and what the options are. +Read [More about Hints](hints.md) for how they work and what the options are. ### 6. 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. @@ -248,11 +248,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the ## 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](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](update_game.md). ## 8. Publish your game -To publish your game on the official server, see [Publishing a game](doc/publish_game.md) +To publish your game on the official server, see [Publishing a game](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: diff --git a/doc/running_locally.md b/doc/running_locally.md index 390a025..2a044fd 100644 --- a/doc/running_locally.md +++ b/doc/running_locally.md @@ -2,7 +2,7 @@ The installation instructions are not yet tested on Mac/Windows. Comments very welcome! -Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected. +Please also consult the [Troubleshooting Collection](troubleshoot.md), where some known pitfalls are collected. There are several options to play a game locally: @@ -33,14 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta * The first start will take a while, ca. 2-15 minutes. After the first start this should be very quickly. - * Once built, you can open http://localhost:3000 in your browser. which should load the game. + * Once built, you can open http://localhost:3000 in your browser, which should load the game. 3. **Editing Files** *(everytime)*:
After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes. ## Codespaces -You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser". +You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser". Note: You have to wait until npm started properly, which might take a good while. diff --git a/doc/server.md b/doc/server.md index 41698a0..e706e47 100644 --- a/doc/server.md +++ b/doc/server.md @@ -6,7 +6,7 @@ In order to set up the server to allow imports, one needs to create a 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 +with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if you're using `pm2` Then people can call: @@ -24,5 +24,5 @@ where you replace: ## data management Everything downloaded remains in the folder `lean4game/games`. -the subfolder `tmp` contains downloaded artifacts and can be deleted without loss. +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. diff --git a/doc/troubleshoot.md b/doc/troubleshoot.md index 5171a75..8254d1d 100644 --- a/doc/troubleshoot.md +++ b/doc/troubleshoot.md @@ -3,11 +3,11 @@ Here are some issues experienced by users. # VSCode Dev-Container -* If you don't get the pop-up, you might have disabled them and you can reenable it by +* If you don't get the pop-up, you might have disabled them, and you can reenable it by running the `remote-containers.showReopenInContainerNotificationReset` command in vscode. * If the starting the container fails, in particular with a message `Error: network xyz not found`, you might have deleted stuff from docker via your shell. Try deleting the container and image - explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the + explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the container. (this will again take some time) * On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible. From c006be5a9f7b4045c66b5bdb493e320f9465517f Mon Sep 17 00:00:00 2001 From: geo Date: Sat, 20 Jan 2024 16:15:15 -0500 Subject: [PATCH 10/12] Fix minor typos --- .vscode/ltex.dictionary.en-US.txt | 7 +++++++ doc/DOCUMENTATION.md | 6 +++--- doc/create_game.md | 4 ++-- doc/hints.md | 8 ++++---- doc/publish_game.md | 2 +- doc/server.md | 2 +- 6 files changed, 18 insertions(+), 11 deletions(-) create mode 100644 .vscode/ltex.dictionary.en-US.txt diff --git a/.vscode/ltex.dictionary.en-US.txt b/.vscode/ltex.dictionary.en-US.txt new file mode 100644 index 0000000..c1cff73 --- /dev/null +++ b/.vscode/ltex.dictionary.en-US.txt @@ -0,0 +1,7 @@ +GameSkeleton +HiddenTactic +subgoals +KaTex +gameserver +lakefile +Zulip diff --git a/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md index 2364920..153756d 100644 --- a/doc/DOCUMENTATION.md +++ b/doc/DOCUMENTATION.md @@ -8,7 +8,7 @@ relays messages between the lean server and the client. `index.mjs` is the file be run, which is done for example using `pm2` or by calling `npm run start_server` or `npm run production`, see more later. -The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver" +The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver" executable which is the lean server that handles the files the player plays on. The second job is to provide the lean commands which are used when creating a game. These are located in `Commands.lean`. @@ -27,7 +27,7 @@ saved to lean env-extensions which the lean server has access to after loading t For games to be run successfully, it is important that the "gameserver" executable inside the game's `.lake` folder is actually built. -Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`. +Currently, this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`. (both commands are to be executed in the game's directory!) ## Modifying the server @@ -50,7 +50,7 @@ npm run start_client npm run production ``` -(in two separate terminals) to test the production modus of the server. This way it will only +(in two separate terminals) to test the production modes of the server. This way it will only change once you build and restart the server. ### Modifying the lean server diff --git a/doc/create_game.md b/doc/create_game.md index e3caf07..0fc347f 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -221,7 +221,7 @@ There are a few extra tactics that help you with structuring the proof: - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches the one where `Hint` is placed. For more options about hints, see below. - `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which - helps setting `Hints` in different places. The `Branch` does not affect the main + helps to set `Hints` in different places. The `Branch` does not affect the main proof and does not need to finish any goals. - `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template` will be copied into the editor with all `Hole`s replaced with `sorry`. Note that @@ -264,7 +264,7 @@ Prerequisites "NNG" CoverImage "images/cover.png" ``` * `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag. -* `CaptionShort`: One catch phrase. Appears above the image. +* `CaptionShort`: One catchphrase. Appears above the image. * `CaptionLong`: 2-4 sentences to describe the game. * `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text. * `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens. diff --git a/doc/hints.md b/doc/hints.md index 591edb1..9e3a937 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -10,7 +10,7 @@ Statement .... := by ... ``` -Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof. +Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof. ## 1. When do hints show? @@ -19,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in player's context. The player's context may contain additional items. This means if you have multiple identical -subgoals, you should only place a single hint in one of them and it will be displayed in +subgoals, you should only place a single hint in one of them, and it will be displayed in all of them. However, identical (non-hidden) hints which where already present in the step @@ -32,12 +32,12 @@ Hidden hints are not filtered. You can use `Branch` to place hints in dead ends or alternative proof strands. -A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end +A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end so that no progress has been made on proofing the goal. ``` Statement .... := by - Hint "Huse `rw` or `rewrite`." + Hint "use `rw` or `rewrite`." Branch rewrite [h] Hint "now you still need `rfl`" diff --git a/doc/publish_game.md b/doc/publish_game.md index 368d299..bd017fe 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -11,7 +11,7 @@ tab. ## 2. Import the game -You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call +You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call the URL of the form > adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY} diff --git a/doc/server.md b/doc/server.md index e706e47..509c902 100644 --- a/doc/server.md +++ b/doc/server.md @@ -22,7 +22,7 @@ where you replace: > https://{website}/#/g/{owner}/{repo} -## data management +## 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. From e975c455fe0a0e87a1c6775e5731af66715b7a7c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 22 Jan 2024 12:44:12 +0100 Subject: [PATCH 11/12] Update doc/DOCUMENTATION.md --- doc/DOCUMENTATION.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md index 153756d..ca4a5c2 100644 --- a/doc/DOCUMENTATION.md +++ b/doc/DOCUMENTATION.md @@ -50,7 +50,7 @@ npm run start_client npm run production ``` -(in two separate terminals) to test the production modes of the server. This way it will only +(in two separate terminals) to test the production mode of the server. This way it will only change once you build and restart the server. ### Modifying the lean server From 36bc52c9602f31ccdc3bae553727dfa41eb2b54f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 22 Jan 2024 13:31:43 +0100 Subject: [PATCH 12/12] add logic game to landing page --- client/src/components/landing_page.tsx | 3 ++- relay/index.mjs | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index e2c870f..12dba1b 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -134,7 +134,8 @@ function LandingPage() { "leanprover-community/nng4", "hhu-adam/robo", "djvelleman/stg4", - "miguelmarco/STG4", + "miguelmarco/stg4", + "trequetrum/lean4game-logic", ] let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) diff --git a/relay/index.mjs b/relay/index.mjs index a0dd7ea..8d1e9cf 100644 --- a/relay/index.mjs +++ b/relay/index.mjs @@ -19,7 +19,8 @@ import { importTrigger, importStatus } from './import.mjs' const queueLength = { "g/hhu-adam/robo": 2, "g/hhu-adam/nng4": 5, - "g/djvelleman/stg4": 2, + "g/djvelleman/stg4": 0, + "g/trequetrum/lean4game-logic": 0, } const __filename = url.fileURLToPath(import.meta.url);