leanpkg args

Stream: new members

[Yury G. Kudryashov]

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.

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

(or leanpkg -- --profile)

[Yury G. Kudryashov]

@Simon Hudon Thank you