setting up local lean server for online use by students?

Stream: Lean for teaching

[Mark Aagaard]

Is it feasible for me to setup a local lean server for students to use Lean on the web, similar to https://live.lean-lang.org/, where I can preload libraries for the students to use? If so, are there instructions for how to do this?

I'm using Lean in an undergrad course with 150 students running Lean on their own computers. There are the usual collection of odd behaviours that the students encounter. Most the problems are caused by students not following the installation instructions, or having oddly configured computers. Having a web version would be nice for students who are having difficulty installing Lean themselves.

-mark

[Kevin Buzzard]

Is gitpod not a good solution for you?

[Kevin Buzzard]

See for example the README of my FLT project https://github.com/ImperialCollegeLondon/FLT : just under the title there's a "gitpod - ready to code" link and if you click there then you get an online version of the FLT project with a fully compiled mathlib.

[François G. Dorais]

Gitpod still requires using vscode. Usually not a big deal but a solution that does not require installing any software would be better.

[Eric Wieser]

No it doesn't! (edit: it doesn't require installing VSCode. You have to know how to use the vscode clone that gitpod sends you to of course)

[Julian Berman]

Technically gitpod doesn't require that either, you can use it just fine with e.g. lean.nvim as well (instructions are here). Though I doubt that's the concern in a teaching channel?

[François G. Dorais]

Sorry, I wrote that totally wrong. Students have to join (not install) gitpod, which may not be approved.

[François G. Dorais]

At my university, there is an approval process for any thing that might store student data on servers not controlled by the university. This is not really enforced and we still ask our students to use things that haven't (yet) been approved, but we're breaking the rules anytime we do that.

[Shreyas Srinivas]

Have you looked at distributing devcontainers?

[Shreyas Srinivas]

Mathlib has devcontainers

[Shreyas Srinivas]

You need to install vscode but after that you can ask students to open the devcontainer that you provide

[Shreyas Srinivas]

As a last resort, you can use an old trick, which is distributing virtualbox VMs with lean pre-installed, and a project directory setup

[Mark Aagaard]

I just quickly setup a gitpod clone of Kevin Buzzard's FLT environment. It provides the features that I want, but I am concerned about asking students to create an account at an external organization.

I haven't investigated dev containers yet. My first choice to have a web interface, so that the students don't have to install anything and I can update the environment easily.

-mark

[Shreyas Srinivas]

Gitpod allows self hosting, but I have to guess this will cost a bit: https://www.gitpod.io/contact/enterprise-self-serve

[Shreyas Srinivas]

(deleted)

[Julian Berman]

There are good other tools for self-hosting devcontainers a la Gitpod. The one I've seen is... https://github.com/loft-sh/devpod

[Julian Berman]

It'd probably be nice if some day someone tries that out with Mathlib for exactly the reason Francois mentions (which technically I've run into in the past as well...).

[Shreyas Srinivas]

One thing I learnt about platform agnostic no install process is that someone somewhere has to install docker

[Julian Berman]

Yep definitely, but things like binder hub or that devpod thing mean hopefully the "someone somewhere" is "your uni's container cluster" and not any individual student.

[Jon Eugster]

to quickly circle back on the original question, installing lean4web on your own servwr and letting it run your custom lean project (with whatever dependencies you want. The instructions are at the github repo:

https://github.com/leanprover-community/lean4web

(which btw is directly linked from the menu of live.lean-lang.org)

If you run into troubles or have questions, please DM me anytime, I can help:blush: (or maybe be coerced into improving the docs :wink:).

For having 150 students on it simultaneously (all using mathlib) you probably need quite a powerhorse of a server... I dont have the numbers in my head right now, you might need to do some testing again yourself. maybe Lean does good memory sharing and all is okay, I dont exactly know/remember these technical details about how Lean processes work

[Mark Aagaard]

Thanks for the pointer to the github for lean4web. I should have taken the time to check all of the links on live.lean-lang.org. I just assumed that the github link pointed to the main github site for Lean.

-mark

[Cas Haaijman]

Did you try using lean4web? I am looking into doing a similar thing, but for ~300 students, so I am curious if this is a workload lean4web can handle.