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: May 16 2021 at 22:14 UTC