Computer power

Stream: general

[Martin Dvořák]

[soft question]
How much does computational power of one's computer influence their productivity in interactive theorem proving?

I think I've been underestimating this issue over the past year.
If, on average, I have to wait 10 seconds after writing every line of proof, having a stronger computer that would do it in 5 seconds on average would probably boost my productivity a lot! Maybe by 20 % or so.

What do you think?

[Ruben Van de Velde]

That five seconds is still a lot! I believe I recall that you lose your train of thought when the lag is more than about a hundred milliseconds. That's pretty unlikely for complex proofs, though

[Martin Dvořák]

I will not get it under 200 ms. Among realistic options, how much should I care about what computer I use?

[Patrick Massot]

Many serious Lean users have rather strong computers for that purpose.

[Martin Dvořák]

Any serious Lean user willing to share their computer specs?

[Patrick Massot]

Searching on Zulip will answer that question.

[Patrick Massot]

Maybe search for Ryzen for instance

[Rémi Bottinelli]

Martin Dvořák said:

[soft question]
How much does computational power of one's computer influence their productivity in interactive theorem proving?

I think I've been underestimating this issue over the past year.
If, on average, I have to wait 10 seconds after writing every line of proof, having a stronger computer that would do it in 5 seconds on average would probably boost my productivity a lot! Maybe by 20 % or so.

What do you think?

What's your setup?

[Martin Dvořák]

In short: 6x 3.6 GHz, 16 GB RAM

Details:
ASROCK X370 Killer SLI
AMD RYZEN 5 2600X
ADATA 16GB KIT DDR4 2400MHz CL17
WD Black NVMe SSD 500GB
ASUS PHOENIX GeForce GTX 1050TI 4G

[Kevin Buzzard]

Anything reasonable with 16 gigs ram should be fine

[Martin Dvořák]

Kevin Buzzard said:

Anything reasonable with 16 gigs ram should be fine

Are you suggesting that I cannot get significantly better performance than I currently have?

[Martin Dvořák]

Shouldn't the computer power scale both short and long proofs?

[Eric Wieser]

In lean3 the delay you experience when editing is linear in the length of the proof

[Martin Dvořák]

Let me split this thread into two. We are discussing two topics where each can help with the waiting times on its own.

[Notification Bot]

A message was moved here from #general > Computer power by Martin Dvořák.

[Notification Bot]

10 messages were moved here from #general > Computer power by Martin Dvořák.

[Notification Bot]

A message was moved here from #general > Tips how to speed up elaboration by Martin Dvořák.

[Notification Bot]

5 messages were moved here from #general > Tips how to speed up elaboration by Martin Dvořák.

[Martin Dvořák]

Eric Wieser said:

In lean3 the delay you experience when editing is linear in the length of the proof

At the same time, the delay should be reciprocal of the computational power, right?

[Eric Wieser]

I don't think lean usually parallelizes with a tactic block

[Eric Wieser]

Unless you use tactic#async

[Rémi Bottinelli]

What kind of parallelization/hardware acceleration are theoretically possible, I'm wondering?

[Martin Dvořák]

Lean 3 does not parallelize tactic-proof elaboration.

[Eric Wieser]

... except with async, then it does

[Martin Dvořák]

The delay should be reciprocal of the single-thread computer speed, right?

[Eric Wieser]

Plausibly. Of course, longer proofs have more things in the context, so there's sometimes a quadratic term too.

[Martin Dvořák]

The question stays: Can I get significantly better performance (of Lean elaborator on the same code) if I upgrade my PC?

[Arthur Paulino]

You can try building mathlib4 on different AWS or Azure machines before actually spending money on a new PC

[Arthur Paulino]

Or, if you SSH via VS Code you can experiment theorem proving on different machines. That would be a better experiment than just building mathlib4

[Martin Dvořák]

Wait. I can SSH via VS Code? I thought I would have to use something like remote desktop and run VS Code on the remote machine.

[Arthur Paulino]

Ah, wait, when I tried it the infoview didn't work. So I doubt you would be able to see orange bars :/

[Kyle Miller]

Martin Dvořák said:

The question stays: Can I get significantly better performance (of Lean elaborator on the same code) if I upgrade my PC?

I think the answer is simply "no" unless you can get a CPU that's significantly faster than your 3.6 GHz.

[Martin Dvořák]

Ah! Is my CPU the bottleneck?

[Kyle Miller]

That's already a very fast CPU. I think I only have access to ones with 2.4 GHz myself. I have >= 32 GB of RAM, but that's mostly useful for having way too many VS Code instances open.

[Jason Rute]

I’ve certainly used lean on a remote server via vs-code’s official ssh plugin (there is a similar plugin for Docker and Kubernetes as well). It is just like using it on my local machine. If I recall, you have to install the lean plugin again (through vs code) on the remote machine (after you have sshed in via vs code).

