Stream: Coq devs & plugin devs

Topic: compcert / vst waiting for overlay

Gaëtan Gilbert (Nov 25 2022 at 09:04):

if you see a compcert or compcert-embedded-in-vst error like

File "./cfrontend/Ctypes.v", line 1905, characters 10-24:
Error: Cannot infer an instance of type "Type" for the variable F

it is because they are waiting for an overlay merge

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?

Ali Caglayan (Nov 25 2022 at 12:39):

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

Théo Zimmermann (Nov 25 2022 at 13:33):

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

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

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

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.

Ali Caglayan (Nov 25 2022 at 13:56):

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

Ali Caglayan (Nov 25 2022 at 13:57):

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

Ali Caglayan (Nov 25 2022 at 13:57):

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

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.

Ali Caglayan (Nov 25 2022 at 13:58):

Every week would be sufficient IMO.

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.

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.

Ali Caglayan (Nov 25 2022 at 14:00):

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

Théo Zimmermann (Nov 25 2022 at 14:00):

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

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

Ali Caglayan (Nov 25 2022 at 14:00):

How is that any different to the current situation?

Théo Zimmermann (Nov 25 2022 at 14:00):

Hum? What are you talking about?

Pierre-Marie Pédrot (Nov 25 2022 at 14:01):

An overlay only makes sense for a given PR.

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.

Ali Caglayan (Nov 25 2022 at 14:02):

and the job will fail right?

Ali Caglayan (Nov 25 2022 at 14:02):

So like it does today then

Pierre-Marie Pédrot (Nov 25 2022 at 14:02):

Yes, for everybody.

Ali Caglayan (Nov 25 2022 at 14:02):

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

Pierre-Marie Pédrot (Nov 25 2022 at 14:02):

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

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.

Ali Caglayan (Nov 25 2022 at 14:03):

We are not making anything time based?

Last updated: Feb 02 2023 at 13:03 UTC