Zulip Chat Archive

Stream: new members

Topic: Compilation time of each theorem


Martin Dvořák (Dec 19 2022 at 16:05):

Can I view the compilation time of each theorem? I'd like to run one command that will do it for my project, without needing to modify multiple files.

Kevin Buzzard (Dec 19 2022 at 16:07):

In Lean 3? set_option profiler true

Martin Dvořák (Dec 19 2022 at 16:40):

Yes, in Lean 3.

Where can I write the command?

Kevin Buzzard (Dec 19 2022 at 16:40):

before the place where you want Lean to start telling you how long it takes to compile each declaration

Martin Dvořák (Dec 19 2022 at 16:43):

And to do it for all files in my project?

Kevin Buzzard (Dec 19 2022 at 16:44):

Oh I see, I had misread the question. Apologies. I don't know.


Last updated: Dec 20 2023 at 11:08 UTC