Why can't we apply overlays in our CI and stop applying them when they are merged?
I never understood why it only applied to the PR being merged.
Do you have a way of auto-detecting whether the overlay was merged?
Or would that require additional PRs (possibly opened automatically) to remove the overlays once they are not needed? (If that's the latter, then that would be close to a proposal I made years ago but which was blocked.)
gh
CLI can detect if a PR is merged or not I believe. https://cli.github.com/manual/gh_pr_status
And when we detect the overlay has been merged we can emit a warning or do occasional batch clean ups.
We do this check when we are about to apply the overlay.
I'm sure there is a way to tell coqbot about it too.
Then coqbot can open a PR automatically cleaning up the overlays.
What coqbot could do would be to do a routine check every once in a while.
Every week would be sufficient IMO.
Ali Caglayan said:
gh
CLI can detect if a PR is merged or not I believe. https://cli.github.com/manual/gh_pr_status
This obviously doesn't work for Gitlab however.
I don't think this is a good idea, because overlays can become very quickly obsolete.
@Pierre-Marie Pédrot What do you mean?
What do you fear @Pierre-Marie Pédrot?
Especially when there are competing PRs with overlays on the same dev, this means essentially adding a one week-delay for any progress
How is that any different to the current situation?
Hum? What are you talking about?
An overlay only makes sense for a given PR.
Once you start applying overlays for several branches you have to consider the possibility of conflict.
and the job will fail right?
So like it does today then
Yes, for everybody.
If an overlay has not been merged it will fail for everybody, today.
Today the lock is not on our side, which is the problem.
But making the lock time-based with a week delay is probably worse than a few hours, or days at best, of missing downstream dev overlays.
We are not making anything time based?
We are suggesting that the CI for everybody tries to apply the overlay.
That means a merge, then?
And doesn't apply it once it is merged.
Pierre-Marie Pédrot said:
That means a merge, then?
Yes we will merge the PR into the CI sources.
Pierre-Marie Pédrot said:
But making the lock time-based with a week delay is probably worse than a few hours, or days at best, of missing downstream dev overlays.
You've completely misunderstood Ali's proposal.
What I fear is the criterion to detect that an overlay was merged.
Right, that is what gh
does. You can query GitHub directly about a PR.
And come up with a curl request for GL probably.
We can quite easily understand if a PR/MR has been merged and act accordingly.
What we were suggesting with the week clean up cycle is to remove the overlays we know have been merged.
Another solution: if the overlay does not apply cleanly on the base branch, you just test the base branch (instead of failing).
We still have to care for semantic conflict of overlays, though.
That's fine, we fail if overlays conflict.
That is strictly better than what we are doing today.
Which is fail everywhere when unmerged.
Indeed. I guess I'll to see it in action.
43 messages were moved here from #Coq devs & plugin devs > compcert / vst waiting for overlay by Ali Caglayan.
(this also assumes that downstream devs merge PR overlays correctly, which is not always the case. I've seen several people rebasing the commits locally and closing the PR.)
Yes that is a problem
Anyway just an idea how we might improve things rather than be at the whim of every CI entry.
Pierre-Marie Pédrot said:
(this also assumes that downstream devs merge PR overlays correctly, which is not always the case. I've seen several people rebasing the commits locally and closing the PR.)
That's fine if we do not use the gh
trick proposed by Ali but instead just check if the overlay merges cleanly with the base and otherwise skip it.
As for the auto-removal PR that coqbot could open, it could be very stupid: just remove overlays and let CI tell you if that works or not.
Last updated: May 31 2023 at 17:01 UTC