The vst job in the CI usually take just over 60min. But my mangle names light PR is causing it to take 3 hours and time out. I'm not really sure what is going on. https://gitlab.com/coq/coq/-/jobs/1453578591
I think I've seen it timeout on some other PR too
VST uses rather intricate Ltac1 tactics and I would say it is quite imaginable that name mangling makes some of these tactics take forever rather than fail. I wouldn't expect that name mangling requires some fixes in VST.
But whats confusing is that no place in the repo contains the word "mangle" so could that really be the problem?
Can I somehow get coqbot to minimize the part that is taking too long? cc @Jason Gross
Figure out which tactic invocation takes too long. Then do
@coqbot resume CI minimize followed by a triple backtick on the next line followed by the contents of the file with a
Timeout <n> preceding whatever tactic invocation takes too long (make sure n is larger than the time it takes on master).
hmm I haven't been able to ask coqbot to minimize the file
veric/binop_lemmas5.v yet, but it seems to also have the same issue on master. That's good for me, but we probably need to workout what broke
veric/binop_lemmas5.v recently so that it doesn't work. I'm guessing due to the CI noise, something slipped in.
Here is the same problem with vst a weak ago
Weirdly a few runs in between are all fine
but then again with this 6 days ago
But then it seems to be persistently failing with a few exceptions
I'm not sure what can cause a job that takes 60min to randomly take over 3hrs and fail??
hmm I wouldn't of expected it to make such a difference. I wonder if we can try a generous timeout like 12hrs or something just to see if the job even finishes.
Last updated: May 28 2023 at 13:30 UTC