I would like the LLM discussion to also address projects under the Rocq umbrella beyond Rocq itself (bot, Rocq Platform, VsRocq, etc.) (Théo Zimmermann, will probably require additional time)
Moving from OCaml 4.14 -> 5.4 or 5.5 (PMP, 10min).
Support for OCaml 4.14 is discontinued, we start recommending 5.4 (+ flambda when not using native) starting with Rocq 9.3.0. (5.4 is the first version without performance regressions, and currently the last one with a compatible ocamlfind.)
Places to update: INSTALL.md, release notes, website (opam instructions).
Assia and Guillaume will re-test native compute on macOS.
Discussion on genAI use:
Starting point is the Debian policy that a lot of people think is reasonable. Discussion also of the Codeberg policy.
Discussion on the consequences of AI use in terms of (un)learning expertise and time (boost in productivity can be a double-sword edge).
Rocq is a very complex software with a lot of embedded knowledge that we should not lose from our heads.
The case of the satellite project is different (with fewer people who maintain them in particular). Use of AI so far has been limited to very specific projects, or for code review and code audit.
No one express strong opposition to AI use, but allowing AI-generated PRs means spending reviewers' time and risk burning energy for nothing.
What is the goal of the discussion: to produce a resolution/AI-policy of the Rocq project. Should it be restricted to the contributions that we receive and the impact it has on maintainers' time? Or should it also warn about the AI usage that can be done by the maintainers themselves and the associated risk of losing competences?
PRs must stay human-readable and the walls of text in comments are examples of things that make code only readable by LLMs.
Goal is to produce an AI-policy (short) by next week.
Discussion of copyright and environmental implications toward the end. Environmental issues should at least get a mention in the policy (e.g., can discourage the rush for increased productivity).