Debugging Lean games & building JS/WASM versions for Lean

Stream: general

[Ryan Lahfa]

I'm currently packaging Lean games into NixOS, with some generic builder to deploy easily more Lean games (some code is around there: https://github.com/RaitoBezarius/nixexprs/blob/master/pkgs/tools/make-lean-game.nix).

I have deployed the master branch of NNG on https://nng.lean.v6.lahfa.xyz (IPv6-only website sorry! Can make it available through IPv4 though upon request), though I am getting empty infoboxes everywhere.

I admit that I have done something that I should not have, e.g. it produces the NNG game using Lean 3.24.0 when it asks for Lean 3.4.2, and it uses Lean 3.4.2 JS/WASM files in the browser with 3.24.0 olean files I guess (as the ZIP file must contain those).

Though, I expect some kind of error, the thing is I get nothing, the editor, the world looks to be working fine, but when I do "refl," on the first level, it just does nothing after a short "Lean is busy...", so I assume that there is something wrong with the Lean runtime.

That's the first part of the question.

For the second part, one way to test the previous hypothesis would be to produce JS/WASM files for Lean 3.24.0 and remake the NNG for 3.24.0, it appears to me that @Gabriel Ebner is maintainer on the Lean package on NixOS, I would like to ask: how much effort would be needed to add as an output the lean_js_js.js, lean_js_wasm.js, lean_js_wasm.wasm files in the Lean package? Or how can I produce them given the Lean package? I tried to poke around in the source code but didn't find really explicit stuff, I was planning to dig into the CMake files but maybe it is faster and better to just ask?

[Bryan Gin-ge Chen]

The lean_js_* files are available from the community Lean releases on GitHub, e.g. https://github.com/leanprover-community/lean/releases/tag/v3.26.0 (see lean-3.26.0--browser.zip).

[Bryan Gin-ge Chen]

Does any of the info here help?

[Ryan Lahfa]

Bryan Gin-ge Chen said:

The lean_js_* files are available from the community Lean releases on GitHub, e.g. https://github.com/leanprover-community/lean/releases/tag/v3.26.0 (see lean-3.26.0--browser.zip).

I could just copy them in the repo and follow the same workflow but hopefully I'm aiming at automating to "produce" the right Lean version end to end for those games, so I would just need to know how to derive them from source

[Bryan Gin-ge Chen]

If Lean in the browser gets stuck, you can sometimes figure out what's going wrong by looking in your browser's console.

[Ryan Lahfa]

Bryan Gin-ge Chen said:

If Lean in the browser gets stuck, you can sometimes figure out what's going wrong by looking in your browser's console.

The console shows nothing alas

[Ryan Lahfa]

image.png

[Ryan Lahfa]

(afaik the two "unrelated" errors are due to Chrome WASM impl and are indeed unrelated)

[Bryan Gin-ge Chen]

Unfortunately I can't access your test website (I guess due to the IPv6 vs IPv4 thing). The screenshot you posted seems to indicate that Lean in the browser is working OK.

[Bryan Gin-ge Chen]

If you want to compile the JS/WASM versions of Lean 3 yourself, you could get inspiration from what's done in our CI: https://github.com/leanprover-community/lean/blob/master/.github/workflows/on-push.yml#L161

[Bryan Gin-ge Chen]

There's also some docs here for building Lean with Emscripten, but they might be out of date.

[Ryan Lahfa]

Bryan Gin-ge Chen said:

There's also some docs here for building Lean with Emscripten, but they might be out of date.

Awesome, that sounds like what I need

[Bryan Gin-ge Chen]

Ah, my guess is Lean on your page is getting stuck because it can't find olean files with the right version so it's trying to compile everything...

[Ryan Lahfa]

Bryan Gin-ge Chen said:

Unfortunately I can't access your test website (I guess due to the IPv6 vs IPv4 thing). The screenshot you posted seems to indicate that Lean in the browser is working OK.

https://nng.lean.lahfa.xyz/ should do the trick, unfortunately, the HTTPS cert is broken

[Ryan Lahfa]

Bryan Gin-ge Chen said:

Ah, my guess is Lean on your page is getting stuck because it can't find olean files with the right version so it's trying to compile everything...

Wouldn't this print something on the console ideally? (maybe not)

[Ryan Lahfa]

Bryan Gin-ge Chen said:

Ah, my guess is Lean on your page is getting stuck because it can't find olean files with the right version so it's trying to compile everything...

But that would make a lot of sense

[Ryan Lahfa]

