Kinda "slideshow" when working in Lean

Stream: new members

[Ilmārs Cīrulis]

It feels like Lean starts checking the currrent file I'm working in from its start too often. :( Kinda missing Rocq, if you understand. (But Rocq doesn't have Mathlib and other good things.)

Is it okay, or maybe that's a problem I need to fix somehow?

[Mario Carneiro]

You need to provide more information for this to be actionable

[Ilmārs Cīrulis]

Maybe my computer is just too slow? Could that be an explanation?

image.png

[Kevin Buzzard]

How much ram do you have?

[Ilmārs Cīrulis]

It says that 32 GB

[Kevin Buzzard]

Well that's plenty so that's not the problem

[Ilmārs Cīrulis]

I will take a look with Task Manager, maybe I see some spikes or smth, when Lean slows down. :thinking:

[Ilmārs Cīrulis]

Anyway, yes, for now this is useless post by me, more like a simple venting.

[Mario Carneiro]

you described more than just being slow

[Mario Carneiro]

you said it restarts often

[Mario Carneiro]

One thing that can help to make things more snappy is to put #exit after the proof if it's a proof in the middle of a big file

[Ilmārs Cīrulis]

Ok, if I figure out something real, then I will comment again.