Coq Call 2021 11 10

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

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

• https://github.com/coq/coq/pull/13861 fixing coq_config would be more tricky, let's go with this solution for now.

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

• Hackaton: Zulip thread on the subject.