Coq Call 2021 05 05 - rocq-prover/rocq GitHub Wiki

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

Topics

• https://github.com/coq/coq/pull/14034

• Silent compilation modes (Emilio and Ali), see also:

  • https://github.com/coq/coq/wiki/BreakOut-2020-12-02-Ali
  • https://github.com/coq/coq/issues/12923
  • https://github.com/HoTT/HoTT/issues/1487

• coqdoc and docstrings, report for the #[doc=...] attribute and HB.about experiment

  • https://github.com/math-comp/hierarchy-builder/tree/master/tests/about.v
  • https://github.com/math-comp/hierarchy-builder/tree/master/tests/about.v.out

• coqdoc maintenance, plans for coqdoc 3 ? [Emilio]

Notes

• Silent compilation. Following https://github.com/coq/coq/pull/13202 (per component debug flags) also.

  • beware of PG changes
  • a priori not changes to coqtop, only coqc

• coqdoc and docstrings, report for the #[doc=...] attribute and HB.about experiment

  • https://github.com/math-comp/hierarchy-builder/tree/master/tests/about.v
  • https://github.com/math-comp/hierarchy-builder/tree/master/tests/about.v.out

  Require meta-data https://github.com/math-comp/math-comp/wiki/Minutes-May-05-2021

  coqdoc is not up to the task. A serAPI/Alectryon based or some form of meta-data database in .vos seems required to scale. Especially for metadata that is produced by commands like HB. Everyone seems happy with the proposed features, more discussion will be needed as to the syntax and the methodology: how to implement the DB, how to query it, should it be built-in in Coq or accessible through serAPI or some other protocol?

• Visual debugger in CoqIDE #14252 (Jim). Postponed to next week.