Stream: Coq devs & plugin devs

Topic: four-color takes more time on coq-dev


view this post on Zulip Cyril Cohen (Jun 08 2020 at 15:15):

Dear all, since yesterday, we are starting to have timeouts on fourcolor for coq-dev (the compilation time used to be around 50 min, but the last two times I tried it went up to a timeout or 57min... @Erik Martin-Dorel could your last commit have introduced this? Is there a way to get the CPU time (rather than the user time)?

view this post on Zulip Enrico Tassi (Jun 08 2020 at 20:21):

I think you should post this on coq dev as well

view this post on Zulip Cyril Cohen (Jun 08 2020 at 20:24):

Enrico Tassi said:

I think you should post this on coq dev as well

maybe I should move the topic to coq dev?

view this post on Zulip Notification Bot (Jun 08 2020 at 20:25):

This topic was moved here from #math-comp devs > four-color takes more time on coq-dev by Cyril Cohen

view this post on Zulip Enrico Tassi (Jun 08 2020 at 20:28):

Any recent merge that could affect 4ct?

view this post on Zulip Enrico Tassi (Jun 08 2020 at 20:34):

Actually, not many changes recently: https://github.com/coq/coq/pulls?q=is%3Apr+is%3Aclosed

view this post on Zulip Jason Gross (Jun 08 2020 at 22:04):

Is fourcolor on the bench? If you have a commit on coq-dev where it was good, and a commit where it was bad, I can try to manually bisect on the bench

view this post on Zulip Erik Martin-Dorel (Jun 08 2020 at 22:08):

@Cyril Cohen Don't you think there is an issue with GitLab CI itself? as my PR that you have merged recently is orthogonal AFAICT,
and moreover now that I look on the latest pipeline in https://gitlab.com/math-comp/math-comp/-/pipelines → it seems jobs fail with a failure in a earlier stage now, even math-comp master on coq-8.10 itself timeouts:
https://gitlab.com/math-comp/math-comp/-/jobs/586450031

view this post on Zulip Erik Martin-Dorel (Jun 08 2020 at 22:23):

Anyway, we might want to increase a bit the math-comp timeout setting in GitLab CI? given that 50' in average for the 4ct jobs (before yesterday's unexpected issue) is really near the limit..

view this post on Zulip Cyril Cohen (Jun 08 2020 at 23:27):

Erik Martin-Dorel said:

Anyway, we might want to increase a bit the math-comp timeout setting in GitLab CI? given that 50' in average for the 4ct jobs (before yesterday's unexpected issue) is really near the limit..

Sure, will do... but it worries me that the timing is consitently higher than for coq-8.10 for example (around +10min whatever the case)

view this post on Zulip Enrico Tassi (Jun 09 2020 at 11:34):

It is on the bench, we should use that to identify the commit. @Cyril Cohen when did you start noticing the slowdown? (bisecting from 8.10 is possible, but having a closer commit could speed things up)

view this post on Zulip Cyril Cohen (Jun 10 2020 at 15:23):

I started noticing when it timed-out on Monday... and then I tried to scroll up the jobs, but I have not consistent nor convenient way of analysing that...


Last updated: Oct 16 2021 at 03:02 UTC