Coq Call 2020 09 23

• September 23rd 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

[Emilio: I may trouble attending this week call, see one comment below]

• New zarith dependency. The latest version, released just a week ago and not in any version of Debian is required since lia depends on it (because of bugs of previous versions). Was the transition done too soon? Should we revert it for now? See https://github.com/coq/coq/pull/13049.

  • Emilio: IMHO the dep is fine given the timeline for 8.13; note that in this case people packaging Coq can easily also update the zarith package, updating OCaml is way way harder in Debian so we are more conservative.

• Have a better integration of the bench system for the opam packages on https://coq-bench.github.io/ See the issue https://github.com/coq/coq/issues/10418 In particular we can talk about how to open access to / share the server infrastructure, which new package tests to develop, how to communicate the test results.

Notes

• Emilio's option is to update zarith at the same time as Coq 8.13 is introduced. The new package is already there so that e.g. projects on CI don't break.

• Integration of coq.io with coq-platform and the coqbot seems very interesting (maybe even coq-community). Karl and Guillaume both maintain the bench. Now integrated with zulipchat. We don't yet know how to open the access and share the server infrastructure (Maxime investigates at Inria, at least the website part). The actual benchmarking can be shared with the hopefully upcoming infrastructure for performance tests.