Stream: Coq devs & plugin devs

Topic: why not use overlays everywhere (compcert / vst waiting f...


view this post on Zulip Ali Caglayan (Nov 25 2022 at 12:39):

Why can't we apply overlays in our CI and stop applying them when they are merged?

view this post on Zulip Ali Caglayan (Nov 25 2022 at 12:39):

I never understood why it only applied to the PR being merged.

view this post on Zulip Théo Zimmermann (Nov 25 2022 at 13:33):

Do you have a way of auto-detecting whether the overlay was merged?

view this post on Zulip Théo Zimmermann (Nov 25 2022 at 13:34):

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.)

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:53):

gh CLI can detect if a PR is merged or not I believe. https://cli.github.com/manual/gh_pr_status

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:54):

And when we detect the overlay has been merged we can emit a warning or do occasional batch clean ups.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:56):

We do this check when we are about to apply the overlay.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:57):

I'm sure there is a way to tell coqbot about it too.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:57):

Then coqbot can open a PR automatically cleaning up the overlays.

view this post on Zulip Théo Zimmermann (Nov 25 2022 at 13:58):

What coqbot could do would be to do a routine check every once in a while.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:58):

Every week would be sufficient IMO.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 13:59):

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.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 13:59):

I don't think this is a good idea, because overlays can become very quickly obsolete.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:00):

@Pierre-Marie Pédrot What do you mean?

view this post on Zulip Théo Zimmermann (Nov 25 2022 at 14:00):

What do you fear @Pierre-Marie Pédrot?

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:00):

Especially when there are competing PRs with overlays on the same dev, this means essentially adding a one week-delay for any progress

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:00):

How is that any different to the current situation?

view this post on Zulip Théo Zimmermann (Nov 25 2022 at 14:00):

Hum? What are you talking about?

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:01):

An overlay only makes sense for a given PR.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:01):

Once you start applying overlays for several branches you have to consider the possibility of conflict.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:02):

and the job will fail right?

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:02):

So like it does today then

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:02):

Yes, for everybody.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:02):

If an overlay has not been merged it will fail for everybody, today.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:02):

Today the lock is not on our side, which is the problem.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:03):

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.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:03):

We are not making anything time based?

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:03):

We are suggesting that the CI for everybody tries to apply the overlay.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:03):

That means a merge, then?

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:03):

And doesn't apply it once it is merged.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:04):

What I fear is the criterion to detect that an overlay was merged.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:05):

Right, that is what gh does. You can query GitHub directly about a PR.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:05):

And come up with a curl request for GL probably.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:05):

We can quite easily understand if a PR/MR has been merged and act accordingly.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:06):

We still have to care for semantic conflict of overlays, though.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:06):

That's fine, we fail if overlays conflict.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:06):

That is strictly better than what we are doing today.

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:06):

Which is fail everywhere when unmerged.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2022 at 14:07):

Indeed. I guess I'll to see it in action.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Ali Caglayan (Nov 25 2022 at 14:09):

Yes that is a problem

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 04:02 UTC