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
libcore to download a ~2 MB ZIP file instead. You can also customize things further by following the directions here to use the
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):
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: May 16 2021 at 05:21 UTC