LEAN 4

Stream: general

[MOHAMMAD]

Hello, Is there a way to download LEAN4 Without using VS code?

[Ira Fesefeldt]

You can install the compiler using lean version manager called elan, see here. You can create a project and build a project using the lean 4 package manager called lake that is installed along lean4.

But neither of them give you an interactive theorem proving view. So if you actually would like to prove anything in lean, it is recommended to use any editor that uses the language server procotol - such as vscode, emcas and others

[Jireh Loreaux]

I think neovim is currently the only other supported editor besides those two

[Yury G. Kudryashov]

With emacs being only half supported (I'm the current maintainer and I don't have much time for it)

[Eric Rodriguez]

There's also the lean web playground (live.lean-lang.org) but that's basically VSCode with extra steps

[Shreyas Srinivas]

Is there a way to package leanweb into a self-contained executable that can be run locally

[Jon Eugster]

Shreyas Srinivas said:

Is there a way to package leanweb into a self-contained executable that can be run locally

Yes that's called "download vscode" ;)

But jokes aside, you can download lean4web from github install npm and run your local server using npm start. So any of of these steps could be bundled,
for example using a docker container. There might also be other tools to bundle react/npm apps, but I dont know them.

The question is why though? What's the benefit of having a local bundle running a (slightly broken) trimmed down "monaco editor" locally (which doesn't really support saving your progress) instead of using vscode? If there is a good use case, you can open an feature request issue.

[Shreyas Srinivas]

Sometimes I just like a playground I can open with one click without the internet (especially when Deutsche Bahn decides that wasting an hour of my time is cheaper than adding more rail lines). It might also come in handy for demos where people don't have to install lean, just download an AppImage or something.

[Yaël Dillies]

Shreyas Srinivas said:

Sometimes I just like a playground I can open with one click without the internet

Is that not vscode?

[Shreyas Srinivas]

Yaël Dillies said:

Is that not vscode?

Minus installation, setup time, and debugging errors

[Shreyas Srinivas]

It isn't a complete setup. Just a GUI app serving the same role as utop or the ipython terminal.

[Eric Wieser]

Shreyas Srinivas said:

Yaël Dillies said:

Is that not vscode?

Minus installation, setup time, and debugging errors

Those steps will surely happen when installing leanweb too?

[Shreyas Srinivas]

Presumably not if they ship with an image of some sort?

[Eric Wieser]

Why not ship vscode in an image of some sort, if you want an image?

[Eric Wieser]

I think for most users, installing such an image is more work than installing vscode

[Jon Eugster]

didn't we use to have some "try-lean bundles"? Are they still a thing and do they work this way?

[Shreyas Srinivas]

Eric Wieser said:

Why not ship vscode in an image of some sort, if you want an image?

Because VSCode is a complicated beast. A playground should take you straight to the editor with an empty math project already setup. It is not meant to be used for projects, so it doesn't have to support all the complex features of vscode. The playground should not store user files unless explicitly asked to. The basic project being used should always be a fresh project.

To a user it should not even show a file (much like the web editor). If the user wants, they can save files to a separate location

[Shreyas Srinivas]

In addition it must handle updates in the background. Its job is to provide newbies the latest and greatest lean has (toolchain, mathlib, paperproof, etc) in a consistent manner and let users fiddle around. It should not be offering features for complex project management. (EDIT : This is basically what lean web already does)

[Kim Morrison]

Webpage in a container seems strictly worse to me than a webpage, but @Shreyas Srinivas if you wanted to build and maintain such an image we could find out how useful it was!

[Shreyas Srinivas]

I'll try

[Eric Wieser]

Shreyas Srinivas said:

Because VSCode is a complicated beast. A playground should take you straight to the editor with an empty math project already setup.

Is this different from having an empty math project on your machine that you just reuse?

[Yury G. Kudryashov]

@Eric Wieser As far as I understand, the idea is that new users download 1 file, run it, and get a preconfigured VSCode+mathlib+empty project.

[Jon Eugster]

@Shreyas Srinivas if you build anything thelike based on lean4web, we can maybe have github CI in the lean4web repo automatically create and publish it. (only thing I wouldnt know how to do is testing in CI whether the image is working correctly)

[Shreyas Srinivas]

What Yury says. The idea is people don't think about setup or files and folder structure at all. Just download a fancy electron app and give it a spin. Once they like it, they can setup lean properly with vscode. And also it might be handy for trying out stuff from time to time

[Mark Fischer]

Vs Code can be stripped down/reconfigured significantly with a little bit of work until it acts effectively like a playground. I like to do something like this when learning a language so I just double-clip an icon and get a fresh environment to mess about in.

Something I haven't tried but should be manageable is to compress everything you need into a single file and write a script that sets everything up without needing an internet connection. You don't get the newest version or anything.

That's a bit easier on an end user than configuring Vs Code from scratch, though just a bit! You would still need to maintain — and they still need to acquire — the right file for their environment.

[Patrick Massot]

Aren’t we reinventing the trylean bundles here?

[Shreyas Srinivas]

Patrick Massot said:

Aren’t we reinventing the trylean bundles here?

There was a discussion about this after the port. I am not sure it ever reached fruition.

[Kim Morrison]

Yes, we are reinventing the bundles, but this is still something that needs to be done for Lean 4. It would be great if someone enthusiastic about bundles set one up, along with CI that will keep it tested and fresh.

[Shreyas Srinivas]

I will give it a shot. Time is my main constraint, so it might take a few weeks