Zulip Chat Archive

Stream: general

Topic: Debugging Lean games & building JS/WASM versions for Lean


view this post on Zulip Ryan Lahfa (Feb 07 2021 at 00:59):

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?

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:04):

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).

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:04):

Does any of the info here help?

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:06):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:06):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:07):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:07):

image.png

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:08):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:08):

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.

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:09):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:12):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:16):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:18):

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...

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:18):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:19):

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)

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:20):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:21):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:21):

But now, time to sleep

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:21):

Thanks a lot @Bryan Gin-ge Chen !

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:31):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:35):

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

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:35):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 01:37):

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.

view this post on Zulip Ryan Lahfa (Feb 07 2021 at 01:37):

Thanks a lot, will do tomorrow

view this post on Zulip Huỳnh Trần Khanh (Feb 07 2021 at 03:57):

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.

view this post on Zulip Huỳnh Trần Khanh (Feb 07 2021 at 04:01):

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

view this post on Zulip Gabriel Ebner (Feb 07 2021 at 08:45):

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"; ... }.

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 00:36):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:38):

@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?

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:40):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2021 at 02:48):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2021 at 02:51):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:52):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:53):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:54):

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)

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2021 at 02:55):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:57):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:57):

I double-tripled-checked

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 02:57):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:00):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:00):

So the issue lies in the Nix packaged Lean

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:00):

I have an idea on what's going on

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:01):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:01):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:02):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:03):

@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

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2021 at 03:05):

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.

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:07):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2021 at 03:10):

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?

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:21):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:22):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:23):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 03:34):

and… that's the win!

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 12:19):

@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?

view this post on Zulip Gabriel Ebner (Feb 08 2021 at 12:21):

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

view this post on Zulip Ryan Lahfa (Feb 08 2021 at 12:21):

Gabriel Ebner said:

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

On each dependency?

view this post on Zulip Gabriel Ebner (Feb 08 2021 at 13:05):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2021 at 17:48):

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.


Last updated: May 15 2021 at 22:14 UTC