Coq Call 2021 09 08
- September 8st 2021, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- 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)
- #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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.