Zulip Chat Archive
Stream: general
Topic: Lean re-builds
Simon Hudon (Jul 11 2018 at 22:32):
@Sebastian Ullrich What criterion does leanpkg use to decide whether a certain file has to be rebuilt or not? I'm caching .olean files on travis and the whole thing gets rebuilt anyway. If I also cache .lean files, then the rebuild is more conservative.
Gabriel Ebner (Jul 11 2018 at 22:50):
It's modification time.
Simon Hudon (Jul 11 2018 at 22:52):
It's curious that caching doesn't play well with that.
Simon Hudon (Jul 11 2018 at 22:52):
Is the .lean modification time recorded inside the .olean file?
Gabriel Ebner (Jul 11 2018 at 22:56):
No, but we also compare the olean modification times with the imports. So the olean files need to be newer than the lean files and also in the same temporal order as the import order.
Simon Hudon (Jul 11 2018 at 23:47):
Yes, I noticed that. Caching ~/.elan became necessary for any .olean files to be reused at all
Mario Carneiro (Jul 17 2018 at 01:14):
@Simon Hudon Do you know what is up with the latest build failure? https://travis-ci.org/leanprover/mathlib/jobs/404668129 It seems like travis_long is messing with some kind of change detection
Simon Hudon (Jul 17 2018 at 01:18):
what might be happening is a sort of race condition: some builds share the same cache (for example, the builds of the same branch) so it's possible that one build finishes its stage one, uploads its new version of the cache, then the other build does the same and then the first build tries to start its stage two. I have guarded stage two so that it fails when the binaries in the cache were built from a different commit. The only thing to do is to restart the build.
Simon Hudon (Jul 17 2018 at 01:19):
One may try to remove that guard but what would happen then is that Travis would try to redo all the work of stage 1 only to fail at the end.
Simon Hudon (Jul 17 2018 at 01:19):
I chose to make it fail as quickly as possible
Simon Hudon (Jul 17 2018 at 01:29):
That will probably happen at time of high affluence. It's annoying but it should still be better than before. Would it make it better if it sent you an email when it happens?
Mario Carneiro (Jul 17 2018 at 01:30):
I always get an email when it fails
Mario Carneiro (Jul 17 2018 at 01:31):
but I've reset the build a few times and it's still not working
Simon Hudon (Jul 17 2018 at 01:31):
This email would tell you its a race condition. Nothing you can't check yourself, that's true
Simon Hudon (Jul 17 2018 at 01:31):
The whole build or only stage two?
Simon Hudon (Jul 17 2018 at 01:33):
I'm starting to consider it might be worth letting the build restart in stage two when there's a race condition. With the cache, the build time sometimes gets much shorter than 45 minutes; it might just succeed
Mario Carneiro (Jul 17 2018 at 01:34):
Does stage 1 ever use the cache?
Mario Carneiro (Jul 17 2018 at 01:34):
If we give the old oleans to lean and let it sort them out we may gain a big improvement on many commits
Simon Hudon (Jul 17 2018 at 01:35):
It does. but that doesn't cause significant trouble. The cache contains code and binaries. Stage 1 just discards the code from the cache and ensure the right code from git is used.
Simon Hudon (Jul 17 2018 at 01:35):
That's actually what has been happening
Simon Hudon (Jul 17 2018 at 01:38):
Ok, I'll remove the guard. That will be easier to handle.
Simon Hudon (Jul 17 2018 at 01:38):
When stage 2 fails, be sure to restart the whole thing
Last updated: Dec 20 2023 at 11:08 UTC