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?
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
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?)
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?
I don't know what the current GitLab.com behavior is, but at some point it was keeping logs indefinitely.
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).
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.
From then, we could try to download the logs we are interested in.
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.
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)
Wow, thanks a lot.
Gaëtan Gilbert said:
it's generally possible this way:
step1.png
step2.pngyou 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?
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?
No, that would really be a feature request for GitHub then.
we could put a neutral status "previous pipelines" linking to the pipelines?ref=pr-XXXX
no?
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: Oct 13 2024 at 01:02 UTC