Minimal requirements for using Lean (through VSCode)

Stream: general

[Lessness]

Hello!

VSCode Lean extension lags often. It's possible to work with it, but there is patience needed.
So, what are minimal requirements? So that I know what my computer lacks.

(No such problems with CoqIde - editor for Coq.)

[Lessness]

My current hardware:

Processor   11th Gen Intel(R) Core(TM) i3-1115G4 @ 3.00GHz   3.00 GHz
Installed RAM   4.00 GB (3.75 GB usable)
System type 64-bit operating system, x64-based processor

[Patrick Massot]

I'm sorry but I think there is no way you can hope to use Lean with so little RAM.

[Patrick Massot]

There are plans to prevent Lean from checking the same proofs over and over again, but we are not there yet.

[Patrick Massot]

You can play online on https://live.lean-lang.org/ or on Gitpod or GitHub codespaces.

[Kevin Buzzard]

Using gitpod or codespaces is a common solution to this problem (at least with undergraduates at my university with low spec machines)

[Shreyas Srinivas]

@Lessness : There are a few tricks you can use to reduce the problem: Write smaller lemmas, even seemingly trivial ones, and write the proofs in multiple files. But with 4GB Ram, even CoqIDE will start chugging at some point when your files get large enough. Vscode itself is a substantial memory hog. It is a fact of life that a lot of modern PC software is not written for low spec machines. It is simply too costly to do so.

[Yaël Dillies]

I will second Patrick that you should really try using gitpod.io. You get 50 hours free every month and if you drop them an email saying you are contributing to open source software, they bump that upto 250 hours.

[Eric Wieser]

(gitpod is 8GB of RAM by default, which probably still isn't great)

[Alex J. Best]

Eric Wieser said:

(gitpod is 8GB of RAM by default, which probably still isn't great)

but its also not running as much of a full os on the same machine I guess, so you probably get more of that 8 for lean than you do with an 8gb laptop say, where you also have a browser and zulip open as part of your workflow

[Yaël Dillies]

I've found gitpod's 8GB of RAM to be largely enough most of the time.

[Lessness]

Yaël Dillies said:

I will second Patrick that you should really try using gitpod.io. You get 50 hours free every month and if you drop them an email saying you are contributing to open source software, they bump that upto 250 hours.

Receive 50 hours of usage per month by connecting your LinkedIn account.
Without LinkedIn account it is only 10 hours per month. Ok, that means I'm making LinkedIn account finally... :D

[Yaël Dillies]

Oh they must have changed it :rolling_eyes:

[Rob Lewis]

These days I prefer Codespaces to Gitpod, the VSCode extension is particularly convenient!

[Rob Lewis]

Although I see Gitpod has a VSCode extension now too...

[Lessness]

Thank you all! Now using Gitpod for Lean proofs and it is comfortable experience.
Now Lean thinks and reacts reasonably/comfortably fast. :partying_face: