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 builds 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