Minutes November 22 2023

Participants: Cyril, Enrico, Kazuhiko, Pierre, Quentin and Yves.

Merging #1046? (cleanup of phantom types)

• Was waiting 8.18, since the display is horrible on previous versions.
• Some commits should be removed, eg {poly R} -> poly R in code and doc, since the notations are sometimes nicer even if not needed anymore (no phantoms).

#986 (Generalize ler_sqrt)

• MC classical is broken, to be investigated
• ssrnum uses french conventions about positive/strictly-positive, we should fix this in another PR
  • analysis already uses it

#1127: Incoherence of the implicit status of lemmas (everywhere but particularly in ssralg)

• Should we Set Maximal Implicit Insertion?
  • Pierre, Cyril and Enrico agrees
• let's try and see if there is a lot of breakage or not

recurring topic from the previous meeting

there are several "mathcomp complements" files and directories in the mathcomp hierarchy, e.g.:

Coq-Combi: https://github.com/math-comp/Coq-Combi/tree/master/theories/SSRcomplements
cad: https://github.com/math-comp/cad/blob/master/extra_ssr.v
newtonsums: https://github.com/math-comp/newtonsums/blob/master/auxresults.v
multinomials: https://github.com/math-comp/multinomials/blob/master/src/ssrcomplements.v
CoqEAL: https://github.com/coq-community/coqeal/blob/master/theory/ssrcomplements.v

it would be nice to collect useful things from them but how to do that efficiently?

• Cyril proposes to make sprints for that, after the finmap one (i.e. February)

follow-up from the previous meeting

Inria application that would include the topic of putting together "mathcomp extra files"
and about general maintenance of MathComp

• to the next meeting, Cyrils has to do some prior work

PR triaging:

• Abel backports (https://github.com/math-comp/math-comp/pull/944)

  • cyril should rebase and merge

• Add semi-module and semi-algebra (https://github.com/math-comp/math-comp/pull/1125)

  • some issue about scaling morphisms (semiring acting on a monoid), axioms are weird, looks only technical, not really interesting from a math perspective.
  • the current solution is not "composable"
  • cyril suggests following, which composes but does not cover "forms" https://drops.dagstuhl.de/storage/00lipics/lipics-vol237-itp2022/LIPIcs.ITP.2022.10/LIPIcs.ITP.2022.10.pdf
  • the PR affects multinomials, a generalization of it
    • another idea: op 1 = id, op -1 = neg should suffice for the generalization

• Keywords (https://github.com/math-comp/math-comp/pull/1123)

  • can be merge even if it is not the ultimate list
  • this metadata should be generated, but for now we don't have tools
  • the attributes supported by Coq commands such as Lemma and Definition should be extensible
  • maybe ping Assia for character, not necessarily wait for her to merge

• inductions on a measure https://github.com/math-comp/math-cocompmp/pull/1120

  • the PR cannot be merged as is
  • hints at lack of proper documentation

• sets https://github.com/math-comp/math-cocompmp/pull/1119

  • cyril reviews it

Sprint on finmap

• collision with Liberabaci on monday
• cyril does the announcement, the sprint starts on Tuesday