Zulip Chat Archive

Stream: general

Topic: cpu on mac


Yulia Zaplatina (Aug 13 2018 at 09:18):

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

Mario Carneiro (Aug 13 2018 at 09:20):

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

Yulia Zaplatina (Aug 13 2018 at 09:21):

Just opened the workspace

Mario Carneiro (Aug 13 2018 at 09:24):

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

Mario Carneiro (Aug 13 2018 at 09:24):

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

Yulia Zaplatina (Aug 13 2018 at 09:25):

thanks, I'll try

Kevin Buzzard (Aug 13 2018 at 09:27):

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 (Aug 13 2018 at 09:28):

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

Yulia Zaplatina (Aug 13 2018 at 09:28):

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

Yulia Zaplatina (Aug 13 2018 at 09:29):

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

Kevin Buzzard (Aug 13 2018 at 09:37):

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 (Aug 13 2018 at 10:05):

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 (Aug 13 2018 at 10:07):

are there yellow bars in the gutter of vscode?

Yulia Zaplatina (Aug 13 2018 at 10:09):

nope

Yulia Zaplatina (Aug 13 2018 at 10:10):

only green, blue and red

Mario Carneiro (Aug 13 2018 at 10:10):

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

Yulia Zaplatina (Aug 13 2018 at 10:11):

oh actually, yes, in some files

Yulia Zaplatina (Aug 13 2018 at 10:12):

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

Mario Carneiro (Aug 13 2018 at 10:13):

maybe it would be best to wait for Kevin

Yulia Zaplatina (Aug 13 2018 at 10:15):

O

Yulia Zaplatina (Aug 13 2018 at 10:16):

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


Last updated: Dec 20 2023 at 11:08 UTC