Zulip Chat Archive
Stream: mathlib4
Topic: infinite loop in CI: get cache
Thomas Murrills (Oct 23 2023 at 21:29):
In the mathlib PR #7686 for testing a lean PR, get cache seems to have entered an infinite loop:
Warning: lake-packages/std/Std/Tactic/Relation/Rfl.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Symm.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Rfl.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Symm.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Rfl.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Symm.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Rfl.lean not found. Skipping all files that depend on it
...
Last night it ran for 6+ hours; I re-ran it again today and the same thing happened. I'll try pushing another commit just to jostle it, but I just wanted to report that this was possible.
Mario Carneiro (Oct 23 2023 at 21:36):
Do you possibly have circular imports?
Mario Carneiro (Oct 23 2023 at 21:37):
cache doesn't have any import cycle detection so this seems like the most likely way to get it to loop
Thomas Murrills (Oct 23 2023 at 21:39):
It's possible—I don't really know what's on this branch, since it's mostly nightly-testing and other PR testing branches.
Thomas Murrills (Oct 23 2023 at 21:43):
Weirdly (to me), lake update seems to have fixed it :)
Mario Carneiro (Oct 23 2023 at 21:46):
fixed in #7876
Mario Carneiro (Oct 24 2023 at 00:25):
@Thomas Murrills Could you try merging #7876 into your branch and see if it fixes the issue here? I know that this fixes a bug but I don't know if it fixes the one reported here.
Thomas Murrills (Oct 24 2023 at 00:50):
I'll undo my lake update commit and try. :)
Thomas Murrills (Oct 24 2023 at 01:54):
Unfortunately, since then, I've rebased too much and I just can't get it into the failing state again (so that I can test the fix). But for what it's worth, here is one of the looping builds. The issue is that I've tried to fix the std4 branch that this depends on in the meantime, and I'm not sure exactly how. If there's some way to extract the std commit this depends on from the log files, though, maybe I can recreate it...
Mario Carneiro (Oct 24 2023 at 02:08):
The commit there is https://github.com/leanprover-community/mathlib4/tree/835c1b33b13c640a22a1b3e68bb2ec99d7b4616f, which contains https://github.com/thorimur/std4/tree/4298098844094010117d0db4ca3f38d86bacfb28 in the lake-manifest.json
Thomas Murrills (Oct 24 2023 at 02:14):
Ah great, thanks. I reset --hard to those commits; let's see what happens.
Thomas Murrills (Oct 24 2023 at 02:16):
Alright, we've got an infinite loop! workflow
Thomas Murrills (Oct 24 2023 at 02:16):
Thomas Murrills (Oct 24 2023 at 02:16):
Now I'll merge #7876.
Thomas Murrills (Oct 24 2023 at 02:20):
Great, it made it past the crucial stage! workflow
Last updated: Dec 20 2023 at 11:08 UTC