Zulip Chat Archive

Stream: new members

Topic: leanproject build mathlib


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?

Yakov Pechersky (Aug 24 2020 at 22:51):

Seems to be automatically parallel.

Yakov Pechersky (Aug 24 2020 at 22:52):

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

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.

Yakov Pechersky (Aug 24 2020 at 23:02):

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

Kevin Buzzard (Aug 24 2020 at 23:04):

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

Yakov Pechersky (Aug 24 2020 at 23:05):

lean --make src has the same issue

Reid Barton (Aug 24 2020 at 23:07):

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


Last updated: Dec 20 2023 at 11:08 UTC