Zulip Chat Archive

Stream: new members

Topic: leanpkg args


view this post on Zulip Yury G. Kudryashov (Jun 18 2019 at 20:39):

Hi,
Is it possible to
(a) make leanpkg build stop at the first error like the normal make does?
(b) get per-file build time stats?
(c) same, but per-def/lemma in a file?

I want (a) when I change some defs, and want to fix all newly broken files one by one, and (b)/(c) to know I should look at if I want to speed up the compilation process.

view this post on Zulip Simon Hudon (Jun 19 2019 at 01:11):

For a), look at scripts/detect_errors.py in mathlib, we had to hack it together for the travis build

view this post on Zulip Simon Hudon (Jun 19 2019 at 01:12):

For b) and c), have you looked at lean --profile?

view this post on Zulip Simon Hudon (Jun 19 2019 at 01:12):

(or leanpkg -- --profile)

view this post on Zulip Yury G. Kudryashov (Jun 26 2019 at 18:51):

@Simon Hudon Thank you


Last updated: May 18 2021 at 16:25 UTC