Cyril Cohen (Jun 08 2020 at 15:15): 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)?
Enrico Tassi (Jun 08 2020 at 20:21):I think you should post this on coq dev as well
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?
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
Enrico Tassi (Jun 08 2020 at 20:28):Any recent merge that could affect 4ct?
Enrico Tassi (Jun 08 2020 at 20:34):Actually, not many changes recently: https://github.com/coq/coq/pulls?q=is%3Apr+is%3Aclosed
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
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
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..
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)
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)
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: Sep 09 2024 at 05:02 UTC