Stream: Coq devs & plugin devs

Topic: Why is vst taking so long


view this post on Zulip Ali Caglayan (Jul 26 2021 at 23:15):

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

view this post on Zulip Gaëtan Gilbert (Jul 27 2021 at 07:44):

I think I've seen it timeout on some other PR too

view this post on Zulip Michael Soegtrop (Jul 27 2021 at 08:41):

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.

view this post on Zulip Ali Caglayan (Jul 27 2021 at 09:17):

But whats confusing is that no place in the repo contains the word "mangle" so could that really be the problem?

view this post on Zulip Ali Caglayan (Jul 27 2021 at 09:18):

Can I somehow get coqbot to minimize the part that is taking too long? cc @Jason Gross

view this post on Zulip Jason Gross (Jul 27 2021 at 14:28):

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).

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:04):

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.

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:08):

Here is the same problem with vst a weak ago

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:08):

https://gitlab.com/coq/coq/-/pipelines?page=2&scope=all&ref=master#:~:text=exe%20to%20.gitignore-,library%3Aci-vst,-library%3Aci-color

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:09):

Weirdly a few runs in between are all fine

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:09):

but then again with this 6 days ago

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:09):

https://gitlab.com/coq/coq/-/pipelines?page=2&scope=all&ref=master#:~:text=part%20of%20%2314505-,library%3Aci-vst,-library%3Aci-color

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:10):

But then it seems to be persistently failing with a few exceptions

view this post on Zulip Ali Caglayan (Jul 28 2021 at 09:11):

I'm not sure what can cause a job that takes 60min to randomly take over 3hrs and fail??

view this post on Zulip Gaëtan Gilbert (Jul 28 2021 at 09:19):

different machines?

view this post on Zulip Ali Caglayan (Jul 29 2021 at 11:27):

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: Oct 21 2021 at 21:03 UTC