Stream: Coq devs & plugin devs

Topic: CI - flocq3/flocq4

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2022 at 10:28):

Regardless of the solution, the RM would like to kindly remind the whole audience that we're 2 weeks away from the branching of the 8.16. It'd be nice if we had a green CI on master by then...

view this post on Zulip Michael Soegtrop (Apr 28 2022 at 11:28):

I can take care of the VST issue.

view this post on Zulip Michael Soegtrop (Apr 28 2022 at 11:33):

What is the final conclusion on having coq-flocq3 + flocq3 patched CompCert / VST in the main opam repo (not the flocq3 variants of interval and gappa)? Please use up vote (put it in main opam) or downvote (don't put it in main opam).

The VST issues are transitional (Flocq3/Flocq4 porting) and will eventually go away but might be not that easy to fix meanwhile, but I didn't have a deeper look. I will discuss it with Andrew.

@Guillaume Melquiond @Karl Palmskog

view this post on Zulip Karl Palmskog (Apr 28 2022 at 11:35):

my final conclusion is that the coq-flocq3 is welcome to be hosted in the Coq opam released repository, if someone submits it. But, we generally don't want to host packages against the will of the project maintainer. So if Guillaume says final "no" I think that's the end of it.

view this post on Zulip Karl Palmskog (Apr 28 2022 at 11:40):

on the other hand, if Guillaume isn't actively against it, I would treat a coq-flocq3 PR as just another package PR and merge it when CI passes

view this post on Zulip Michael Soegtrop (Apr 29 2022 at 06:37):

I am in discussions with Andrew on fixing the CI issues.

To conclude this discussion I would say we wait for pushing the packages upstream until someone says (s)he wants them. Since the packages are there and tested in Coq Platform this can be done very quickly.

view this post on Zulip Théo Zimmermann (Apr 29 2022 at 08:14):

Just some piece of advice: next time such Platform packaging discussions need to take place, hold them on a public channel (GitHub issues or Zulip for instance) instead of through private email. Having more people able to be involved in the full discussion would give more chances to take into account every aspect of the problem in the discussion.

Last updated: Feb 06 2023 at 18:03 UTC