Coq Call 2024 12 03

• 2024-11-29, 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Notes

• inria gitlab storage quota (Gaëtan, 20min) Gaetan explains that the requirements for gitlab.inria.fr. Total space is 4 tera-bytes. 800 Gigabytes would be safe, probably also 700. Yves promises to send a request for exception with 800 Gigabytes. The contact is Didier Chassignol. There is a script on Zulip explaining how to reduce the usage: https://coq.zulipchat.com/user_uploads/23559/4uHTqnGW9Onx9ijhj5Je-kFO/myartifacts.py
• check absence of disagreements to removal of stdlib2 from CI #19820 (Pierre, 5min) stdlib 2 was started by M. Dénès and V. Laporte, trying to unify usage of typeclasses and canonical structure. Theo agrees that there is no need to keep it. Gaétan mentions the existence of work on a new prelude, developped for the Sort Polymorphism extension, currently developed here and explained in the article https://nantes-universite.hal.science/hal-04801739. The answer to Pierre's question is go ahead. The project could also be archived on https://github.com/rocq-archive
• logical path for new rocq-init package (c.f. #19530) ) (Pierre, 20min) Emilio noticed that dune will fail to use the new organisation of stdlib properly, there is a need to make sure that that what remains in the coq repo has a different name. the name that is suggested is Corelib. This is approved. There is a wrapper in stdlib so that final users do not need to worry about it. The team plans to maintain this wrapper in the long term. This Corelib will be provided as an independent opam package (for users who do not want to use stdlib, like unimath). The current coq-core will become rocq-runtime and the new package for Corelib will be rocq-core and there is a package rocq-prover that contains these two plus the stdlib. coq packages will remain as compatibility for some time.
• logo proposal (Philippe, 5-10min) Philippe proposes a logo with a guitar theme. The discussion then goes around ways to make this logo available to the wider community, including license (it is suggested to look at the creative common licenses https://creativecommons.org/). It is suggested to make the logo available on the discourse forum https://coq.discourse.group/.
• opam CI broken (Karl Palmskog, 5min) It is currently impossible to work check opam packages using CI. There are too few runners, inria gitlab is not a friendly environment for opam-CI. Karl has the problem that there is a desynchronization, which was caused by some recent force-push by Guillaume. We can add some of the runners we use for coq-CI. We have a gold sponsorship at gitlab.com, but we do not use it. There is a lack of caching on Inria's gitlab. Pierre is suggesting that we use docker-image, but this is not straight-forward because we are testing opam files, which do not rely on docker. It seems the decision has been taken to move CI back to gitlab.com, thanks to the gold membership that we currently have.
• issue #11479 (Yves) This issue has been mentioned in the recent Coq Workshop (Sept. 2024, in Tbilisi). It is agreed that provided a compilation mode that recovers from proof failures with a possibility to gather statistics about the number of failing proof instead of a compilation mode that stops at the first error is of general interest. Several members of the audience suggest to look at what fcc, the Coq compiler provided in fleche can provide in this respect. Emilio states that he hass a branch of fleche that almost provides the required functionality. Yves will discuss the matter with Emilio.
  • Emilio adds: Indeed fcc / coq-lsp already skip broken proofs by default. People have already written some plugins for fcc to summarize errors. I will post an example in the issue. I think that should cover Hendrik's use case. Note that there are several interpretations of what a "broken proof" is. Regarding the branch, it is only needed if you want to do as .vos and skip proofs first, then check them later. IMHO that should not be needed for Hendrik's use case.

Roles

• Chairman: Matthieu Sozeau
• Secretary: Yves Bertot
• Audience: Andres Erbsen, Karl Palmskog, Gaëtan Gilbert, Enrico Tassi, Théo Zimmermann, Pierre Roux, Philippe, Emilio Gallego Arias,