Zulip Chat Archive

Stream: general

Topic: install own lean web server?

Thorsten Altenkirch (Sep 12 2020 at 15:27):

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 (Sep 12 2020 at 15:38):

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

Edward Ayers (Sep 12 2020 at 15:39):

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

Edward Ayers (Sep 12 2020 at 15:40):

I’ll hunt it down

Bryan Gin-ge Chen (Sep 12 2020 at 15:40):

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

Bryan Gin-ge Chen (Sep 12 2020 at 15:49):

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 (Sep 12 2020 at 15:53):

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 (Sep 12 2020 at 17:27):

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 (Sep 13 2020 at 12:17):

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

Kevin Buzzard (Sep 13 2020 at 12:18):

Yes lean is compiled to JS

Bryan Gin-ge Chen (Sep 13 2020 at 16:34):

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

Last updated: Dec 20 2023 at 11:08 UTC