Zulip Chat Archive
Stream: lean4
Topic: Random lake build curiosity
Julian Berman (May 08 2024 at 14:28):
This is pure useless curiosity, but just having finished building Mathlib on 4.8.0-rc1 for the first time, the last lines in lake build
's output are:
[1181/4463] Building Mathlib.GroupTheory.Exponent
[1507/4463] Building Mathlib.Algebra.Category.FGModuleCat.Limits
where the numbers on the left there are quite low obviously -- I've imported some deep file and it does seem like the build has completed and is OK overall -- I know lake previously counted in "chunks" rather than file by file as it built each one -- is there any reason though now why I'd see numbers like that rather than counting all the way towards 4463?
Julian Berman (May 08 2024 at 14:30):
(I'll mention my ssh connection dropped once, so indeed this is 2 separate lake build
s rather than just one -- but still it did indeed finish with those two files when I resumed, seemingly.)
Last updated: May 02 2025 at 03:31 UTC