Zulip Chat Archive

Stream: lean4

Topic: Lean 4 as an application language


Jesper Nordenberg (Aug 01 2022 at 08:27):

Hi, the Lean 4 language looks amazing and it would be awesome to use as an application language (currently I use Scala and Rust, but would prefer a pure FP language with dependent types). How viable is it to use as a general application development language currently (I believe that's at least a minor goal)? I use Scala.js a lot, which is great, and I don't believe Lean 4 has a JS backend. How much effort would it be to create a JS (or WASM) backend?

Mario Carneiro (Aug 01 2022 at 08:33):

There have been talks about making a WASM backend, but in the short term that would probably only be compiling the generated C code to WASM

Mario Carneiro (Aug 01 2022 at 08:33):

which is what we already do for the in-browser version of lean

Sebastian Ullrich (Aug 01 2022 at 08:34):

And there's not much wrong with that, I believe

Sebastian Ullrich (Aug 01 2022 at 08:34):

Prior discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20and.20WASM/near/242384891

Huỳnh Trần Khanh (Aug 01 2022 at 08:36):

Would it be wise to make a WASM backend that directly emits WASM? I think it might be useful because if we emit WASM directly, we can emit a much smaller file.

Huỳnh Trần Khanh (Aug 01 2022 at 08:36):

I'm just asking. I'm not demanding anything, I swear!

Mario Carneiro (Aug 01 2022 at 08:36):

@Siddharth Bhat was looking into that as a possible project

Mario Carneiro (Aug 01 2022 at 08:38):

but also, keep in mind that if you directly emit WASM then you aren't getting any e.g. LLVM optimizations

Sebastian Ullrich (Aug 01 2022 at 08:40):

I'm not sure why a direct backend would generate smaller code than, say, LLVM optimizing for size; what makes you believe that? And as Mario said, you may still want some optimizations for speed. I don't know if anyone's profiled the costs and benefits of AOT optimization regarding the different WASM JITs yet.

Jesper Nordenberg (Aug 01 2022 at 08:50):

@Mario Carneiro Ok, that's possible of course, but maybe not the fastest turn around during development as LLVM is quite slow. With Scala.js the re-compilation is basically instant for small projects.

Mario Carneiro (Aug 01 2022 at 08:52):

Okay, but writing a good optimizing compiler is a tremendously huge project so it would be reasonable to expect that any homebrew solution will be much worse than an off-the-shelf compiler framework

Mario Carneiro (Aug 01 2022 at 08:53):

For lean, you can run things on the spot as interpreted, but the compiler takes a bit longer

Jesper Nordenberg (Aug 01 2022 at 08:54):

@Mario Carneiro I'm thinking more of a development build for quick iteration, and then use LLVM for final release build. This is basically what Scala.js does (but compiles to JavaScript instead)

Jesper Nordenberg (Aug 01 2022 at 08:55):

Mario Carneiro said:

For lean, you can run things on the spot as interpreted, but the compiler takes a bit longer

Hmm, but that doesn't work if you call from JS or use browser API's right?

Mario Carneiro (Aug 01 2022 at 08:55):

During development, you get live response in the editor. That's as quick iteration as you could ever ask for

Mario Carneiro (Aug 01 2022 at 08:55):

You can even run JS code on the spot in the widget view

Mario Carneiro (Aug 01 2022 at 08:57):

I don't know that much about scala.js but I don't think lean is trying to be a direct competitor

Jesper Nordenberg (Aug 01 2022 at 08:58):

Mario Carneiro said:

During development, you get live response in the editor. That's as quick iteration as you could ever ask for

Ok, where is this online editor?

Jesper Nordenberg (Aug 01 2022 at 09:00):

Mario Carneiro said:

I don't know that much about scala.js but I don't think lean is trying to be a direct competitor

It's just compiling Scala code to JS, with libraries providing access to JS API's (basically FFI). It uses the JS GC though.

Mario Carneiro (Aug 01 2022 at 09:00):

The editor is VSCode, which is an electron app so it integrates with a node.js backend IIUC

Mario Carneiro (Aug 01 2022 at 09:01):

I wouldn't recommend the online editor for serious application development

Jesper Nordenberg (Aug 01 2022 at 09:02):

But let's say I want to call a Lean 4 function from JS and then render stuff in a HTML canvas, then I would have to compile to WASM using LLVM?

Mario Carneiro (Aug 01 2022 at 09:02):

I'm saying you can literally do this in the editor, it shows up on the right side panel

Jesper Nordenberg (Aug 01 2022 at 09:04):

Hmm, in VS Code? Where would my canvas be rendered?

Mario Carneiro (Aug 01 2022 at 09:06):

It's a little outdated, but here's an example of a widget application: https://github.com/TwoFX/sudoku

Kevin Buzzard (Aug 01 2022 at 09:06):

Here's another one (Lean 3): https://github.com/kendfrey/rubiks-cube-group

Jesper Nordenberg (Aug 01 2022 at 09:07):

Oh, that's really cool! :smile:

Jesper Nordenberg (Aug 01 2022 at 09:09):

So, you can also add user interaction, timers etc. on the page and re-evaluate Lean functions?

Mario Carneiro (Aug 01 2022 at 09:14):

The whole lean document is kept up to date, it's not like python worksheets where you have to run them in order. So re-evaluation happens transparently: if you edit the code you see the changes immediately

Mario Carneiro (Aug 01 2022 at 09:15):

and yes, you can put user interface elements in the page to interact with the widget

Mario Carneiro (Aug 01 2022 at 09:16):

I think one of those puzzle game examples allowed you to click on the puzzle and it would add the corresponding move to the source code

Jesper Nordenberg (Aug 01 2022 at 09:25):

@Mario Carneiro Can't seem to find that. How would I call/eval a Lean function from a JS function?

Mario Carneiro (Aug 01 2022 at 09:26):

@Edward Ayers and @Wojciech Nawrocki are the ones to ask about Lean/JS integration

Wojciech Nawrocki (Aug 01 2022 at 09:42):

Jesper Nordenberg said:

Mario Carneiro Can't seem to find that. How would I call/eval a Lean function from a JS function?

Wow good timing, I am literally writing a tutorial on this now (for Lean 4) :) I can ping you when it's done.