[Martin Dvořák]

Is it better to run IDE on your computer and outsource only the backend execution to the remote server? The alternative is to run IDE with everything on the remote server and connect via some kind of remote desktop. I have experience with neither.

[Eric Wieser]

I do all my lean development on gitpod

[Eric Wieser]

I would recommend against using a remote desktop for vscode

[Eric Wieser]

Why send a whole screen over when you can just send over text data through vscode?

[Martin Dvořák]

Eric Wieser said:

I do all my lean development on gitpod

Would you recommend it to others? Why is it good?

[Kevin Buzzard]

I never use it. It's good if the default machine at the end of it is better than the machine you are using to connect to it.

[Matthew Ballard]

When I am away from my home including at the office I use an iPad. For mobile safari, I've found no sufficient incarnation of VS Code in the browser or app. This herded me toward using (neo)vim over ssh to my home machine.

[Matthew Ballard]

For low intensity things, I set up Codespaces (and to a lesser extent GitPod) for my students. The limitations of this can quickly become clear.

[Martin Dvořák]

Matthew Ballard said:

For low intensity things, I set up Codespaces (and to a lesser extent GitPod) for my students. The limitations of this can quickly become clear.

I am also interested in this topic, but that's a separate issue. I continue here:
https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/codespaces

[Martin Dvořák]

Kevin Buzzard said:

I never use it. It's good if the default machine at the end of it is better than the machine you are using to connect to it.

Is there a chance that GitPod will provide me with a better machine than I have?

[Eric Wieser]

It does for me. 8 core 2.2GHz + 16GB on gitpod, 4 core 2.2Ghz + 8GB locally

[Eric Wieser]

Plus the 8GB locally is also doing things like running Zulip and Chrome and the vscode UI

[Eric Wieser]

So even if the gitpod machine is the same as yours there can be still be an advantage

[Reid Barton]

Eric Wieser said:

It does for me. 8 core 2.2GHz + 16GB on gitpod, 4 core 2.2Ghz + 8GB locally

But it could be the case for you but not the case for Martin, due to a linguistic feature of the word "me" known as indexicality

[Eric Wieser]

Eric Wieser said:

So even if the gitpod machine is the same as yours there can be still be an advantage

One such advantage is that you can have two open at the same time without them sharing resources

[Eric Wieser]

Of course you'll hit the quota limits pretty quickly that way unless you pay them money or ask nicely

[Martin Dvořák]

And if you pay them money, will they give you a stronger machine (in addition to being allowed to use it longer)?

[Henrik Böving]

Martin Dvořák said:

Is it better to run IDE on your computer and outsource only the backend execution to the remote server? The alternative is to run IDE with everything on the remote server and connect via some kind of remote desktop. I have experience with neither.

I got a powerful server at work that I run all my Coq stuff on remotely by telling proof general in emacs to execute the coq stuff on that other machine. And it works quite well.

Then again I only have the server because it would be doing nothing otherwise and our IT doesnt want Coq and all its libraries direclty on my work laptop :)

[Jason Rute]

@Henrik Böving forgive my naive question. Is emacs running on the server or on your computer? If the server are you using emacs through the ssh terminal, or some xwindow sort of thing?

[Niels Voss]

I don't use Emacs for Lean right now, but I think it has a system called TRAMP which let's you run Emacs on your computer and edit files on other computers. I'd imagine running programs like Coq through it would require special support so I don't know if that's what Henrik Böving does.

[Henrik Böving]

Jason Rute said:

Henrik Böving forgive my naive question. Is emacs running on the server or on your computer? If the server are you using emacs through the ssh terminal, or some xwindow sort of thing?

What Niels is explaining is also a thing but not the way this proof general stuff works. So basically both the source file of the project and emacs are on my laptop and emacs sends the text file to the remote machine for proof checking/proof search. In coq behavior like this is rather easy to implement since their editor integration is based upon their REPL which they just pipe text into. So if I tell my thing to run "ssh tonks coqtop" instead of just "coqtop" I'm on a remote machine.

[Reid Barton]

Does that mean you are editing a local file, but all its dependencies are on the remote server?

[Henrik Böving]

Correct

[Henrik Böving]

I only have a checkout of our research project on my machine, all the funky libraries that we use are on the remote machine.

[Jireh Loreaux]

For most Lean tasks, I use my decade old, 4 core, 2.5 Ghz machine, 16gb ram and it's plenty fast enough. Waiting 10 seconds for a proof is abominably slow, and it usually (admittedly not always) indicates there is something wrong with the proof or the lead up to it.

When I need more compute (e.g., I want to compile a significant portion of mathlib locally) then I ssh into my work machine (12 cores) with VS Code. It's nearly indistinguishable in usability and interface except for the extra power. On my work machine I can compile all of mathlib in about 3.5 hours