release FCF through coq-released and Coq Platform?

[andrew-appel]

Since FCF is useful and seems to have at least one maintainer (for example, @andres-erbsen), I suggest that FCF should be released via opam in the coq-released archive, and then added to the Coq Platform.

• To add this to coq-released, you make a fork of https://github.com/coq/opam and then submit a pull request.
• Once that is done and accepted, you can nominate FCF for inclusion in the Coq Platform. That is a set of libraries that, in each release every 6-12 months, are all guaranteed compatible with each other (to avoid "dependency hell"). Then the Coq Platform board decides whether FCF satisfies the criteria.

Does anyone else think this is a good idea, and is anybody willing to be a "maintainer" for the purposes of this process? If so, there's at least one member of the Coq Platform board who will advocate for it.

[adampetcher]

I'm not opposed to the idea, but I don't know if there is enough justification, as required by the inclusion criteria. I'm not even aware if anyone has used it in the last 5 years other than me. @andrew-appel are you aware of significant uses of FCF, or did you have some other justification in mind?

[andrew-appel]

It seems to be used by (1) VST testcases and (2) @andres-erbsen, two external users independent of the FCF developer and of each other. That might be enough for the Coq Platform, and it's certainly enough to justify inclusion in coq-released.

[adampetcher]

Thanks for the info! I'm still not opposed to the idea, but I'm not willing to be the maintainer. So I think we will need a volunteer for this part.