Jesper Nordenberg (Aug 01 2022 at 09:48):

@Wojciech Nawrocki That would be awesome! I'm considering using it for simple game development, like updating game state based on user input and re-drawing a canvas or WebGL (similar to Elm examples).

Wojciech Nawrocki (Aug 01 2022 at 10:00):

Jesper Nordenberg said:

Wojciech Nawrocki That would be awesome! I'm considering using it for simple game development, like updating game state based on user input and re-drawing a canvas or WebGL (similar to Elm examples).

Then the Lean/JS interface will probably not be of much help to you, unfortunately. In this case "calling Lean from JS" means "making a remote procedure call", with JS running in a browser (or VSCode, which is a browser) and Lean running in the Lean language server. This is useful for accessing objects such as Environments and Exprs which live in the server, but not so much for general-purpose "I would rather write this function in Lean" programming. Anything low-latency has to be written in JS. As others noted above, it would also be possible to compile Lean to JS/WASM so that it can run in the client, but afaik noone has gotten that to work so far.

Jesper Nordenberg (Aug 01 2022 at 10:08):

@Wojciech Nawrocki Yes, I realize that. I don't care much about performance during the initial development phase (it doesn't have to be realtime). And for later release build I would definitely compile to WASM using LLVM. But maybe I'm too early adopter of Lean 4 for such an application :)

Wojciech Nawrocki (Aug 01 2022 at 10:18):

@Jesper Nordenberg another way to put it is that we currently have a way to invoke a remote Lean server from JS, but no way to invoke Lean code within the same execution environment that the JS is running in. So it's not just a question of performance but also ABI - to make RPC calls to remote Lean you need to encode data in various ways whereas a local call could pass it around directly. Additionally when the remote server is actually remote (i.e. on a separate machine rather than a different process on the same machine), the latency can be up in hundreds of ms which means you can really only make such calls sparingly.

Jesper Nordenberg (Aug 01 2022 at 10:28):

@Wojciech Nawrocki Ok, I suppose the only viable way is to compile to WASM then for testing

Reinier van der Gronden (Aug 08 2022 at 12:44):

@Wojciech Nawrocki is your method of calling a Lean function from JS different from the User Widgets? I'm investigating this right now because I want to talk between Lean code and infoview for code improvement suggestions, but it seems that one of your latests point on having to encode all data to the Lean server complicates the use of TacticM, because all MVars and contexts are likely difficult to communicate, currently widgets seem to build on top of TermElabM.

Wojciech Nawrocki (Aug 08 2022 at 13:10):

@Reinier van der Gronden no, it is exactly the method described there. Here is an example of how we can send a tactic context to and from the infoview. I suppose we should also have a section about this in the User Widgets tutorial.

Reinier van der Gronden (Aug 09 2022 at 09:51):

@Wojciech Nawrocki Thanks for that pointer, I'll take a look!


Last updated: Dec 20 2023 at 11:08 UTC