Coq Call 2021 12 01 - coq/coq GitHub Wiki
- 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)
- 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 aTest Run
command. => Patching the test-suite build could also be done. => Waiting for the dune PROr 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.