Coq Call 2021 12 01 - rocq-prover/rocq GitHub Wiki

Topics

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.