Coq Call 2020 09 09

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

Topics

• Update to the Coq Installation section from the wiki, especially Linux and VSCoq (Arthur) https://github.com/coq/coq/wiki
• Instructions for configuring NIX build to not recompile Coq (Arthur)
• Status of a -no-qed-check and -no-universe-check flags for coq/coqide (Arthur) and also add support for -o filename when producing .vo* files.
• ETA 8.12.1 ? (ssr is unusable in 8.12.0 + needs from SF)

Notes

• Install instruction discrepancy:

  • INSTALL.md should point to the wiki page.
  • Arthur will do a pass on the wiki page.

  Probably pointing to known issues related to compilation as well!

• NIX issues: noone available to respond -> issue

• -no-qed-check possible according to PMP but not exactly the same as replacing Qed by Admitted. A PR by Gaëtan might solve this. Debate about using typing_flags for this purpose: it might be better to do it at a higher level, e.g. a declare_constant_as_axiom in Declare.

  -no-universe-check is -type-in-type (and is dangerous for maintainability).

• Adding an -o option? No opposition to that.

• 8.12.1 ETA: planning a release for end of next week (18th sept).

• PMP point about OCaml version 4.05 and 4.06 being incompatible with newer gcc (on Debian Unstable) -> add to known issues.