## Stream: new members

### Topic: leanpkg args

#### 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.

#### 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

#### Simon Hudon (Jun 19 2019 at 01:12):

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

#### Simon Hudon (Jun 19 2019 at 01:12):

(or leanpkg -- --profile)

#### Yury G. Kudryashov (Jun 26 2019 at 18:51):

@Simon Hudon Thank you

Last updated: May 18 2021 at 16:25 UTC