Coq Call 2021 09 08 - rocq-prover/rocq GitHub Wiki

• September 8st 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Short announcement on the survey working group setup, list of alternative names (Matthieu and Théo)
• Stop renaming arguments in the with ... tactic construct (#13837, PMP)
• Review needed for #14644 Debugger part 3: display call stack and variable values, which incorporates #14252 [Debugger] Visual debugger in CoqIDE (Jim Fehrle)
• Creating a "Debugger preview" release through Coq platform to get feedback (Jim Fehrle)
• What to do about Remove the ssrsearch plugin and the ssr Search command (deprecated in 8.12)? (Jim Fehrle)
• Status of pyrolyse and do we need to buy new servers (Théo).
• Refactoring of cooking, towards supporting access to the discharged version of a constant from inside a section #14727 (Hugo)
• Wishes about primitive projections (Hugo)

Notes (by Matthieu)

• #13837, ok with a compatibility flag and to come back to no renaming by default.
• https://github.com/coq/coq/pull/13760 reconsider after Math-Comp meeting if we remove in 8.15.
• pyrolyse and new servers. No need for new ressources, we can keep pyrolise and Guillaume might be able to make it a runner
• Primitive projections: https://github.com/coq/coq/pull/14640. First remove the unfolded flag.