Ali Caglayan (Nov 25 2022 at 14:03): Ali Caglayan (Nov 25 2022 at 14:03):We are suggesting that the CI for everybody tries to apply the overlay.
Pierre-Marie Pédrot (Nov 25 2022 at 14:03):That means a merge, then?
Ali Caglayan (Nov 25 2022 at 14:03):And doesn't apply it once it is merged.
Ali Caglayan (Nov 25 2022 at 14:04):Pierre-Marie Pédrot said:
That means a merge, then?
Yes we will merge the PR into the CI sources.
Théo Zimmermann (Nov 25 2022 at 14:04):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.
Pierre-Marie Pédrot (Nov 25 2022 at 14:04):What I fear is the criterion to detect that an overlay was merged.
Ali Caglayan (Nov 25 2022 at 14:05):Right, that is what gh does. You can query GitHub directly about a PR.
Ali Caglayan (Nov 25 2022 at 14:05):And come up with a curl request for GL probably.
Ali Caglayan (Nov 25 2022 at 14:05):We can quite easily understand if a PR/MR has been merged and act accordingly.
Ali Caglayan (Nov 25 2022 at 14:05):What we were suggesting with the week clean up cycle is to remove the overlays we know have been merged.
Théo Zimmermann (Nov 25 2022 at 14:06):Another solution: if the overlay does not apply cleanly on the base branch, you just test the base branch (instead of failing).
Pierre-Marie Pédrot (Nov 25 2022 at 14:06):We still have to care for semantic conflict of overlays, though.
Ali Caglayan (Nov 25 2022 at 14:06):That's fine, we fail if overlays conflict.
Ali Caglayan (Nov 25 2022 at 14:06):That is strictly better than what we are doing today.
Ali Caglayan (Nov 25 2022 at 14:06):Which is fail everywhere when unmerged.
Pierre-Marie Pédrot (Nov 25 2022 at 14:07):Indeed. I guess I'll to see it in action.
Notification Bot (Nov 25 2022 at 14:08):43 messages were moved here from #Coq devs & plugin devs > compcert / vst waiting for overlay by Ali Caglayan.
Pierre-Marie Pédrot (Nov 25 2022 at 14:09):(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.)
Ali Caglayan (Nov 25 2022 at 14:09):Yes that is a problem
Ali Caglayan (Nov 25 2022 at 14:10):Anyway just an idea how we might improve things rather than be at the whim of every CI entry.
Théo Zimmermann (Nov 25 2022 at 14:12):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.
Théo Zimmermann (Nov 25 2022 at 14:12):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: Feb 06 2023 at 00:03 UTC