Compiling Lean 3.4.2 is a bit annoying it looks like due to GCC version constraints apparently ; so I will try to produce 3.24.0 JS/WASM files and use them in the final bundle

[Ryan Lahfa]

But now, time to sleep

[Ryan Lahfa]

Thanks a lot @Bryan Gin-ge Chen !

[Bryan Gin-ge Chen]

Hmm, it's actually not getting stuck for me in Firefox, instead it's complaining about missing Lean files (which is another symptom of the olean versions not matching). [Annoyingly, the error popup sometimes ends up above the line with an error in it, which makes it impossible to see.]

Screen-Shot-2021-02-06-at-8.30.03-PM.png

[Ryan Lahfa]

ha! @Bryan Gin-ge Chen :D Maybe that was my bug :')

[Ryan Lahfa]

Though, I'm now put at ease that the Lean runtime is doing something

[Bryan Gin-ge Chen]

Yeah, feel free to ping me if you get stuck again. I spent a fair bit of time debugging this kind of thing when I was playing around with the Lean web editor. I don't have experience with the NNG itself, but I imagine it's very similar.

[Ryan Lahfa]

Thanks a lot, will do tomorrow

[Huỳnh Trần Khanh]

A quick tip: if you want to access an IPv6 only website when your ISP doesn't support it for some reason, you can use the Tor Browser.

[Huỳnh Trần Khanh]

But Tor Browser doesn't support WASM because of security reasons :joy:

[Gabriel Ebner]

Ryan Lahfa said:

For the second part, one way to test the previous hypothesis would be to produce JS/WASM files for Lean 3.24.0 and remake the NNG for 3.24.0, it appears to me that Gabriel Ebner is maintainer on the Lean package on NixOS, I would like to ask: how much effort would be needed to add as an output the lean_js_js.js, lean_js_wasm.js, lean_js_wasm.wasm files in the Lean package? Or how can I produce them given the Lean package? I tried to poke around in the source code but didn't find really explicit stuff, I was planning to dig into the CMake files but maybe it is faster and better to just ask?

Not trivial, but not impossible either. To get these files, you need to compile lean with emscripten. (But we have emscripten in nixpkgs.) If you want to upstream the nixos modules into nixpkgs, then I'd suggest to make a second lean3-emscripten derivation which compiles lean from source using emscripten. If you just want it for personal use, then use fetchurl { src = "https://github.com/leanprover-community/lean/releases/download/v3.26.0/lean-3.26.0--browser.zip"; ... }.

[Ryan Lahfa]

Gabriel Ebner said:

Ryan Lahfa said:

For the second part, one way to test the previous hypothesis would be to produce JS/WASM files for Lean 3.24.0 and remake the NNG for 3.24.0, it appears to me that Gabriel Ebner is maintainer on the Lean package on NixOS, I would like to ask: how much effort would be needed to add as an output the lean_js_js.js, lean_js_wasm.js, lean_js_wasm.wasm files in the Lean package? Or how can I produce them given the Lean package? I tried to poke around in the source code but didn't find really explicit stuff, I was planning to dig into the CMake files but maybe it is faster and better to just ask?

Not trivial, but not impossible either. To get these files, you need to compile lean with emscripten. (But we have emscripten in nixpkgs.) If you want to upstream the nixos modules into nixpkgs, then I'd suggest to make a second lean3-emscripten derivation which compiles lean from source using emscripten. If you just want it for personal use, then use fetchurl { src = "https://github.com/leanprover-community/lean/releases/download/v3.26.0/lean-3.26.0--browser.zip"; ... }.

Unfortunately, it seems like this step: https://github.com/leanprover-community/lean/blob/master/src/CMakeLists.txt#L282 makes it impossible to reproduce WASM/JS files without further patching of the source tree

[Ryan Lahfa]

@Bryan Gin-ge Chen Well chasing down the problem made me understood that it's nastier than what I thought, I am now trying locally to do make-lean-game which does lean --make and package everything in a ZIP ; but when I try locally without Nix except to provide Lean 3.24.0, it still fails with the same errors as the olean are incompatible

I'm unsure if I can just open the olean and check which versions they are for, also, I get this message each time from leanpkg:

WARNING: Lean version mismatch: installed version is leanprover-community/lean:3.24.0, but package requires 3.24.0

Unsure what to do with this, can it really cause issue? To me, leanpkg.toml is only declarative stuff, right? As long as I indeed use Lean 3.24.0 for WASM/JS and Lean 3.24.0 for olean building, it should be just fine?

[Ryan Lahfa]

