Coq Call 2021 03 10 - rocq-prover/rocq GitHub Wiki

• March 10th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• new bench machine instabilities
• debugger support in IDEs https://github.com/coq/coq/pull/13783
• cProfile, what to do? [c.f. https://github.com/coq/coq/pull/11791 ]
• dumping of warnings for documentation? [c.f. https://github.com/coq/coq/pull/11901 ]

Notes

• debugger support in IDEs https://github.com/coq/coq/pull/13783
  • Emilio notes that only small changes / clenaups are needed, so no big need for discussion, it could be more practical for him to push an extra commit on the branch.
• https://github.com/coq/coq/pull/13911 remove the unused (and probably encodable) :> coercion
• new bench machine instabilities https://github.com/coq/coq/pull/13907 Still to be investigated. New machines disabled for now.
• cProfile, what to do? [c.f. https://github.com/coq/coq/pull/11791 ] We should rather remove the remaining commented/outcommented code.
• dumping of warnings for documentation? [c.f. https://github.com/coq/coq/pull/11901 ] see comments in the pull request