• January 5, 2022, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• 15392 (Format proof contexts in the debugger as they are outside). I'd like to know how to get a correct stack when stopped in the debugger. This draft PR is part of an investigation, not yet submitted for review. It appears the respondents didn't read my comments at all. (Jim)
• 15423 (Ltac2 internal debugger interface) (Jim)
• 12640 (PMP)

Notes

• [15392] The global proof state info is not available to Ltac but to the document manager only, so it shouldn't appear as expected initially by Jim.

• [15423] Ltac2 should first have a debugger for itself, respecting its semantics (PMP points at issues of breakage of semantics by Ltac1's debugger). Mixing Ltac1/Ltac2 is not necessarily possible or worthwhile, at least it should be postponed after there is a proper debugger for Ltac2. (JEF: mixing is definitely possible and not difficult. I'll explain how elsewhere.)

• [12640] Postponed to discussion with Guillaume. The crux of the disagreement seems to be using state ref -> unit vs explicit state passing.