Pitch for Webassembly support (and follow-up projects)

Stream: general

[Pim Otte]

I'd like to make a pitch for WebAssembly support, mostly in the context of education. This is kind of a thought-dump, so I'm very happy to hear additions and counterpoints:)

In general the point of these use cases is: Being able to do as much as possible with as little threshold as possible. In particular avoiding installation is a big deal for teachers; supposing about 10% of students will have some sort of installation issue, this automatically occupies a chunk of valuable class time. (Note that I appreciate how smooth the Lean installation process is, students just have a) wacky machines and b) varied ability in following instructions). In particular, drive-by usage of Lean in courses could get a boost if installation is not necessary. (i.e. use in a logic course as an optional project)

Some use cases that would be enabled by a Webassembly build, in order of estimated technical effort required:

1. vscode.dev with a Lean WebExtension: This would enable using Lean without installing anything, code and cache would still be stored on the users file system.
2. Client-side (and customizable) live.lean-lang.org. This would enable courses where a more light-weight experience is desirable. Client-side is important because then bigger courses won't put undue burden on live.lean-lang.org. Customizable is important to enable teachers to setup environments for exercises (In particular, I'm thinking of Verbose Lean here).
3. Interactive text-books. I'm thinking along the lines of the test that @Alex Kontorovich created recently. This test uses live.lean-lang.org, which I think is fine for a test, but (in my opinion) does not quite suffice in general for the reasons mentioned above.

Technical notes on each of these:

1. This would require slight adaptations to the VSCode extension: Any node-exclusive API's can't be in the imports of the WebExtension.
2. The currently ongoing improvements to the cache are likely needed to achieve this: The cache is no longer on disk, and having a 5Gish mathlib cache in the browser is not ideal. I also think we would want to set this up in a way that teachers could roll their own version relatively easily.
3. I think the way to go here is to integrate with a Verso Genre. Verso does all the elaboration at compile time, but I'm not really how this could be combined. Again, the caching is an issue here if you want to use mathlib.

Use case 1 is also something that we're currently pushing towards with Waterproof in the context of Rocq. Use cases 1 and 3 are the ones that are personally on my long-term TODO-list, but if others wanted to pick this up I would be very happy. (Actually getting (Verbose) Lean supported in Waterproof is one of the things that has my personal priority).

In general, I have no clue how stable and performant the webassembly build was to begin with, if anyone has experiences with this, I'd love to hear them.
@Kim Morrison lean4#6424 (temporarily) disabled the CI builds for webassembly, do you know what would be needed to bring them back?

[(deleted)]

Very interesting proposal. I believe Lean 4 has never properly supported WebAssembly. And having WebAssembly support is a good first step towards my lockdown mode proposal.

[(deleted)]

Lean 4 is currently dependent on mmap and linking precompiled Lean binaries :eyes: so out of the box Lean doesn't even function properly when compiled to WebAssembly.

[Johan Commelin]

cc @Joachim Breitner, who has a lot of ideas about wasm/lean (although maybe more about formalizing wasm in lean then running lean in wasm)

[Mario Carneiro]

My understanding was that there used to be a wasm build but it was ridiculously heavy after the move to mmapped oleans and it was very impractical compared to lean 3 days

[Joachim Breitner]

This came up before recently, and there are unfortunately very serious technical challenges. For example lean loads the .olean files using mmap for efficient start-up time, which is something that Wasm doesn’t support yet. Then there is the 4GB memory restriction of Wasm, which is not going to be enough to load a decent project like mathlib. So I’m not very optimistic (and it’s certainly not just a matter of compiling to a different platform)

[Mario Carneiro]

I would really love if lean could get its memory footprint down to sane levels though

[Mario Carneiro]

maybe the module stuff will help with this?

[Mario Carneiro]

reminder that mathlib in lean 3 was only around 200 MB and it has only ~tripled since then

[Mario Carneiro]

the fact that it is in the multiple gigabyte regime is entirely because of lean storage design decisions, not mathlib being big

[Pim Otte]

