Coq Call 2022 01 05
- January 5, 2022, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
-
15392 (Format proof contexts in the debugger as they are outside). I'd like to know how to get a correct
stackwhen 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)
-
[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 -> unitvs explicit state passing.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.