Coq Call 2021 12 01

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

Topics

• Status/plan of/for Load plugins with findlib - #15220 (Enrico, needs to leave early)
• Testing output of extracted code (Ali)
  • https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Testing.20ocaml.20output.20in.20test-suite/near/263103163
  • https://github.com/coq/coq/pull/15098
• VSCode and Coq master (Matthieu)

Notes

• Status/plan of/for Load plugins with findlib - #15220 (Enrico, needs to leave early)

  • The solution requires patching dune, but dune is expected to use "sites" in the future. However internally the solutions are pretty similar apparently, at least w.r.t. depending on packages.

  • We should ask Francois Bobot about the situation in dune and if the direction we are taking is problematic. => Emilio will ask him to join a conversation on Zulip.

• Testing output of extracted code (Ali)

  • https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Testing.20ocaml.20output.20in.20test-suite/near/263103163
  • https://github.com/coq/coq/pull/15098

  => We would suggest to improve Extraction Test Compile to a Test Run command. => Patching the test-suite build could also be done. => Waiting for the dune PR

  Or simply put a rule in the test-suite/misc folder.

• VSCode and Coq master (Matthieu)

  => We need more care when changing the XML protocol.

  Long discussion about IDEs and Coq / where to focus our efforts.