How to build locally?

Question

How to build locally?

Closed this issue a year ago · 29 comments

How can I preview NNG4 locally in a browser?
There is a Dockerfile, but I didn't know how to use it. Sorry for the rudimentary question.

Seasawher commented a year ago

:(

Answer 1 · 2023-06-06T09:02:17.000Z

That's not as straight-forward as I would like it to be. I have now written a summary here:

https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#running-games-locally

I hope it works; I haven't really tested it yet. Let me know if you run into any issues.

Answer 2 · 2023-06-06T10:01:32.000Z

npm start failed... :(

❯ npm start  

> lean4-game@0.1.0 start
[server] Building GameServer.EnvExtensions
[server] Compiling GameServer.Graph
[server] Building GameServer.RpcHandlers
[server] Compiling GameServer.EnvExtensions
[server] Building GameServer.Game
[server] Compiling GameServer.RpcHandlers
[server] Building GameServer.Watchdog
[server] Compiling GameServer.Game
[server] Building GameServer.FileWorker
[server] Compiling GameServer.Watchdog
[server] Building Main
[server] Compiling GameServer.FileWorker
[server] Compiling Main
[server] Linking gameserver.exe
[server] 'NODE_ENV' �́A�����R�}���h�܂��͊O���R�}���h�A
[server] ����\�ȃv���O�����܂��̓o�b�` �t�@�C���Ƃ��ĔF������Ă��܂���B
[server] npm run start_server exited with code 1

Answer 3 · 2023-06-06T10:35:09.000Z

It worked for me on linux. Maybe try in WSL instead?

If that doesn't help I'd check the node version with node -v

Answer 4 · 2023-06-06T10:48:29.000Z

@Seasawher Is this on Windows?

Answer 5 · 2023-06-06T11:11:03.000Z

Oh, yeah, it seems to be Windows, judging from your output.

Try to run npm start in WSL or in Git Bash. I am guessing you must have Git Bash installed anyway to be able to clone the repositories?

Alternatively, I just pushed a change on lean4game that should make npm start work on Windows, too. To get it, in the lean4game directory, run:

git pull
npm install
npm start

Answer 6 · 2023-06-06T12:41:03.000Z

Thanks, npm start may have worked.

But I failed to compile. (I'm still working on Windows)

The error message displayed in the browser was as follows:

Failed to compile.
Module parse failed: Unexpected token (2:12)
node_modules/lean4-infoview/src/infoview/contexts.ts
You may need an appropriate loader to handle this file type, currently no loaders are configured to process this file. See https://webpack.js.org/concepts#loaders
| import * as React from 'react';
> import type { DocumentUri, Diagnostic } from 'vscode-languageserver-protocol';
| 
| import { LeanFileProgressProcessingInfo, InfoviewConfig, defaultInfoviewConfig } from '@leanprover/infoview-api';

Answer 7 · 2023-06-07T07:42:14.000Z

I've pushed something that might help here. Can you try again? I can't currently test it on Windows, unfortunately.

Answer 8 · 2023-06-07T09:21:06.000Z

Thank you very much. But the error occurred again.

Answer 9 · 2023-06-07T09:27:24.000Z

Error message:

Error
Client is not running and can't be stopped. It's current state is: startFailed

Call Stack
 MonacoLanguageClient.shutdown
  bundle.js:330595:19
 MonacoLanguageClient.stop
  bundle.js:330566:21
 MonacoLanguageClient.doInitialize
  bundle.js:330548:27
 async MonacoLanguageClient.start
  bundle.js:330403:13

Answer 10 · 2023-06-07T09:32:00.000Z

Any idea how to build using docker? Devcontainer or docker-compose might work in my environment.
My environment is Windows 11, but docker desktop is installed and WSL2 is available.

Answer 11 · 2023-06-07T09:36:04.000Z

The Docker container is used to contain the Lean process, so that users cannot get access to our server. The Docker container does not contain the entire web server. So we would have to set up a different Docker file to do what you would like to do.

Answer 12 · 2023-06-07T09:41:47.000Z

What is the output on the command line where you executed npm start?

Answer 13 · 2023-06-07T09:52:25.000Z

A part of output is:

[server] [Wed Jun 07 2023 18:49:32 GMT+0900 (日本標準時)] Socket opened - ::ffff:127.0.0.0
[server] [Wed Jun 07 2023 18:49:32 GMT+0900 (日本標準時)] Number of open sockets - 1
[server] [Wed Jun 07 2023 18:49:32 GMT+0900 (日本標準時)] Free RAM - 2951 / 16069 MB
[server] CLIENT: {"jsonrpc":"2.0","id":0,"method":"initialize","params":{"processId":null,"clientInfo":{"name":"Monaco","version":"1.69.0"},"locale":"ja","rootPath":null,"rootUri":null,"capabilities":{"workspace":{"applyEdit":true,"workspaceEdit":{"documentChanges":true,"resourceOperations":["create","rename","delete"],"failureHandling":"textOnlyTransactional","normalizesLineEndings":true,"changeAnnotationSupport":{"groupsOnLabel":true}},"codeLens":{"refreshSupport":true},"executeCommand":{"dynamicRegistration":true},"workspaceFolders":true,"semanticTokens":{"refreshSupport":true},"inlayHint":{"refreshSupport":true},"diagnostics":{"refreshSupport":true}},"textDocument":{"publishDiagnostics":{"relatedInformation":true,"versionSupport":false,"tagSupport":{"valueSet":[1,2]},"codeDescriptionSupport":true,"dataSupport":true},"synchronization":{"dynamicRegistration":true},"completion":{"dynamicRegistration":true,"contextSupport":true,"completionItem":{"snippetSupport":true,"commitCharactersSupport":true,"documentationFormat":["markdown","plaintext"],"deprecatedSupport":true,"preselectSupport":true,"tagSupport":{"valueSet":[1]},"insertReplaceSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"insertTextModeSupport":{"valueSet":[1,2]},"labelDetailsSupport":true},"insertTextMode":2,"completionItemKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]},"completionList":{"itemDefaults":["commitCharacters","editRange","insertTextFormat","insertTextMode"]}},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"signatureHelp":{"dynamicRegistration":true,"signatureInformation":{"documentationFormat":["markdown","plaintext"],"parameterInformation":{"labelOffsetSupport":true},"activeParameterSupport":true},"contextSupport":true},"definition":{"dynamicRegistration":true,"linkSupport":true},"references":{"dynamicRegistration":true},"documentHighlight":{"dynamicRegistration":true},"documentSymbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"hierarchicalDocumentSymbolSupport":true,"tagSupport":{"valueSet":[1]},"labelSupport":true},"codeAction":{"dynamicRegistration":true,"isPreferredSupport":true,"disabledSupport":true,"dataSupport":true,"resolveSupport":{"properties":["edit"]},"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}},"honorsChangeAnnotations":false},"codeLens":{"dynamicRegistration":true},"formatting":{"dynamicRegistration":true},"rangeFormatting":{"dynamicRegistration":true},"onTypeFormatting":{"dynamicRegistration":true},"rename":{"dynamicRegistration":true,"prepareSupport":true,"prepareSupportDefaultBehavior":1,"honorsChangeAnnotations":true},"documentLink":{"dynamicRegistration":true,"tooltipSupport":true},"typeDefinition":{"dynamicRegistration":true,"linkSupport":true},"implementation":{"dynamicRegistration":true,"linkSupport":true},"colorProvider":{"dynamicRegistration":true},"foldingRange":{"dynamicRegistration":true,"rangeLimit":5000,"lineFoldingOnly":true,"foldingRangeKind":{"valueSet":["comment","imports","region"]},"foldingRange":{"collapsedText":false}},"declaration":{"dynamicRegistration":true,"linkSupport":true},"selectionRange":{"dynamicRegistration":true},"semanticTokens":{"dynamicRegistration":true,"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator","decorator"],"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"formats":["relative"],"requests":{"range":true,"full":{"delta":true}},"multilineTokenSupport":false,"overlappingTokenSupport":false,"serverCancelSupport":true,"augmentsSyntaxTokens":true},"linkedEditingRange":{"dynamicRegistration":true},"inlayHint":{"dynamicRegistration":true,"resolveSupport":{"properties":["tooltip","textEdits","label.tooltip","label.location","label.command"]}},"diagnostic":{"dynamicRegistration":true,"relatedDocumentSupport":false}},"window":{"showMessage":{"messageActionItem":{"additionalPropertiesSupport":true}},"showDocument":{"support":true}},"general":{"staleRequestSupport":{"cancel":true,"retryOnContentModified":["textDocument/semanticTokens/full","textDocument/semanticTokens/range","textDocument/semanticTokens/full/delta"]},"regularExpressions":{"engine":"ECMAScript","version":"ES2020"},"markdown":{"parser":"marked","version":"1.1.0"},"positionEncodings":["utf-16"]}},"initializationOptions":{"editDelay":200,"hasWidgets":true},"trace":"off","workspaceFolders":null}}
[server] Lean Server: Watchdog error: Error while running Lake: error: no such file or directory (error code: 2)

Answer 14 · 2023-06-07T09:53:37.000Z

Localhost:3000 is available. But natural number game is not visible.

Answer 15 · 2023-06-07T10:08:03.000Z

You could try to replace line 12 of lean4game/server/index.mjs, which currently says dir: "../../../../NNG4", by dir: "..\\..\\..\\..\\NNG4",.

If that does not help check that

running lake env printenv LEAN_PATH in the NNG4 folder works
the NNG4 folder is next to the lean4game folder
the NNG4 folder is really called NNG4.

Answer 16 · 2023-06-07T10:39:12.000Z

replacing / to \\ does not work.
lake env printenv LEAN_PATH does not work

$ lake env printenv LEAN_PATH
warning: manifest out of date: source kind (git/path) of dependency GameServer changed, use `lake update` to update
.\build\lib;.\./../lean4game/server\build\lib;.\lake-packages\std\build\lib;c:\Users\11325\.elan\toolchains\leanprover--lean4---nightly-2023-03-09\lib\lean

the NNG4 folder is next to the lean4game folder
the NNG4 folder is really called NNG4.

Answer 17 · 2023-06-07T10:45:40.000Z

In the NNG4 directory, delete the lake-packages folder, then run

set NODE_ENV=development
lake update
lake build

Sorry, I'll have to find a better solution for this, but this should work for now.

Answer 18 · 2023-06-07T11:00:41.000Z

Terminal message:

[client] <i> [webpack-dev-server] [HPM] Upgrading to WebSocket
[server] [Wed Jun 07 2023 19:59:11 GMT+0900 (日本標準時)] Socket opened - ::ffff:127.0.0.0
[server] [Wed Jun 07 2023 19:59:11 GMT+0900 (日本標準時)] Number of open sockets - 1
[server] [Wed Jun 07 2023 19:59:11 GMT+0900 (日本標準時)] Free RAM - 2799 / 16069 MB
[server] CLIENT: {"jsonrpc":"2.0","id":0,"method":"initialize","params":{"processId":null,"clientInfo":{"name":"Monaco","version":"1.69.0"},"locale":"ja","rootPath":null,"rootUri":null,"capabilities":{"workspace":{"applyEdit":true,"workspaceEdit":{"documentChanges":true,"resourceOperations":["create","rename","delete"],"failureHandling":"textOnlyTransactional","normalizesLineEndings":true,"changeAnnotationSupport":{"groupsOnLabel":true}},"codeLens":{"refreshSupport":true},"executeCommand":{"dynamicRegistration":true},"workspaceFolders":true,"semanticTokens":{"refreshSupport":true},"inlayHint":{"refreshSupport":true},"diagnostics":{"refreshSupport":true}},"textDocument":{"publishDiagnostics":{"relatedInformation":true,"versionSupport":false,"tagSupport":{"valueSet":[1,2]},"codeDescriptionSupport":true,"dataSupport":true},"synchronization":{"dynamicRegistration":true},"completion":{"dynamicRegistration":true,"contextSupport":true,"completionItem":{"snippetSupport":true,"commitCharactersSupport":true,"documentationFormat":["markdown","plaintext"],"deprecatedSupport":true,"preselectSupport":true,"tagSupport":{"valueSet":[1]},"insertReplaceSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"insertTextModeSupport":{"valueSet":[1,2]},"labelDetailsSupport":true},"insertTextMode":2,"completionItemKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]},"completionList":{"itemDefaults":["commitCharacters","editRange","insertTextFormat","insertTextMode"]}},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"signatureHelp":{"dynamicRegistration":true,"signatureInformation":{"documentationFormat":["markdown","plaintext"],"parameterInformation":{"labelOffsetSupport":true},"activeParameterSupport":true},"contextSupport":true},"definition":{"dynamicRegistration":true,"linkSupport":true},"references":{"dynamicRegistration":true},"documentHighlight":{"dynamicRegistration":true},"documentSymbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"hierarchicalDocumentSymbolSupport":true,"tagSupport":{"valueSet":[1]},"labelSupport":true},"codeAction":{"dynamicRegistration":true,"isPreferredSupport":true,"disabledSupport":true,"dataSupport":true,"resolveSupport":{"properties":["edit"]},"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}},"honorsChangeAnnotations":false},"codeLens":{"dynamicRegistration":true},"formatting":{"dynamicRegistration":true},"rangeFormatting":{"dynamicRegistration":true},"onTypeFormatting":{"dynamicRegistration":true},"rename":{"dynamicRegistration":true,"prepareSupport":true,"prepareSupportDefaultBehavior":1,"honorsChangeAnnotations":true},"documentLink":{"dynamicRegistration":true,"tooltipSupport":true},"typeDefinition":{"dynamicRegistration":true,"linkSupport":true},"implementation":{"dynamicRegistration":true,"linkSupport":true},"colorProvider":{"dynamicRegistration":true},"foldingRange":{"dynamicRegistration":true,"rangeLimit":5000,"lineFoldingOnly":true,"foldingRangeKind":{"valueSet":["comment","imports","region"]},"foldingRange":{"collapsedText":false}},"declaration":{"dynamicRegistration":true,"linkSupport":true},"selectionRange":{"dynamicRegistration":true},"semanticTokens":{"dynamicRegistration":true,"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator","decorator"],"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"formats":["relative"],"requests":{"range":true,"full":{"delta":true}},"multilineTokenSupport":false,"overlappingTokenSupport":false,"serverCancelSupport":true,"augmentsSyntaxTokens":true},"linkedEditingRange":{"dynamicRegistration":true},"inlayHint":{"dynamicRegistration":true,"resolveSupport":{"properties":["tooltip","textEdits","label.tooltip","label.location","label.command"]}},"diagnostic":{"dynamicRegistration":true,"relatedDocumentSupport":false}},"window":{"showMessage":{"messageActionItem":{"additionalPropertiesSupport":true}},"showDocument":{"support":true}},"general":{"staleRequestSupport":{"cancel":true,"retryOnContentModified":["textDocument/semanticTokens/full","textDocument/semanticTokens/range","textDocument/semanticTokens/full/delta"]},"regularExpressions":{"engine":"ECMAScript","version":"ES2020"},"markdown":{"parser":"marked","version":"1.1.0"},"positionEncodings":["utf-16"]}},"initializationOptions":{"editDelay":200,"hasWidgets":true},"trace":"off","workspaceFolders":null}}
[server] Lean Server: Watchdog error: Error while running Lake: warning: manifest out of date: source kind (git/path) of dependency GameServer changed, use `lake update` to update
[server] error: no such file or directory (error code: 2)

Answer 19 · 2023-06-07T11:39:06.000Z

Ok, I have no idea what's going wrong here. Using a docker container as you suggested is probably much easier. I will try to set up a Docker file for this.

Answer 20 · 2023-06-07T11:45:59.000Z

Yea maybe it's time we make this easier to set up locally 😆

Here is a sequence of commands, I would use to try and fix your setup until Alex created a docker file that contains everything. Untested, so might need adaptation. Also I assume they are both fresh copies of the git repos, otherwise you might want to checkout main again.

cd lean4game
git pull

cd ../NNG4
export NODE_ENV=development
rm -rf lake-packages/
rm lake-manifest.json
lake update
lake build

cd ../lean4game
npm install
npm start

Answer 21 · 2023-06-07T11:56:10.000Z

Thank you very much. By the way, I have created a Dockerfile to create devcontainer, but from now on, I seem to get an error at npm install. Share my Dockerfile.

I thought I followed the instruction to the letter, but what went wrong?

FROM node:20

WORKDIR /

ENV ELAN_HOME=/usr/local/elan \
    PATH=/usr/local/elan/bin:$PATH \
    LEAN_VERSION=leanprover/lean4:nightly

SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]

RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
    chmod -R a+w $ELAN_HOME; \
    elan --version; \
    lean --version; \
    leanc --version; \
    lake --version;

RUN git clone https://github.com/hhu-adam/NNG4.git

WORKDIR /NNG4
RUN lake update && lake build

WORKDIR /
RUN git clone https://github.com/leanprover-community/lean4game.git

WORKDIR /lean4game
RUN npm install

EXPOSE 3000

Answer 22 · 2023-06-07T12:22:16.000Z

That's weird, your Dockerfile works for me:

$ docker build - < test.Dockerfile                                                                   
[+] Building 84.7s (12/12) FINISHED                                            
 => [internal] load build definition from Dockerfile                      0.0s 
 => => transferring dockerfile: 719B                                      0.0s 
 => [internal] load .dockerignore                                         0.0s
 => => transferring context: 2B                                           0.0s
 => [internal] load metadata for docker.io/library/node:20                1.5s
 => [ 1/10] FROM docker.io/library/node:20@sha256:14f0471d0478fbb9177d0  10.4s
 => => resolve docker.io/library/node:20@sha256:14f0471d0478fbb9177d0f9e  0.0s
 => => sha256:6710592d62aa1338ac1c1c363dedc255659f666c 15.76MB / 15.76MB  0.5s
 => => sha256:75256935197ed1bb3b994a77c01efa00349b9010 54.58MB / 54.58MB  2.4s
 => => sha256:14f0471d0478fbb9177d0f9e8c146dc872273dcdcf 1.21kB / 1.21kB  0.0s
 => => sha256:c6b8ae21142621595ae24ca50eeda1299a33bba46c 2.00kB / 2.00kB  0.0s
 => => sha256:f03de6896e9e068cf6c241b5d668cc1f4b3c851a0b 7.23kB / 7.23kB  0.0s
 => => sha256:bd73737482dd5575526c7207872963479808d979 55.05MB / 55.05MB  1.6s
 => => sha256:c1e5026c64577dee4b6bac20b18196f964a41d 196.85MB / 196.85MB  4.9s
 => => extracting sha256:bd73737482dd5575526c7207872963479808d979ab2741c  1.2s
 => => sha256:f2e4b4cbd0b8a554057e4c702cf430b30539db4912 4.20kB / 4.20kB  1.7s
 => => sha256:ea5ab4043c9d4c35cdff54e7efd4c18f47a6e3c8 47.55MB / 47.55MB  3.4s
 => => sha256:00aabd86b438c7cfd5dc60720647bd77c770da5475 2.27MB / 2.27MB  2.6s
 => => sha256:e3f550576775f4e0fc59ed9e28b348778af799165d1229 453B / 453B  2.8s
 => => extracting sha256:6710592d62aa1338ac1c1c363dedc255659f666cc41441c  0.2s
 => => extracting sha256:75256935197ed1bb3b994a77c01efa00349b901014448a2  1.3s
 => => extracting sha256:c1e5026c64577dee4b6bac20b18196f964a41d8b9016fbb  3.8s
 => => extracting sha256:f2e4b4cbd0b8a554057e4c702cf430b30539db4912a8406  0.0s
 => => extracting sha256:ea5ab4043c9d4c35cdff54e7efd4c18f47a6e3c844897a5  1.4s
 => => extracting sha256:00aabd86b438c7cfd5dc60720647bd77c770da54754f4b4  0.0s
 => => extracting sha256:e3f550576775f4e0fc59ed9e28b348778af799165d1229e  0.0s
 => [ 2/10] RUN curl https://raw.githubusercontent.com/leanprover/elan/  13.7s
 => [ 3/10] RUN git clone https://github.com/hhu-adam/NNG4.git            1.3s
 => [ 4/10] WORKDIR /NNG4                                                 0.0s
 => [ 5/10] RUN lake update && lake build                                34.9s
 => [ 6/10] RUN git clone https://github.com/leanprover-community/lean4g  3.2s
 => [ 7/10] WORKDIR /lean4game                                            0.0s
 => [ 8/10] RUN npm install                                              14.3s
 => exporting to image                                                    5.4s
 => => exporting layers                                                   5.4s
 => => writing image sha256:6918ebea71422955d030bae1b518ab1cdac8b25832ac

Answer 23 · 2023-06-07T12:57:55.000Z

I upgraded docker desktop from 4.18 to 4.20 and now I can build and view NNG4 from my browser. Thanks. 😄

It was also confirmed that the game can be played locally.

The following problems have been identified so far.

Incredibly slow loading.
Code changes are not reflected on the page
Docker image size is too large (3.4 GB)

My current NNG4/.devcontainer directory contents are as follows.

dockerfile

Thanks to https://github.com/xubaiw/docker-lean

FROM node:20

WORKDIR /

ENV ELAN_HOME=/usr/local/elan \
  PATH=/usr/local/elan/bin:$PATH \
  LEAN_VERSION=leanprover/lean4:nightly

SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]

RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
  chmod -R a+w $ELAN_HOME; \
  elan --version; \
  lean --version; \
  leanc --version; \
  lake --version;

RUN git clone https://github.com/hhu-adam/NNG4.git

WORKDIR /NNG4
RUN lake update && lake build

WORKDIR /
RUN git clone https://github.com/leanprover-community/lean4game.git

WORKDIR /lean4game
RUN npm install

EXPOSE 3000

docker-compose.yml

version: "3.9"

services:
  nng4:
    build:
      context: .
      dockerfile: Dockerfile
    image: lean4-game-dev
    container_name: lean4-develop
    command: npm start
    volumes:
      - ..:/NNG4
    ports:
      - "3000:3000"

Answer 24 · 2023-06-07T13:18:53.000Z

Code changes are not reflected on the page

In the local setup (i.e. without docker) you can run lake build inside NNG4/ after which the code changes will be visible in your browser.

(you probably need to reload the browser, but no need to restart the npm server.)

Edit: we deliberately disabled the automatic building when a lean-file is modified, as this constantly triggered lake build when editing a file. That made it impossible to play through the game and edit the code simultaneously. Calling lake build manually gives you the control.

Answer 25 · 2023-06-07T13:27:52.000Z

Incredibly slow loading.

Yep :( Although, what is "incredibly"? On my local machine and online we are talking around 5-30s for loading a new World but much quicker for changing levels.

If it's worse than that, add some comments to this issue: leanprover-community/lean4game#15

Answer 26 · 2023-06-07T13:42:19.000Z

Yep :( Although, what is "incredibly"? On my local machine and online we are talking around 5-30s for loading a new World but much quicker for changing levels.

When reloading in the browser, it took 1m15s before the screen reappeared. (on my local machine)

Answer 27 · 2023-06-07T13:44:03.000Z

In the local setup (i.e. without docker) you can run lake build inside NNG4/ after which the code changes will be visible in your browser.

It worked. Thank you.

Answer 28 · 2023-06-07T14:21:09.000Z

Thanks to your kindness, I now know how to build locally. You may close this issue as completed. 🙇