Coq Call 2023 11 07

• November 7th 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Coq Meeting in december or january (https://framadate.org/NouP2cvyjtpa1u7a) (Matthieu, 5 min)
• Support for Ltac2 and vsCoq2 in the Ltac debugger; general comments on the review process (Jim, 30 min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Matthieu Sozeau

Notes

• Next Coq Working Group in Nantes on December 18th (10am - 5pm).
• Support for Ltac2 in Ltac debugger: Jim presented a combination of both Ltac's and Ltac2's visual debuggers in a single system and a few UI improvements on CoqIDE, some loosely related, some coupled like the diffing feature, we did not see the code though. Debate on the review process for these PRs: Jim feels he did not get timely feedback on his changes, whereas maintainers Emilio and Pierre-Marie asked repeatedly for changes in the design and implementation of the feature (e.g. stopping the use of global state and ad-hoc communication protocols), which have not been followed yet. Moving to DAP (as will be required for VSCode integration) and figuring out how to (re-)implement the feature cleanly are still prerequisites for integration of this feature.

(Jim's comment) Everything I demonstrated was either new functionality or display functionality that didn't previously work while in the debugger. I wouldn't say "loosely related". The ability to pick which goal to fully show in the context provides information that otherwise can't be seen in the debugger, but it can also be used outside the debugger.

The initial version of the debugger was merged 2 years ago, which used some global variables. Apparently they later changed their mind on using any global variables this but never communicated this clearly. Emilio objected to adding a single additional global in an unmerged PR from about 21 months ago but was totally unwilling to explain or discuss that. Stonewalling. Use of DAP is prospective; I don't recall a serious suggestion that the CoqIDE version should use DAP.

To be continued:

• Implementation plans for namespaces, CEP #25 (HH, 5-10 min, if Enrico and/or Cyril are there).

Postponed:

• Stabilization of user syntax for library file deprecation/warning (PR #18193, currently: command Library Attributes #[...] + new attribute information="...") (Hugo, 5-10 min)
• Reflection on CEP #73, useful for small inversion and for the parametricity plugins (HH, 5-10 min)