Attendees : Reynald Affeldt, Yves Bertot, Cyril Cohen, Assia Mahboubi, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Quentin Vermande

Probably 2.4.0, unless we release 2.5.0 soon. We need to review #1439's overlay. We need a release manager : Pierre volunteers and will see if Alessandro is available.

Could be useful. We do not control the number of subgoals. The syntax should be uniform with the dispatch. This is similar to bulk intros.

We would like to use several patterns to do several rewrites without writing the lemma name. Do we want a sequence or abstract over all patterns simultaneously? Trocq requires simultaneous pattern matching. It does not compose well with the other flags (e.g. ? and !). Maybe a calc tactic would answer the request. We do not have someone yet working on Trocq, there should be a meeting to discuss in what form we want to have someone do it. Yves is working with Thomas on a restricted version of calc, using anti-unification to find the place in the goal where things are happening.

We want a use tactic that does rewrite for now. Later on, use should subsume apply and rewrite (i.e. generalized rewriting). As of now, we use rewrite as apply when the goal is boolean because they are easier to chain.

rw would put us closer to Lean's syntax, which could be nice for Lean users. Would Lean users complain that Rocq's rw and Lean's rw do not have the same behavior? Probably not? It would not be exactly the same syntax either because of patterns and chaining. Furthermore, rewrite also exists (existed?) in Lean. Assia suggests not introducing use before we do have the generalized rewriting. Yves thinks that most of the learning curve is moving from stating the theorem instead of stating the resulting goal.

Should we have shorter names for other tactics?

rw would allow having ssreflect in the prelude. There might be an issue with keywords.

use might be hard to teach because its semantics may be unclear.

Let's do it and discuss other aliases later.

Theo is trying to have automatically generated docstrings (see LLM4Docq, please contribute, it need reviews). We need guidelines for the edition of docstrings for uniformity. A documentation sprint was discussed for the Rocq workshop, but there are already a lot of things to do so it might not happen. Yves participated in a collective documentation event, they worked slowly but were able to synchronize themselves. There should be both individual and collective reviews. Assia things we should work individually and collect the docstrings we are not sure about and discuss them during a meeting or on Zulip.

People do not look at headers because editors give you documentation when you hover over a lemma. People want to use AI based tools which are best at using natural language. We are lacking manpower to do the documentation.

Reynald thinks it is important to give information about naming conventions and design principles. We already have something but no one reads it. Maybe we can systematically add a link to the design principles page, or make the convention or any useful general information (e.g. how cancel lemmas are supposed to be used) available from the docstring. We could have better lemma search, using keywords. We could automatically give additional references such as references (books, articles, ...).

There should be a dedicated meeting about this. We can ask on Zulip if other people want to participate. Cyril suggests October 8th 10am.

We use group theory theorems on additive finite rings. Using aliases is very painful. What we can do is keep group theory separate from ring theory. We have multiplications in monoids, groups and rings. We could use the same multiplication in monoids and groups but then we can not define [something something in polymonials] as the freely generated [thing] of some monoid. Maybe we can have a copy of monoid below groups with 0 and rings. A reason to have monoids below finite groups is lifting operations, which produce monoids, not groups.

Let us postpone.

Cyril volunteers.