Attendees : Reynald Affeldt, Yves Bertot, Cyril Cohen, Calosci Matteo, Pierre Roux, Quentin Vermande

2025 is tagged, not yet released. A few things did not make it in time (e.g. the lra PR). We should ask Kazuhiko for his plans about zify and algebra tactics. There is a printing issue since #1256.

There were several meetings to port HB to the new algebraic universes algorithm. There are a few issues in Rocq, Rocq-Elpi and HB. Most issues are silly mistakes, which is encouraging. The port is being done on the HB/pglobal branch.

Postponed

Reynald thinks that the time we spend writing a few more characters is negligible, the language should be designed as a whole and not an a per tactic basis. There was already a discussion on rw vs. rewrite in 2012, Enrico found out that rewrite was the most used tactic back then. Today its 28497 lines with rewrite against 11053 lines with apply (and 17639 vs. 9760 in MCA). There is an issue with porting scripts to ssreflect because legacy rewrite and ssreflect rewrite are not compatible. We could make ssreflect rewrite syntactically shorter or use rw and let rewrite be the legacy version. This way we could Require ssreflect in the Prelude. This should be discussed in a Rocq call. If changing names causes issues with the community, maybe we should try changing only rewrite.

The PR is ready. Merged.

We want to use micromega in MC. This is done in algebra tactics, which depends on MC and Stdlib. We would like to put everything in MC and stop depending on Stdlib. Modifications on the Stdlib part are currently blocked by its maintainer. We could fork the micromega repository, that we would need to maintain, and experiment.

Cyril