cpu on mac

Stream: general

[Yulia Zaplatina]

Anyone had an issue with lean using > 95% cpu on mac?

[Mario Carneiro]

lean often takes up as much cpu as it can. It depends on what you are doing

[Yulia Zaplatina]

Just opened the workspace

[Mario Carneiro]

If you import a heavy theory, it may take a few minutes

[Mario Carneiro]

You can also try building the lean files with lean --make to help speed it up

[Yulia Zaplatina]

thanks, I'll try

[Kevin Buzzard]

Yulia -- I'll be in the MLC in about an hour. You might want to build your mathlib (make all the .olean files) if this is constantly happening.

[Yulia Zaplatina]

it went down to 20%, but now that i've open

[Yulia Zaplatina]

*opened a file, it's back up to over 300%

[Yulia Zaplatina]

@Kevin Buzzard I'll do that now :+1:🏼

[Kevin Buzzard]

This is not abnormal behaviour -- the first time Lean starts up it might have to do a lot of work. It could be building the real numbers from the axioms of mathematics, for example. It only needs to do this once though.

[Yulia Zaplatina]

Ok, so I've built lean and the cpu remains around 90% - is that normal? or is there a way of decreasing it even more?

[Mario Carneiro]

are there yellow bars in the gutter of vscode?

[Yulia Zaplatina]

nope

[Yulia Zaplatina]

only green, blue and red

[Mario Carneiro]

does lean have the :check: in the status bar?

[Yulia Zaplatina]

oh actually, yes, in some files

[Yulia Zaplatina]

yep, there's a :check: but some files are highlighted yellow

[Mario Carneiro]

maybe it would be best to wait for Kevin

[Yulia Zaplatina]

O

[Yulia Zaplatina]

it's down to 10 now :sweat_smile: I think it should be fine, thank you!