Zulip Chat Archive

Stream: new members

Topic: Telling what lean is currently building (vs code)


view this post on Zulip Eric Wieser (Jul 30 2020 at 10:26):

I'm editing files in mathlib, and finding that the orange "busy" bar spans my entire file for a very long time.

This presumably means that lean is rebuilding a dependent file in the background. Is there any way for me to find out which one?

view this post on Zulip Kenny Lau (Jul 30 2020 at 10:36):

well you can do lean --make [current file] in terminal

view this post on Zulip Kenny Lau (Jul 30 2020 at 10:36):

and look at the output


Last updated: May 09 2021 at 19:11 UTC