Stream: Coq devs & plugin devs

Topic: V8.18.0 tag


view this post on Zulip Enrico Tassi (Sep 07 2023 at 15:31):

I think the branch v8.18 can be tagged. I did not do it tobay because I run out of time.
If a CI expert could validate my assessment of the failure here https://github.com/coq/coq/pull/18016 it would help.
I've never seen this error before (artifact too large), but seems really unrelated (the PR change only the version number, also in the .vo files). Are we so close to the limit that irritating gzip can cause the this failures?

view this post on Zulip Gaëtan Gilbert (Sep 07 2023 at 15:44):

could be anything
The fiat crypto devs don't seem to be interested in providing a reasonably sized CI target so I'm waiting until they consistently exceed the timeout then we can remove the fiat-crypto job from regular testing

view this post on Zulip Jason Gross (Sep 08 2023 at 03:48):

How hard would it be to scrape github issues and CI logs and find out where fiat-crypto build failures occurred? I'm down to supply some more reasonably sized CI targets, as long as the files that we're cutting out haven't caught changes in Coq that were not caught by any earlier file / other development. (@Théo Zimmermann do you know an easy way to do this scraping?)

view this post on Zulip Pierre Roux (Sep 08 2023 at 06:19):

Are the CI artifacts even preserved for more than a few months? If not, then there is probably not much to recover. Maybe your best bet would be to analyze the overlays produced along Coq PRs then?

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 07:40):

I don't know what the current GitLab.com behavior is, but at some point it was keeping logs indefinitely.

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 07:41):

In any case, yes, I do want to perform such empirical analysis of past CI results / logs, also to try to figure out how performant external projects have been in catching compatibility issues (to decide which projects to remove if we need to cut some out).

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 07:42):

The strategy I considered so far is to start from the GitLab.com API. Its GraphQL API has been much extended and should allow finding relatively quickly a list of all failing jobs from the entire CI history.

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 07:42):

From then, we could try to download the logs we are interested in.

view this post on Zulip Hugo Herbelin (Sep 08 2023 at 08:00):

Théo Zimmermann said:

I don't know what the current GitLab.com behavior is, but at some point it was keeping logs indefinitely.

Does that mean that we should be able to recover the former CIs made on any PR? Sometimes I restart a CI just because I lost the link to the former ones, e.g. after correcting a lint problem or so.

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 08:08):

it's generally possible this way:
step1.png
step2.png

you can also go to eg https://gitlab.inria.fr/coq/coq/-/pipelines?page=1&scope=all&ref=pr-17732 (the pr-XXXXX at the end picks the PR) (gitlab.com for older runs)

view this post on Zulip Hugo Herbelin (Sep 08 2023 at 08:45):

Wow, thanks a lot.

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 09:01):

Gaëtan Gilbert said:

it's generally possible this way:
step1.png
step2.png

you can also go to eg https://gitlab.inria.fr/coq/coq/-/pipelines?page=1&scope=all&ref=pr-17732 (the pr-XXXXX at the end picks the PR) (gitlab.com for older runs)

Maybe we should add this trick to the contributing guide?

view this post on Zulip Hugo Herbelin (Sep 08 2023 at 09:03):

Maybe we should add this trick to the contributing guide?

Would adding a link on the PR page to the list of all runs made on the PR easy to do?

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 09:33):

No, that would really be a feature request for GitHub then.

view this post on Zulip Gaëtan Gilbert (Sep 08 2023 at 09:40):

we could put a neutral status "previous pipelines" linking to the pipelines?ref=pr-XXXX no?

view this post on Zulip Théo Zimmermann (Sep 08 2023 at 09:54):

Hum yeah, if it's just about adding this link, we could even add it in the GitHub Check summary for the current pipeline.


Last updated: Jun 17 2024 at 22:01 UTC