Skip to content

Coq Call 2022 05 18

Ali Caglayan edited this page May 18, 2022 · 5 revisions

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)

Clone this wiki locally