BreakOut 2020 12 02 Ali

Question: Inconsistencies of output for Coq, silent builds

present: Ali Caglayan, Emilio Gallego

Ali (and Emilio) do love silent Dune builds, as they do ease reading CI logs, keeping developments warning free, etc...

However Coq scripts can usually output information, in particular commands that can do that are mainly Search, Check, Print, About, etc... This is done by using the Feedback mechanism.

Coq doesn't provide a good solution to controlling this output, for example for coqtop, they should displayed, but it is not clear that coqc would want this.

Moreover, it is not super clear yet what the Info/Notice levels mean in Coq these days, as despite several attempts for clean up [1,2] there still are inconsistencies.

We thus propose a reformulation of Coq's output levels and command line flags so that users can control Coq's output and have proper output build. Concretely:

• change the verbose command line flag to print_level
• set the defaults for print level as follows:
  • 0 = no info / notice printed [coqc default]
  • 1 = only notices are printed [coqc with compat flag]
  • 2 = info and notices [coqtop default]
  • 3 = debug

We will prepare a PR and submit for review / comments.

This should fix https://github.com/coq/coq/issues/12923

[1] introduction of msg_notice: https://github.com/coq/coq/commit/202903df7be549bea83735e9182814a7741e7f0d

[2] https://github.com/coq/coq/pull/10612

Question: HoTT build with Dune

• Ali: there are problems as of today with coq-hott + Dune, in particular -coqdep doesn't seems to get the -boot flag, and using (boot ...) doesn't fully work, likely needs some customization.

• Research more and patch Dune so it works, the build structure is clear these days so it shouldn't be a big deal.