Here's a tarball of the locally, by hand, produced web source: local_nng_for_3-24-0.tar.gz

[Bryan Gin-ge Chen]

That warning can be safely ignored. I mention this in the leanprover-community/lean-web-editor README in this section.

[Bryan Gin-ge Chen]

If you open an .olean file in e.g. vim, it should start with something like this: oleanfile^@3.26.0, commit 5a5c139af3e9.

[Ryan Lahfa]

Bryan Gin-ge Chen said:

If you open an .olean file in e.g. vim, it should start with something like this: oleanfile^@3.26.0, commit 5a5c139af3e9.

Alright, I can see it in my olean

[Ryan Lahfa]

I also fixed somewhat the warning by following the exact path, with no further success

[Ryan Lahfa]

I also tried the maze game skeleton provided in https://github.com/kbuzzard/lean-game-skeleton with the same errors (cannot import the user code seems like)

[Bryan Gin-ge Chen]

You're using commit Lean 3.24.0 13007eb to build the oleans and using the JS/WASM files from the GitHub release?

[Ryan Lahfa]

Bryan Gin-ge Chen said:

You're using commit Lean 3.24.0 13007eb to build the oleans and using the JS/WASM files from the GitHub release?

Yes

[Ryan Lahfa]

I double-tripled-checked

[Ryan Lahfa]

I'm trying with a Lean downloaded from elan now just in case

[Ryan Lahfa]

tough luck :>
It's now working with the elan-downloaded Lean

[Ryan Lahfa]

So the issue lies in the Nix packaged Lean

[Ryan Lahfa]

I have an idea on what's going on

[Ryan Lahfa]

The Nix packaged Lean has no commit git hash as the src is not provided with a .git so lean -v shows no commit githash even though it's the proper 3.24.0 version

[Ryan Lahfa]

Generating olean this way produces olean with no commit marker in the start of the file

[Ryan Lahfa]

IMHO, commit hash should not be embedded in the oleans, as long as there is a proper versioning scheme, am I wrong?

[Ryan Lahfa]

@Gabriel Ebner Shouldn't you use fetchurl and the tarball URLs for the src attr for the Lean package to inject the githash stuff? I will check if that actually fixes the bug

[Bryan Gin-ge Chen]

Ryan Lahfa said:

The Nix packaged Lean has no commit git hash as the src is not provided with a .git so lean -v shows no commit githash even though it's the proper 3.24.0 version

Yep, I was just about to point this out.

[Ryan Lahfa]

I have built a quick override on the source tree to see if that's definitely the issue

[Bryan Gin-ge Chen]

Ryan Lahfa said:

IMHO, commit hash should not be embedded in the oleans, as long as there is a proper versioning scheme, am I wrong?

There was some previous discussion (wow, in 2019) about removing the commit from the oleans or making Lean 3 less sensitive to the commit string in the oleans: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Time.20to.20move.20to.203.2E5.3F/near/179100595

I think at this point with Lean 4 on the horizon there's very little downside to this. @Gabriel Ebner what do you think?

[Ryan Lahfa]

Sounds like neither leaveDotGit = true; neither deepClone in addition can produce the proper sha1, unsure if I'm doing something wrong as those features are apparently non-deterministic

[Ryan Lahfa]

The easy solution could be to substitute the CMakeLists to give it the commit hash if needed at all, sounds like an easier solution

[Ryan Lahfa]

patching these two lines: https://github.com/leanprover-community/lean/blob/master/src/CMakeLists.txt#L362-L363 seems to be enough I guess, I will try in a quick'n'dirty fashion

[Ryan Lahfa]

and… that's the win!

[Ryan Lahfa]

@Gabriel Ebner Hmm, it seems like that leanpkg always tries to update the revision of dependencies, is there a way to skip this kind of behavior? As fetching git repositories removes the dot git for determinism, would there a way to say: do not try to configure the dependencies and just build using what I give you?

[Gabriel Ebner]

I would just fetch the dependencies by hand and then call lean --make src manually.

[Ryan Lahfa]

Gabriel Ebner said:

I would just fetch the dependencies by hand and then call lean --make src manually.

On each dependency?

[Gabriel Ebner]

Yes. You can also do lean --make src/ _target/deps/foo/src to make everything at once.

[Bryan Gin-ge Chen]

Note that lean --make src/ _target/deps/foo/src will build everything in foo, which usually isn't necessary (e.g. there's a lot of mathlib that the NNG doesn't depend on). So lean --make src should be sufficient in most cases.