with-rocq-wrap.sh / vscoqtop composed build support, what's the deal with OCAMLPATH ? (Matthieu, 10min)
Roles
Chairman: ?
Secretary: Théo Zimmermann
Audience: Enrico Tassi, Pierre Roux, Pierre-Marie Pédrot, Andres Erbsen, Matthieu Sozeau, Théo Zimmermann
Notes
Pierre, current Paramcoq maintainer, proposed to remove it from CI because it is broken (in the sense that some use cases that were not tested in its CI do not work anymore). Pierre will do a last release for Rocq 9.0. Pierre-Marie would like to keep it in CI and is volunteering to maintain it, but there won't be releases anymore and a warning will be added to the README for potential users.
Pierre asks whether CoqEAL should be introduced in the CI.
Pierre was the RM for 8.20 and did opam packages (and Nix packages). But it is not the RM duty to do them. The documentation should clarify whose responsibility it is, especially given that Docker images depend on opam, and people need them to upgrade their libraries. There are also the packages in the git repo which are also used for some use cases (including the Platform). Packaging team could include people from every distribution / packaging system (subteams) and provide recognition and awareness. Also, officially discharge the RM from this role. Théo and Matthieu will take care of creating this and announce it.
Matthieu will hack to make his composed build work. Pierre-Marie asked whether we could import back the official Coq/Rocq support in Dune as part of the Coq/Rocq repo. Apparently, there would be support for this in Dune now? Matthieu also just considers porting Dune to Rocq. Enrico suspects a missing dependency somewhere.