Zulip Chat Archive

Stream: new members

Topic: leanproject build mathlib


view this post on Zulip Yakov Pechersky (Aug 24 2020 at 22:47):

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?

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 22:51):

Seems to be automatically parallel.

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 22:52):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 24 2020 at 22:54):

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

See also lean#454.

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 23:02):

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

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 23:04):

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

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 23:05):

lean --make src has the same issue

view this post on Zulip Reid Barton (Aug 24 2020 at 23:07):

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


Last updated: May 16 2021 at 22:14 UTC