install own lean web server?

Stream: general

[Thorsten Altenkirch]

I want to use the lean web interface in my lecture notes.

I am wondering wether I should install my own server? I am concerned about load and maybe one day I want to have a specific environment. How to do this?

[Johan Commelin]

I guess @Bryan Gin-ge Chen and @Edward Ayers are the experts here

[Edward Ayers]

Hi I wrote a doc about setting up an aws server with lean web interface

[Edward Ayers]

I’ll hunt it down

[Bryan Gin-ge Chen]

The Lean web editor runs entirely in the user's browser, so all that's required is a "static" host.

[Bryan Gin-ge Chen]

I just checked very quickly and I think the instructions here should work. The fetch_lean_js.sh will download the most current version of the Lean web files into the dist/ directory. By default, it includes a ZIP file with a precompiled version of mathlib, which is ~36 MB. If you can get by with just the core libraries, then you can edit the script to change library to libcore to download a ~2 MB ZIP file instead. You can also customize things further by following the directions here to use the mk_library.py script.

[Edward Ayers]

Here are my personal notes from setting up a webserver in aws. I don't know if they still work and they shouldn't be treated as a sure fire walkthrough but might be of some use: https://github.com/EdAyers/lean-web-editor/blob/widget/aws-setup.md

[Patrick Massot]

I use the Lean web editor in a completely static environment on my university webpage, I can guarantee you don't need anything fancy. And everything is explained at https://github.com/leanprover-community/lean-web-editor/blob/master/README.md

[Thorsten Altenkirch]

Ah I wondered and wrongly came to the wrong conclusion! Is lean compiled to JavaScript or how does it work.

[Kevin Buzzard]

Yes lean is compiled to JS

[Bryan Gin-ge Chen]

Lean is compiled to JS and WebAssembly using Emscripten. Most users with reasonably modern browsers should be using the WASM version.