Coq Call 2021 11 10 - coq/coq GitHub Wiki

Topics

  • https://github.com/coq/coq/pull/13861 use / in -print-mod-uid as dir separator on windows. (Gaëtan) (needs Emilio, Gaëtan and Enrico at the same time)

  • request update on https://github.com/coq/coq/pull/13760#issuecomment-924729283 (remove ssrsearch)

  • Coq Hackaton (Ali/Emilio)

  • https://twitter.com/natfriedman/status/1453394825269571591 Github merge trains

  • resurrecting coq_dune (Emilio)

    • coq_dune: simple coqdep to dune file generator
    • very easy to tweak, self-contained
    • first implementation: drawback, bootstrap process [will not be the case in Dune 3.0]
    • compared to dune: lacks composition, some more expressivity [dynamic deps for example, to be lifted in 3.0 too]
    • this is more robust than our current makefiles, and more future proof in general
    • remaining makefile for doc: should be able to remove in Dune 3.0

  • https://github.com/coq/coq/pull/13364 (port test suite to dune)

    • some open questions, but current implementation precise on deps
    • I think this is much faster on average, in most cases! [developing tests, developing Coq]
    • runs tests and build in parallel!
    • big question, avoid two copies of test-suite, migrating?
    • some differences in workflow, which one is better? We need to make a compromise, [and a promise not to whine]

  • Debugger (https://github.com/coq/coq/pull/14644): I made the changes @ejgallego requested a week ago and so informed him, but I haven't received any response. There's very little time left before the 8.15 deadline. Let's not miss it.

Notes