Minutes October 04 2023 - math-comp/math-comp GitHub Wiki

Participants: Reynald Affeldt, Cyril Cohen, Pierre Roux, Quentin Vermande.

Topics for 2023/10/04:

• Schedule of the 2.1 and 1.18 releases
  • Pierre & Reynald found dates to coordinate
  • Cyril: after 1.18 we can stop with mathcomp 1
    • Reynald: infotheo and monae are not on mathcomp 2 yet, because of a bug in HB, so we may have to have a mathcomp 1.19
    • Pierre: The mathcomp 2 pr of Abel was not merged yet and Jasmin's neither
• scope issues with constant literals in ssrint: #1086
  • we would like 42%:~R parses to (intmul 1 (Posz 42)),
  • Cyril does not understand why we want Posz and not natmul, they are convertible, where does this issue occur?
  • Pierre: possibily in the use of algebra-tactic in apery,
  • Pierre: what about automatically normalizing natmul 1 n when n is concrete,
  • postpone until both Kazuhiko and Pierre are here.
• organization of a coding sprint about finset/finmap for December 2023.
  • we will organize a coding sprint week with Georges.
  • a non-parallelisable session at the beginning to coordinate.
  • not for mathcomp 1
  • a list of checkboxes to lock and avoid conflicts: reproduce Enrico's colored graph of files?
• extra topic: https://github.com/coq/coq/pull/17576
  • the removal of Let x := .... Qed. from Coq has an impact
  • proposal by Gaëtan replaces two lines by one, which would not be so nice in mathcomp
  • Cyril: this is a XY problem, the purpose was to have a private lemma which augments the context. This could also be a side effect of https://github.com/coq/ceps/pull/42
    • Pierre: add to Coq Roadmap https://github.com/coq/ceps/pull/69
    • Pierre: mathcomp compiles just with prelude and without stdlib https://github.com/proux01/math-comp/commit/c3150b7a650efee5490c7c7b8a57c298d5341efa . Looks for a volunteer for stdlib chapter of the roadmap.