Coq Call 2022 04 20 - rocq-prover/rocq GitHub Wiki

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

Topics

• 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)