Coq Call 2022 05 18 - coq/coq GitHub Wiki

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

Topics

• Dune test suite (Ali) https://github.com/coq/coq/pull/13364/

  • All tests have been ported to dune.
  • You can incrementally build all tests.
  • Will demonstrate how it will work with Makefile.dune and dune.

• META files / plugins and dune (Ali)

  • There are issues with META when .ml and .v files are in the same directory. The "good practice" version of a theories/ and src/ directory works completely fine however. This is obviously a dune "bug" but is a symptom of a larger issue or relying on META files.

• What is going on with LSP? The people want more info (Ali)