March, Fri 22, 2019 IRL Meeting, Paris (2 rue Simone Iff), Salle de Visio Grace Hopper C118

Suggestions

• interns linked with mathcomp

• Documentation

  • what is needed?
  • Let's find relevant examples
  • editing the ssr doc inside coq's

• Current news

  • PR math-comp/math-comp#270
  • release
  • PR math-comp/math-comp#221
  • PR math-comp/math-comp#203
  • dependent and positive finfun

• Organization of an event

• Roadmaps towards merges

  • finmap
  • multinomial

• Libraries

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

• General list of current projects

• for discussion next time

• Computations

• Automation

Minutes

Present : Reynald Affeldt, Yves Bertot, Cyril Cohen, Maxime Dénès, Georges Gonthier, Assia Mahboubi, Laurence Rideau, Damien Rouhling, Kazuhiko Sakaguchi, Laurent Théry, Enrico Tassi

1. Internship :

   • Yves : there will be 3 students working with mathcomp in Sophia on computational geometry : one (6 months) on Voronoï diagram, another one (6 weeks) on decomposition algorithms, and the last one (6 weeks) on visibility walk.
   • Assia : she will also will also have a student (6 weeks) on number theory (computing class number for quadratic fields)
   • Assia : we should add something on the website with a contact address indicating that we welcome interns

2. Documentation:

   • Assia : the documentation should be improved, it is difficult to find what the current documentation of the system is. The "tutorial" page of the web page is obsolete.

   • Maxime : it is very bad for ranking to leave link to obsolete material.

   • Assia : Lean and Arb two website to get inspiration from.

   • Maxime and Yves : there should be at most two tutorials.

   • Enrico : one for installation and one on how to use the library.

   • Laurent : the material from the various school could be a good starting point for tutorial.

   • Maxime : the web site should be fixed and it needs a web maintainer.

   • Laurence volunteers.

   • Cyril volunteers to restructure the web page to contain less materials.

   • Enrico volunteers to propose logos.

   • Reynald raises the issue of having a FAQ.

   • Yves : we could use stackoverfow as a mean to collect questions.

   • Enrico : there is no mathcomp tag but an ssreflect one.

   • Assia : what about missing tips and gives as example the issue 212 by anton as an example of material that could be turn into a tip.

   • Everybody agree that we need more of this kind.

   • Cyril : we should postpone the decision about FAQ and tips after contacting external people (like Arthur Azevedo De Amorim) for advices.

   • Yves and Maxime volunteer to contact them.

   • Assia : the use of sphinx for the documentation of Coq has made it more difficult to perform changes. Setting-up a proper local environment to rebuild the document is difficult.

   • Other participants share the same experiment.

   • Maxime : maybe the instruction how to build the doc maybe obsolete and advocates the use of nix (since it is what is actually used to build the documentation).

   • Assia and Cyril agree to give a try

   • Maxime : I will update the instruction after these trys.

3. Organization :

   • Enrico : we should mix working meeting with discussion meeting.
   • Maxime : working in small groups on specific tasks.
   • No decision is made.

4. Lunch break

5. Next meeting :

   • Everybody agree on a date for the next meeting: 23 April from 9.30 till 12.30.

6. Release :

   • a discussion is started on the next release.

   • Cyril : the only blocking PR is PR #291. This should be reviewed and merge by April 1st.

   • Assia : this PR lacks a regression test as it fixes some problem. She also indicates that it would be nice if these regression tests could be automatically generated from the graph Kasuhiko is producing.

   • Georges : we should decide what goes in the next release.

   • Enrico creates a milestone 1.8.0 and show how to add this to the PR that should be in the released. Some are added live.

   • Some other improvements are discussed.

   • Kazuhiko : he has a modification to fintype that would make the extraction of finfun application (fun_of_fin) run in constant time.

   • Georges : the proposed modification may not be compatible with the way the new version of finfun works now.

   • Georges : also PR #221 should be included in the Abel branch.

7. Roadmap to integrating finmap and multinomial

   • Cyril : the situations are quite different between the two. Finmap is almost ready only pull requests 301 till 305 needs to be merged. For multinomial the situation is more delicate.

   • Assia : maybe a progressive integration for multinomial.

   • Cyril proposes to present his roadmap for integrating multinomial at the next meeting.

   • Enrico : shortening the Require using the _all files.

   • Cyril : it forbids parallel compilation.

   • Georges : better to be precise and give explicitly the dependency.

8. Computations :

   • Maxime : the design of the new standard lib of Coq he would like to have libraries that compute and having lock or bad complexity could be an issue.

   • Cyril : if we want real computation, refinement (Coqeal) is the way to go.

   • Assia : writing C code in why3 producing mathcomp could be an interesting alternative for real computation. There was an attempt to have a why3/mathcomp output but she does not know the situation.

   • Georges : one reason why mathcomp is not good at computing if that there are much more opaque objects in mathcomp than needed. The problem is that currently comparing term has exponential running-time especially when the comparison fails. So shortcuts were artificially added to make things compile in reasonable time.

   • Enrico : congruence closure could be made more efficient more easily if the reduction would be more naive.

   • Maxime : having a naive reduction could be bearable since we have vm_compute.

   • The discussion shifts to what could be improved in the library.

   • Georges : we should make more use of the printing only capability. Also some constant *_head were artificially added along with some notation. This could be replaced by some arguments annotations. Finally simplifying the grammar would be nice but there is not much that can be done with the current version of Coq only grammar entry for binder could be used.

9. End of the meeting.

Roadmap for mathcomp website

• have one or two tutorials at most
  • how to install
  • how to use (reuse mathcomp winter school)
• the current "tutorial" page should be renamed "bibliography"
  • have a comprehensive list of publications
  • either on a webpage which is not followed by search engines?
  • or a bibtex?
• updated deprecated tutorials (at least 2 + manual) on HAL
• website
  • Laurence is in charge of the website
  • Maxime volunteers for moving the website to the root of math-comp.github.io
  • rephrase the main page: Cyril
    • remove the link to reference manual
    • mathcomp logo and not MSR
    • links in both direction with mcb
    • link to the install
  • decide on a mathcomp logo: Enrico
• include the tutorial in the CI and release process