Coq Call 2022 05 11

• May 11th, 2022, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• CI versus unimath
• findlib version bump
• future of pyrolyse
• #15936 Package uint63.ml and friends separately (Li-yao @Lysxia)

Notes

• CI vs unimath. Frequently runs out of memory with parallel building. Shall we use Inria runners? Seems technically challenging. All the CI VMs were removed recently as we didn't use them (except the MacOS signing one), but Gaëtan thinks they might be more useful for longer runs and to manage/access them and stay secure.

• future of pyrolyse. Not used at the moment, warranty expired. Seems a waste to lose computing power, if we can put it back up again We could use the runners to get more memory and longer runs (for unimath or opam's ci). rocqableu can be put back a priori.

Conclusion: try the VMs first, just for special tagged jobs and document it. We can also ask the unimath devs to provide a target that runs in less than 1hour on our CI.

• testing coq-native with split packages is not done, especially in opam. There is a non-split package test in CI.

• The high memory consumption is due in part to the STM keeping more information than needed while coqc'ing. This might get better in the future.

• findlib: don't bump version, use try/with _ instead

• uint63.ml and friends: a separate package is agreed to be the way to go. We can have a separate opam package as well (and compiled without -rectypes).