Coq Call 2023 10 10
- October 10th 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
- Roadmap update (Théo, 10-15 minutes)
- Website license and website migration to GitHub Pages (Théo, 15-20 minutes)
- Chairman: Nicolas Tabareau
- Secretary: Yves Bertot
There is consensus on the fact that more option of guards should be given and their use should be recorded, thus the options that are considered unsafe could still be provided to users, but with warnings or caveats. Among the 4 options, only the second one (uniform parameters) seems ripe enough to be included in the roadmap, the others should be pushed back to the section for more exploratory work. {For the elements that are ripe enough, a proof of correctness should be provided. In particular, proofs in MetaCoq are mentioned, but this might be overkill (the entry cost seems too high).
Still a proof in MetaCoq of the simplest guard would make it possible to achieve a nice threshold in the MetaCoq proof of correctness of Coq.
The difficulty on this point of guards is to find a core specialists that feels confident enough to review improvements. The one point on uniform parameters stands out as one where more people are confident of the potential correctness.
More feedback from users should be gathered. It is too early for implementatio (and for integration in the roadmap)
This one is at risk for lack of resources
Hugo Herbelin and Pierre Roux agree to collaborate on this topic
There was recent progress in the form of pull request by Yannick Forster, but it is still incomplete. However, the objective "replace extraction towards OCaml" should rather be presented as "provide an alternative". There is a question on whether all possible alternative of extraction should be provided by on the Coq Platform, to encourage their usage.
This topic seems too young. The first stage should be have a separate CEP for this matter.
Nicolas Tabareau agrees to take this topic in earnest, add it to the roadmap, and pick up the pieces of communication with Inria support on the topic. Yves Bertot proposes to participate in the effort.
Hugo asks whether there is any effort from the development team to bring support to Michael Soegtrop on this important contribution. The answer is that Romain Tetley is now in direct collaboration with Michael to prepare the next release of the platform, including with respect to finding enough machines to prepare the packages for various operating systems.
The new host for the Coq web site, githubpages, does not provide all the functionalities that were provided by the previous host. Some of contributors on zulip can propose a solution based on Javascript, but they refuse to contribute any code if the pages have no license.
It is agreed in this meeting to set the license to CC0
An alternative solution would be to rather move to gitlabpages, which provides my capabilities for redirections. Guillaume Melquiond declares his intention to make an experiment in that direction, but not before two weeks.
Still, we aim to ask the person who has a solution based on javascript to include it, as soon as the license issue is resolved.
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.