Coq Call 2020 12 16

• December 16th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Regarding the coq-native Docker packaging: for the old Coq images < 8.13, coq-native is installed by default to preserve backward compatibility. Can we confim this setting before the upcoming release of docker-coq-action is announced?
• Can we agree on 1 version to extensively test so that we can recommend it to our users? (see also the coq-native + docker + ... mess)
• Quick question regarding the upcoming naming convention for 8.14 rc (notably w.r.t. the image coqorg/coq:latest)

From last week:

• CEP #49 and PR #11099 (instantiation of non-dependent implicit arguments by name or index): adopting the with model? generalizing it to all (including @foo-style) applied references? [HH: Unfortunately, I cannot be present today. An alternative is that the discussion be instead on the CEP page.]
• #12409: towards a typed-based or canonical structure based implementation of parametric rings? (possible digressions on how to improve recognition of the ring operations)
• Future of Parameter, Axiom, etc. Context outside sections. See #13416, #13068 and related discussion in #11390.

Notes

• No objection to keep the current setting of Docker-Coq < 8.13 (with the coq-native package to preserve backward compatibility); should do more benchmarks; and debugging to solve the current failure reproduced with graph-theory with coq 8.13 + coq-native + default Docker parameters…
• OCaml version to recommend to users: currently 4.07.1(+flambda), keeping 4.05.0 as compatible version for the moment as no incentive to make 4.07 as the minimal version, but one could directly bump to 4.10.0 later on (changing the "default" ocaml version at that moment)
• Regarding the +beta/+rc naming convention and the related workflow, open a CEP or a documentation PR?