Adding imports to live lean

Stream: lean4

[Patrick Massot]

@Jon Eugster how hard would it be to allow using extra imports on live.lean-lang.org? Adding one single file on top of Mathlib would already be extremely useful. Once again I have to give a two hours long introduction to Lean for curious mathematicians. Installing Lean+mathlib would use up all the time and getting GitPod or GitHub codespaces to work is almost as painful. Using live.lean-lang.org is almost perfect for this, but this requires starting the demo file with distracting code setting up stuff. Having an url that loads stable mathlib + one file taken from a remote webpage would be great.

[Patrick Massot]

A big hack that would be functionally just as good would be to take an extra url argument saying to hide the first N lines of the file in the editor.

[Patrick Massot]

Or equivalently, instead of sending only the file to the lean server, prepend the given extra code.

[Ruben Van de Velde]

That sounds like it would break people using import in that setting, though presumably that's not a worry for your case

[Patrick Massot]

Yes, the hack is clearly a hack that is not great. But it would allow this specific use case, without breaking anything for people not using it.

[Joachim Breitner]

Would it help you if it was easy to run your own instance of the service, with whatever projects added to the drop down? It would take a bit of setup (renting a server, running some deployment), although it could probably be made very simple.

[Patrick Massot]

The big question is how big should the server be.

[Patrick Massot]

I think it is very worthwhile to make it easy for people to setup such servers, including very clear instructions and explanation about the required resources.

[Patrick Massot]

But I still think that supporting the above hack would be useful for many people who wouldn’t bother to setup their servers.

[Joachim Breitner]

Would being able to run your own server solve an immediate need of yours, or are you ok with the status quo for now?

[Patrick Massot]

The hack described above would solve my immediate need and seems rather easy to implement.

[Patrick Massot]

I should also say that “immediate” in “immediate need” means before Friday next week, not today.

[Joachim Breitner]

I don’t know if Jon feels like implementing hacks, though :-)

[Julian Berman]

I'm not sure how trivial this actually would be -- it looks like https://github.com/microsoft/monaco-editor/issues/45 is still open which seems like this functionality -- it references setHiddenAreas as being a private API for doing this in monaco (so it may indeed work, I was trying to just call it client-side, but I don't speak enough React to know where to get access to the monaco instance on the live site.

[Jon Eugster]

The easiest "hack" right now would be that you just set up a Lean project with mathlib and all your content and either convince Joachim to copy that project to the FRO server tell me to load it to https://lean.math.hhu.de. I'm happy to have the project added there

I did this with DuperDemo

Your students them still have to start the file with import YourDemo, but that might not be as confusing

[Patrick Massot]

I know about this hack, but I still think it would be nice to have something everybody can use.

[Jon Eugster]

For sure that would be nice! I'm just saying I'm unfortunately not going to be the person to implement anything like that anytime soon.

And as a side-note, since the responsible people at the FRO seem to be pretty indifferent about making the VSCode-extension browser-compatible (see tracking PR), I'm currently pretty unmotivated to spend any time on updating lean4web, fixing or adding things. As long as running code snippets from Zulip using the latest Mathlib works, I'm pretty happy :)