Coq Call 2021 11 17 - coq/coq GitHub Wiki

Topics

Notes

  • [exn] Add missing info: still unclear if the fix is to do Exninfo.reify everywhere, polluting the code. We can't do the reify inside the tclZERO in general. Debate among Pierre-Marie and Emilio about why we have a problem here. We should get a repro case and advice from the ocaml developers.

  • gappa's CI failing due to delay in merging an overlay. Should we change the CI rules so that this doesn't happen? Having a coq-ci branch + ability for Coq devs to merge there would help us. Accepting only developments with at least n+1 developers available would help as well. We should ask maintainers to give us at least the ability to merge overlays. Emilio suggests a working group on CI management to clarify the rules.

  • 8.16 RM - to be decided by January. Thinking about making this step more community-based by delineating the tasks.