leanproject build mathlib

Stream: new members

[Yakov Pechersky]

When making an edit on a branch of mathlib, I'd like to check locally first if anything breaks before going through the whole CI process. Is the best way to do this leanproject build? Is there a way to parallelize the build?

[Yakov Pechersky]

Seems to be automatically parallel.

[Yakov Pechersky]

Particularly, is the python scripts/detect_errors.py from the CI available to run locally?

[Bryan Gin-ge Chen]

What do you mean by "available to run locally"? It's in the scripts/ directory in the mathlib repo.

See also lean#454.

[Yakov Pechersky]

That lean issue is basically what I'm thinking about.

[Kevin Buzzard]

I just use lean --make src but I might be old school

[Yakov Pechersky]

lean --make src has the same issue

[Reid Barton]

If there are errors I use leanpkg build 2>&1 | less