status of 2.4.0 release

the opam works, discovering that the algebra tactics did not work was delayed because it is not enough to compile the code. The test suite should be run in CI. A new nix derivation is needed. Nix derivations have a builtin test phase. Pierre prefers to not delay his work until a new derivation is produced to make sure there is a test package. Cyril proposes to merge a quick fix and to find a uniform solution to be worked on during the Rocq'n share meeting. The merge is triggered in the meeting.

Graph theory

it takes some time to port it. For now, Pierre removes it from the CI. There is a problem with maintenance. Cyril will discuss the issue with Damien.

There is then a discussion about attendance at the Rocq'n share meeting.

PR triaging

One of Arthur Azevedo de Amorim's pull-request has been approved.

there is a discussion about the unreliabiity of continuous integration solutions. We are currently using one CI based on gitlab and one CI based on nix.

It is agreed to add infotheo to CI again (it was disabled because of a problem with algebra-tactics).

Lemmas from math-comp analysis. Please find a reviewer. Cyril does not know whether he is a co-author so he hesitates reviewing. Pierre states the rule of thumb that if cyril does not remember being an author he can probably review the PR.

The conjC conj_op PR#1404 requires an extra explanation. The PR has been reviewed by Kazuhiko. According to Cyril, this code should be short lived because HB should cope for this kind of problem in the future. (PR#535 in HB should be the long-term fix). The short-term fix is not ready because a mistake was spotted.

#1403 is still a draft because some extension on orders should be included. We come to the conclusion that what is already present is useful and there should be a second PR. There are questions about naming policy, especially have by comparison with transitivity.

#1398 K. Sakaguchi has more time now, there will be more progress

#1338 There is some discussion about this PR that is really important for future development.

Choosing the chair for the next meeting: Pierre Roux volunteers