Zulip Chat Archive

Stream: general

Topic: cpu on mac


view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 09:18):

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

view this post on Zulip 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

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 09:21):

Just opened the workspace

view this post on Zulip Mario Carneiro (Aug 13 2018 at 09:24):

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

view this post on Zulip Mario Carneiro (Aug 13 2018 at 09:24):

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

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 09:25):

thanks, I'll try

view this post on Zulip 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.

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 09:28):

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

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 09:28):

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

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 09:29):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:07):

are there yellow bars in the gutter of vscode?

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 10:09):

nope

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 10:10):

only green, blue and red

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:10):

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

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 10:11):

oh actually, yes, in some files

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 10:12):

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

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:13):

maybe it would be best to wait for Kevin

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 10:15):

O

view this post on Zulip 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: May 10 2021 at 00:31 UTC