Agenda

• Release for coq-8.10+beta1, future coq-8.10 and coq-8.9.1?
• Followup on finmap, multinomials,...
• Followup on PR
• Internship and PhD thesis topics.
• Roadmap for computing with math-comp

Minutes

• Participants: Cyril, Yves, Maxime, Enrico, Kazuhiko, Pierre-Yves, Assia, Marie, Georges, Reynald

• 8.10 beta1 -> math-comp 1.8 fails to build. Two options

  • 1.8.1 : minimal changes just to make it build:
    • make a new branch from tag mathcomp-1.8.0
    • make a PR with commits from April 29 targeting that branch + a compat notation for the derived constructor?
    • release
    • Q: can 1.8.1 be both compatible with 1.8.0 users and Coq 8.10 ? Not 100% but mostly, so we should test before deciding what to do. Moot: if you change Coq then you get he breakage from it, we can't hide it.
  • 1.9.0 : current dev
    • simpler
    • renaming taking place in master are there to stay (adds consistency)

• Shorten backward compatibility (may need to fix opam file)

• Decision: release 1.9.0 is done by/before Just 1st... drum roll... may 22nd!

  • Shepherd: Enrico
  • Guinea pig: Georges

• PR check:

  • Multinomial: September, nothing moves before that (#270)
  • Finmap: nothing moves, just kept compiling (#259)
    • Assia: can we chop it into smaller PRs?
    • Cyril: yes, but I want to know where to cut
  • Fixpoint in finset (#382) is ready (a dependency of Finmap's PR)
  • indexing functions for finTypes (#317) needs progress and Georges shall talk offline with Kazuhiko
  • generalize sort (#328) easy to fix broken CI, should go in with other improvements, namely:
    • some versions of the current lemmas for the more general sort
    • use nonPropType or more maximal implicit arguments to repair views that now are too polymorphic
  • invariant of merge sort (#346) is about complexity and we provide no theory, so it seems a bit out of place. Georges has a pending review with these comments, just submitted.
  • big-enough/near convergence? postponed to next meeting
  • hierarchy tests (#340) needs a fix to the make file, Enrico self assigns
  • PR (#203) evolves during the meeting and the ball is back in Cyril's field
  • dune (#316) ask how devel process works (load vo files in PG for example)

• Topics for interns/PhD

  • next meeting, running out of time

• Computing in MC:

  • Yves: intern wants to debug code by running it before he wants to prove it correct. Initially written in Python, and there it computes, then you go to Coq in R : rcfType and does not compute anymore. Yves hijacked locally the type variable R and notations, with some pain since one needs a bit of overloading for ==, that he resolved to different symbols to avoid the problem. This was enough to get executable code in Coq and debug.
    • Georges: hierarchy is transparent, you could admit the properties. This solves the overloading issue. You may still want to hijack square root for efficiency
  • Assia: irrationality of \zeta(2) needs some computations
    • ssralg->ring via ltac
    • used to be using CoqEAL, now ported to current MC, no more CoqEAL? Cyril just released a version, but won't work out of the box (define the morph?) so some effort is needed
    • options B, recent paper by Nicolas (title contains parametricity, univalence and transport): performance issue because of TC
  • discussion: seems a Coq problem in the large, not MC specific. Meetings on the topic shall be scheduled, but not before September and involving people outside this circle.