I think it would be perfectly acceptable to aim for "a lot smaller than mathlib"-projects for these use cases. I think projects dependent on mathlib are the more common use case, and as I understand it, the caching improvements involve an olean split, so that would also mean needing to load less into memory, right? (I'm not really sure what the module stuff is, is that related to this?)

Then I think the open question would be if pre-loading all the "slim" oleans into memory would be acceptable (or we really need mmap support). If it ends up being 600MB, that seems doable. For interactive books it might be a little bit heavy if every page needs it, but then you could do a single-page html style book.

[Joachim Breitner]

Mario Carneiro schrieb:

maybe the module stuff will help with this?

It certainly will; the oleans to load will be ~half the size. Maybe even less.

[(deleted)]

My radical mind says we can use SQLite instead of mmaping olean files...

[(deleted)]

That does mean we have to say goodbye to the compacted heap region and move to a more relational model

[Mario Carneiro]

I would definitely support something like that. Maybe not sqlite directly, but rather something along the lines of mmapping .ltar files instead, which despite being compressed can still be traversed as a read only data structure, which is just fine for a lot of applications like instantiating level variables during definitional unfolding of something in the environment

[Mario Carneiro]

the thing one has to get away from is the assumption that the thing in memory is already a valid lean_object

[Emilio Jesús Gallego Arias]

Thanks @Pim Otte for making this pitch, I'm very interested in a Lean/WASM port too.

A couple of questions:

lean storage design decisions

@Mario Carneiro , do you have any additional pointers regarding the challenges here?

lean loads the .olean files using mmap for efficient start-up time

I guess allowing a "copy" mode would be possible, and while indeed performance would be impacted, I understand that .olean files are patched after mmaping anyways?

What other challenges would be there? Modern WASIX / Rust WASM toolchain, while not standard, support a large number of extensions and libuv, so (from the bench, and obviating library size), trying a WASM build shouldn't be too far?

[(deleted)]

You mentioned WASIX... Unfortunately the company promoting WASIX doesn't have a very good reputation.

[(deleted)]

I'm not sure whether this has anything to do with the technical merits of WASIX.

[Mario Carneiro]

Emilio Jesús Gallego Arias said:

I guess allowing a "copy" mode would be possible, and while indeed performance would be impacted, I understand that .olean files are patched after mmaping anyways?

They are only patched if they cannot be placed in their requested location, which is a random 64 bit address and therefore vanishingly unlikely to collide with any other mapped oleans even when you have many thousands or even millions

[Mario Carneiro]

unfortunately this trick just doesn't work in WASM's 32-bit address space

[Tristan Figueroa-Reid]

Mario Carneiro said:

unfortunately this trick just doesn't work in WASM's 32-bit address space

Hasn't memory64 support already landed on chrome?

[Tristan Figueroa-Reid]

It's available on both Chrome and Firefox.

[Tristan Figueroa-Reid]

Emilio Jesús Gallego Arias said:

What other challenges would be there? Modern WASIX / Rust WASM toolchain, while not standard, support a large number of extensions and libuv, so (from the bench, and obviating library size), trying a WASM build shouldn't be too far?

I would be surprised if unofficial extensions are necessary to run essential parts of lean4. If they are, I would be against such a port. I would guess that WASM's family of stage 4 & 5 proposals are enough.

[Tristan Figueroa-Reid]

Pim Otte said:

1. vscode.dev with a Lean WebExtension: This would enable using Lean without installing anything, code and cache would still be stored on the users file system.
2. Client-side (and customizable) live.lean-lang.org. This would enable courses where a more light-weight experience is desirable. Client-side is important because then bigger courses won't put undue burden on live.lean-lang.org. Customizable is important to enable teachers to setup environments for exercises (In particular, I'm thinking of Verbose Lean here).

I don't think these would be particularly useful cases unless cache was improved. The current lean4web way is the best way to do this, unless I'm unaware of any stressors being placed on the lean web server.

Pim Otte said:

3. Interactive text-books. I'm thinking along the lines of the test that Alex Kontorovich created recently. This test uses live.lean-lang.org, which I think is fine for a test, but (in my opinion) does not quite suffice in general for the reasons mentioned above.

This is something that has more motivation. Embedded applications of lean4 into sites that do not use mathlib seem very exciting. For example, this seems quite nice to have for some of the lean4 games.