Coq Call 2022 04 20
- April 20, 2022, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- Should coqc require a correct OCAMLPATH setting? (https://github.com/coq/coq/issues/15663 - Jason (and Enrico))
Postponed from last week:
- CEP #64 Requirements for supporting Ltac2 debugging with a high-level outline of changes For discussion (Jim)
- #15737 At breakpoints, format goals the same way as CoqIDE usually does; redisplay the goal when the user changes display options Can we make progress on the review? (No progress for 3 weeks) (Jim)
- #15861 CoqIDE highlighting doesn't reset properly on edit and #15882 CoqIDE processed state isn't updated upon pasting to the buffer - regression in 8.15.1 from #15772 Correctly prevent editable status of text when CoqIDE is busy, regression in commit "Clean up the interaction logic of the CoqIDE buffer manipulation." @ppedrot, do you intend to address this? (Jim)
- #15912 Fix code to display goal in both top script and current script buffers 2-line change awaiting review, candidate for 8.15.2 (Jim)
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq 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.