February, Thu 28, 2019 IRL Meeting, Sophia Antipolis, room Kahn K4

Agenda

• Libraries

  • Roadmap for merging big-enough, finmap and multinomial
  • Missing theory of valuation
  • UTF8 notations

• Tactic language

  • under (assuming @erikmd will attend)

• Documentation

• PRs to be discussed

• Automation

• Computations

• CI

• Misc.

• Organization of a forthcoming Mathcomp event

Minutes

CI (Erik presenting)

PR -> Gitlab mirror -> 5 versions of Coq (8.6, 8.7 8.8 8.9 dev) on docker Documentation https://github.com/coq-community/docker-coq/wiki -> GitlabCI executes a script (cf demo in the above wiki) -> Creates a docker image for coq (8.6, 8.7 8.8 8.9 dev) + mathcomp (1.7.0 + dev) -> Tests dependencies

Questions of Erik:

1. Which dependencies to add to the tests? Cyril: What about changes that are not backward compatible?

• Using an overlay mechanizm based on alternate branches in the CI yml
• Erik will look at overlays.
• Erik will propose a pull request for extra libraries.

2. Policy in cleaning docker temp. images in GitLab CI? (when this API for PR? In case of failure

• problem in the code: no incidence
• conditions external: rerun in exact same condition.

Conclusion: OK to consider a periodic task to remove temporary images, when the corresponding branch has been removed (typically by coqbot when the PR has been merged)

Upcoming release

• Be compatible with at least two versions of Coq (more if possible)
• Next version of mathcomp will be 1.8.0 and released ASAP: after merging PR291.
• No fixed released cycle but we decide to release more often (~3/6 month) and release at least as often as Coq (and anticipate with Coq breaking changes) and trigger the topic regularly.

Today:

• Release manager for 1.8.0: Enrico and Cyril they will also document the process.

Organization of a Mathcomp event

Summary of the discussion between ITP organizer and Coq workshop organizer. We abandoned a Mathcomp workshop for ITP 2019, but we would push for mathcomp talks at Coq workshop

• Yves: We never had such an event, we have to take the risk the first time
• Cyril wants a CoqIW-like event
• Assia: two possible directions
  • new users that could use mathcomp for their work
    • what about people which are not Coq users?
  • existing users that want to meet each others + dev
• Maxime: CoqIW goal's was the interaction between dev and users, but for mathcomp it makes less sense than CoqIW to center the event around the dev/user boundary
• Assia: likes the informal side of the CoqIW though
• Cyril: likes the "suggestions" + discussions + groups format (CoqIW style)
• Maxime: let us have some Coq developers at this event
• Marie: to attract new users, it must be very attractive: we need money and a nice location.
• Assia: talks with big names for two days and discussion slots next days
• Maxime mentions SOFA days
• Assia: Florent Hivert is a Sage developer, and told us about SAGE days, focused on a certain topic 10-15 ppl in a remote location.
• Assia will teach courses of mathcomp in Amsterdam, focus on math.
• Yves does not believe in attracting people who hesitate. For them, there should be a one day tutorial, which can be glued to another event (as Assia said).
• Maxime notes that CoqIW people come to save time by discussing with dev.

Tour de table

• Yves likes it and likes it to be flexible
• Enrico: good idea but we need a plan B in case we do not have enough people (e.g. a mathcomp dev workshop), alternatively a school is easier to guarantee participation.
• Georges mentions the Spring school 2012 MAP format (Assia thinks it was intense and a bit too dense)
• Laurence: it is a good idea to have a mathcomp event
• Kazuiko: good idea, he would have needed such an event 3 years ago when he was learning. Nowadays, he would come too.
• Erik: good opportunity,
  • both the MAP Spring School 2012 (MSS 2012) and CoqIW style are useful.
  • Have a couple days to intiate mathematicians to mathcomp.
  • Interested in talking there about specifics of mathcomp.
  • Have a one week event.
  • Maybe make choices on which public to attend.
  • Dedicated workshop inbetween MSS2012 and CoqIW
• Georges: more focus on applications than MSS/ Let enough time to do a hands-on demo.
• Cyril: good idea, likes the 1 day tuto + 2 day talks + 2 day discussion format and let us have plan B as Enrico said.
• Maxime: good idea. Note that CoqIW changes name and content every year.
• Damien: good idea. Focus on applications. People bringing their own problems and applications, and seeking advice of experts. No more tutorial -> redirect people to these.
• Reynald: from MSS what he remembers was the exercise sessions. dev and people bringing their own exercises. (not everybody may have their own exercise, so we need to provide some of them)
  • Assia: tentative topics? MSS2012 had to kind of talks: first lectures and at the end star talks Should we have invited speakers talking about own applications?
  • Georges had this in mind.
  • Reynald: more WIP and less finished work (invited talks)
• Marie: 1 week school + talks is good for PhD students. Otherwise it is too difficult.
  • That is why Yves suggested to have a 1 day tutorial as a "show-off" Deep spec school might have this kind of format.

Conclusion: having a user oriented mathcomp meeting looks like a good idea for everyone. Target audience unsure. We discuss this later. Assia takes the lead of the discussion by mail -- which does not necessarily mean she will organize the even.

PR discussion

• Assia: it looks like a rainbow, where to look, how to?
• Maxime: have a code owner file and automatically add reviewers We need to have a assignees who are not necessarily knowledgeable and have to know who to ask, who to ping.
• Assia asks about "needs:rebase"
• PR203: someone should be assigned
• explanation for needs propagation
• Cyril will more generally give description to labels (also" kind:tool" should be more pink-ish)
• PR261 recap is badly phrased
• PR221 we should ask Florent about it. <- Cyril should lead the discussion
• The phrasing of the contributing guide should be better.

Conclusion: Have good practices. Be careful about PR messages. Most PR are WIP. Only one blocking PR for the release 1.8.0.

Libraries

• Roadmap for merging big-enough, finmap and multinomial
  • status
    • bigenough subsumed by near
    • finmap is in the progress to be merged in mathcomp in the form of several PRs
    • multinomial needs to be reworked
    • finmap refactored to extract order and norm
  • what to do?
    • assia: can't we have an incremental roadmap?
    • cyril: regarding finmap
      • it is mostly a matter of copy-pasting chunks of code from finmap.v into mathcomp (into seq, etc.)
      • there is a performance issue
    • maxime: potential issues should not block a merge
    • the merge of finmap is blocking other merges
    • assia: can it be done by the next meeting?
      • hopefully another one with near?
        • Grab Existential variables... requires a plugin
    • assia: is the dependency of multinomial w.r.t. bigenough important?
      • mpoly uses bigenough only 21 times
    • enrico: target which version?
      • cyril: let's target 1.9
  • maxime: computation with finmap? is it part of the long-term plan?
    • cyril: the current finmap does not compute and is not supposed to.
    • erik: coqEAL provides computation for multinomials but does not rely on finmap but uses AVL trees from the standard library
    • assia: rename finmap? (no) + Missing theory of valuation
    • not discussed + UTF8 notations
    • not discussed

Tactic language

• under (assuming @erikmd will attend)
  • slides by erik
  • started as a tactic in Ltac1 discussed with cyril
  • to apply some tactics under a bigop or so
    • instead of evar and rewrite
  • now written in OCaml with enrico
    • two tactics
      • under
        • pattern to locate the place where to rewrite
        • discussion on the handling of binders in the two branches opened by the under tactics
        • discussion on the ordering of the syntax
      • over
        • terminator tactic
  • demo using eq_big (the extensionality lemma for bigops)
  • detailed feedback appears as a comment by enrico in the PR coq/coq#9651

Documentation

• Issue coq/coq#9669 by enrico and PR coq/coq#9672 by erik (about the doc of by [t1|t2])

Postponed to next meetings

• Automation

• Computations

• Documentation

• Libraries

  • Missing theories (e.g. valuation)
  • UTF8 notations