Coq Call 2022 04 27

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

Topics

• Postponed topics first
• #15936 Package uint63.ml and friends separately (Li-yao @Lysxia)
• https://github.com/coq/coq/pull/15693 Reversible coercions needs pretyper reviewer (Ali)

Postponed from two weeks ago:

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

Postponed from last week

• Should coqc require a correct OCAMLPATH setting? (https://github.com/coq/coq/issues/15663 - Jason (and Enrico))

Notes

• Jim on Ltac2 debugging. PMP opposes to the way breakpoints are tied to absolute locations, which should be resolved before going further with implementing the Ltac2 + Ltac debugging. Discussion of the ways we can test CoqIDE using fake_ide. Difficulties to submit bugs about coqide so Jim can reproduce them and fix them.