Minutes 2017-11-21

Participants: Laurence, Assia, Cyril, Yves, Emilio, Enrico, Damien, Maxime, Laurent.

Assia: not much going on on the repo. Not clear how to make the library evolve, what should be improved, etc. Should it evolve or stay like that? I prefer the first option but needs to be a team activity, not a single person. Cyril agrees.

Maxime: there are PRs, maybe "who" makes it evolve is not clear... Assia: the meeting is between people that should drive the evolution (editorial board), PR can be driven by a punctual need.

Recap of the status: in Coq 8.7, ssreflect + ssrfun + ssrbool is in Coq. eqtype is not in Coq since it starts the hierarchy (formalization choice, CS vs TC), and is also where cutting was easy (no duplicate, eg seq vs List). This is why only a few files were merged. Shall we merge more? Laurent suggests to merge the whole ssreflect module. Enrico agrees, stresses that we did a baby step in 8.7, we can do more later.

Assia: documentation and advertisement of mathcomp, even for basic stuff that could be merged, is not there, e.g. seq. How do people find seq rather than List?

Going back to the main point, evolution. Who takes the decision to integrate a PR? We look at PR#41 and analyze why it was not merge yet.

Emilio: proposal: "staging area" holding stuff that is merged but not yet considered as mature. This brings a quicker merge process, and leaves space for later refinements. Users must be able to use the staging area.

Careful check of PR#41, some actions happen quickly, some after a long delay. In the very end the stall is cause by an extra change sneaked in. Maxime's suggestion: ask to separate the PR in two, merge the part that is OK and continue discussion on the rest. Emilio's + Maxime: merge in the staging area, and eventually fix/revert the controversial part of the PR. Emilio: it is important to remove blocking processes, and be more smooth. Laurent is not very fond of this idea, better a stable thing.

Cyril: we need a travis running on user's code in order to evaluate big changes on the whole library.

Going back to #41, two roles emerge: the main reviewer and the one acknowledging the requested changes have been made. The two roles may be taken by different people, the latter being way more lightweight.

We look at #115, no reason not to accept it, just lack of confidence. We merge it.

Recap of how the PR reviewing UI of github works. A point is made: decision taking (we should change that) are integration (work on a PR and merge) separate steps and can be taken by different people. Clicking the button should be made by anyone that thinks that the decision was taken, it is not the action of pressing the button that "takes the decision". In any case one can revert (e.g. if he clicks and it was not the result of the discussion).

We go trough the steps defining the life of a PR (request review, check pending reviews... ). Now we are all github black belt.

Call for volunteers to work on the math-comp repo:

• Laurent: PR management (check for forgotten PRs, merge things that are ready, ping people)
• Enrico: Nitpicking on proof scripts (identify fragile scripts, enforce conventions)
• Laurence: PR management
• Emilio: CI infrastructure
• Assia: Reviews and PR management
• Cyril: Reviews and PR management

Let be clear, anyone can review or animate PRs. The people above commit to spend some time regularly.

TODO: checklist before clicking merge.

CI should also use gitlab, Emilio has a plan.

Staging area: discussion of what it is for, how it differs from a separate project....

• a key point seems that things in the staging area are shipped with math comp, even if they are unstable and may disappear in the future
• not so clear what to do when multiple, conflicting code tries to land there (e.g. multiple ssrreals)
• another key point is that the staging area contains extensions to existing libraries (not entire new developments)

Another thing emerges:

• staging for things that will eventually be merged
• extra for stuff that will never be merged but could still avoid duplication (eg. eqType on Coq.Reals)

Minutes 2017-11-22

Participants: Laurence, Assia, Cyril, Yves, Emilio, Enrico, Damien, Maxime, Laurent, Xavier.

Continuing last topic of yesterday: Another example for these extra libraries: boilerplate to communicate with decision procedures (psatz, lia, etc ...).

• Documentation
• Visibility
• Roundtable of topics to work on

Documentation

• the installation of ssreflect/math-comp used to be inaccessible.

  The mathcomp github README.md webpage was made for dev and is not readable by an external user.

  Assia: We should inspire ourselves from pandoc installation guidelines of https://pandoc.org/installing.html for example, and put them in our README.md. or website?

• The website is not visible enough.

  TODO: Modify the old ssr.msr-inria.inria.fr htaccess to have a 403. Or close it, and check we are losing nothing?

  TODO: Release checklist website.

  TODO: README.md -> description of mathcomp and link to the website and wiki and other resources. Try to remove redundancy between website, README.md and github releases

• Portability of mathcomp

  • docker?

    Assia: E.g. you want to distribute an artifact for a paper.

    Do we want to use docker for mathematical components?

    Yves: This mostly interesting for people using clusters. But this can be good for visibility.

    Emilio: This is a problem of Coq, it should be escalated to Coq during a Coq Working Group.

  • Coq in your browser?

    Emilio: there will be a new release of jscoq for the Iris tutorial in POPL, mathcomp should be supported. However browser performance is still a problem, but there is hope for tutorial.

• Documentation of the code

  Laurent: why is there no "help" functionality in Coq (as in Maple).

  Maxime: there should be a standard format to write documentation in Coq and a standard way to read it. For now the only existent solution provided by Coq is Coqdoc.

  Laurent: ssreflect Search replaced grep for me, except for bigop

  Yves: Headers are not easily accessible.

  TODO: check coqdoc output for problems: truncated vernacular, misprocessed comments, in particular header rendering problems.

• Documentation of the style

Afternoon

Laurent: I volunteer for documenting installation instructions.

Assia: the page of math-comp.github.io/math-comp needs to be cleaned. The first link in section Documentation points to something that is practically useless.

Maxime asks why the wiki is a separate repository in the math-comp organization. Should we move the wiki to math-comp. For documentation, these thinks should be served by a normal server. There are three possibility. There should be more than the README.md, there should be links to where the really good information is placed. There should be a web-page that remains very stable, and then a wiki that makes it easier to react to proposals from users.

All people of the math-comp organization are allowed to write in the wiki. There is a discussion on who has write access on this wiki. There is agreement for the wiki to be moved to math-comp, making this wiki writable by every gitub user. Cyril volunteers to make this move.

Assia: still looking for a volunteer for two tasks: checklists on how to manage a pull-request and how to manage a release. Cyril volunteers for the checklists. Theses checklists should be approved by Maxime.

Coming back to the README.md, Assia agrees to take care of it. Where should the current contents of this file be moved. First proposal is to construct a file INSTALL_DEV.md and have this under a dev/ directory. There is still hesitation about the checklists for pull-request and release management that could also be stored in this dev/ directory. Maxime points out that programs can also be stored next to the checklists.

Assia requests input from Xavier and Emilio about the current documentation and the changes that could be suggested.

Xavier started directly on math-comp. The difficulty came from the absence of a book, and reading the sources was the main solution. What is really missing, is how to use the things. The material from all the schools (especially the map 2012 school), was really valuable, but all this data is a bit too spread out with no really unique place for links. Xavier has a clear memory of difficulty with finite types. He came to finite types through matrices, especially "block matrices".

The coq language does not give much support to implement abstraction barriers. For linear algebra, there is also the question of whether one should work at the level of vector spaces or at the level of their implementation using matrices.

Assia shows some part of the math-comp book (page 183). She shows what was made in embryonic stage for natural numbers. The goal is to provide a summary of what users must know, with more information than the headers. Laurent suggests that there should also be pointers, Assia agrees, but would like to know how this should be organized.

Xavier notes that there are several choice in this kind of documentation that correspond to different levels of litteracy by users.

Xavier sees that there are a few examples of uses of tactics and insists that this kind of illustration is important (to be used as a cheat sheet).

Assia asks another question about the difficulty to find the right files. In a synopsis like the one started on page 181. Xavier thinks it is important to have the tools of induction for natural numbers, but Assia objects that when the functions are provided in libraries the proofs by induction are already done and users should rarely have to redo proofs by induction, one wants to explain what are patterns, using certain combinations of tactics and theorems.

Assia thinks that this kind of synopsis should not necessarily be in the book. Enrico argues that we are seeing is a duplication of headers. Maxime points out that maintaining the documentation is a difficult task and using the wiki to rely on documentation is adding a synchronization difficulty. The same source archive should contain both the code and its documentation, the pull-request that modifies both should be the same (and this should be described in the pull-request checklist).

Tasks: read what is in the synopsis what are all the libraries being covered, what are the elements that must be listed for each library. Laurent suggests that all cheat-sheets for our winter schools should serve as basis for this synopsis. Assia takes the example that big operators should be mentioned in nat for instance. For Enrico, this part is very useful.

Assia thinks that the first version of the book could come out only with seq, nat, and bool, knowing that nat for instance also contains prime and div. For bool, this means a synopsis usable in copy-paste for boolean reflection, having predType... An alternative point of view is that proof patterns are part of the language (case/andP seen as a single word).

After the break.

Assia asks again to Xavier what topics he would like to see covered. He insists that documentation is important. The next stage is guidelines to organized developments that become quite large.

Assia suggest that we use as example the file STYLE.md from the HoTT development. Of course, the style we defend may be different, but the pattern of the STYLE guide is integersting. People have a hard time promising to work on it, but Cyril volunteers to start working on this topic and Assia volunteers to help.

Assia would like to clarify that all volunteers mentioned so far should start working on their topic before the end of 2017.

The material from all schools should be easy to find. All tutorial and recent schools should be mentioned in the tutorial page from the wiki. Yves volunteers to do it. Emilio suggests that we should also have pointers to introductory documents that are not necessarily at the level of full-fledged tutorials.

Making a census of existing projects. Assia points out that a wide census is a different question from knowing which projects can be used to help quality insurance. This is more to advertise that this has been used by several people in several context. Making lists of papers and formalization.

Emilio indicates that having two different names makes it more difficult to find projects on internet. Yves suggests that we should also suggests to users a preferred way to refer to our work.

Laurent will look around, but will not promise a fast action on this topic.

Discussing the next meetings. If there are many contributions, then we should start to have regular meetings. topic drifts to the question of releases. Enrico says that there should be minor releases of math-comp for each release of Coq. Assia points out that it is enough to have minor releases because this overlooks opportunities to clean the library when new features of Coq make it possible.

We should have at least virtual meetings to plan tasks and road maps and meetings to review outstanding issues. We should also plan meetings to meet intensive users, this should be planned as specific workshops probably as satellite to conference.

Emilio says that ssreflect has a few hundred questions on stackexchange. This should also be referred to from the documentation site.

Review of what are the current project

Maxime there are two problems with the image so far: identifying that math. comp. is for math is too restrictive. There are many good ideas in math. comp. that are not specific to applications in mathematics. There should be more implementation of tools that extend math comp for application in programming languages. For instance, inversion should be better covered. Adding more code in the ssreflect plugin is highly complex and right now manpower is lacking for these extensions.

Assia: there are things in what you describe that do not require more coding in the plugin.

Maxime: there was also an effort to port software foundations on top of ssreflect. Beta pushed quite far his experiment and the lack of inversion is a problem.

Assia: porting software foundations verbatim is too constrained an exercise. Taking the example of the definition of even shows the message conveyed by software foundations is not compatible with the philosophy of math comp.

Follows a discussion on software foundations.

Maxime would like to work on improving ssreflect for CompCert-style proofs and to obtain a better unified library with Coq. There is a lot in CompCert about inductive and co-inductive predicates.

Yves works on Delaunay triangulations, using fingraph.v for example. projects are visible.

Laurent would like to make computations on Grobner bases.

Xavier works on convex polyhedra especially combinatory properties. With a colleague, they have mostly used linear algebra, now they are looking at the combinatory properties, adjacency properties. On math comp the thing that is quite annoying is the fact that automatic verification using lra is not provided. Using Farkas' lemma would be great. The lack of ordered structure is a problem. order combinations would be useful. finmaps would also be useful. Manipulating about block decomposed matrices is also horrific.

Assia when time becomes available but has three subjects as objectives.

• improve how to branch automatic tactics of math comp structures, adapting ring, lia
• libraries with real numbers, in collab. with P.-Y. Strub (objective : discrete probabilities), slow project. Difficulties find good axioms,
• have good tactics (managing side conditions, transitivity reasoning modulo side conditions), Would also like to work again on certified computer algebra.

Cyril

• rewriting an interface for Coquelicot that is more mathematical components compatible try to minimise the number of definitions. Work on this topic with Reynald Affeldt and Damien Rouhling. Cyril also has a lot of positivity conditions. - Also re-implementing bigenough, that could be integrated in mathcomp.
• There is also work on Tarjan and Kosaraju.
• Cyril also has unitary matrices (aiming for the spectral theorem, aiming for robotics). Quadratic forms are badly packaged.
• Re-implementing the refinement part of CoqEAL on top of ELPI (especially parametricity plugin).
• The task on finmap is quite blocked right now.
• There is a library of orders that has been designed listening to requirements from P.-Y. this one is below in the stack and is a huge task.
• AC tactic.

Laurence

• hermitian forms (with Cyril) and then clean the character theory of math comp from this
• Lots of work on Coquelicot and FLOC, use ssreflect but lacks good support. Waiting for a good support of Coquelicot compatible with math comp. FLOC is an extra level of difficulty.

Emilio

• work on the user-interface side, goes quite deep in the system. modularity, parallel processing. Relevant to math comp for notations, questions of parsing (discussed with F. Pottier, but extensible parsing is a difficulty).
• verification of real time signal processing, sees that math. comp. gives very little.
• Database theory HoTT/SQL paper is an example that is not satisfactory (missing working on monads) Insist that finite types are a very good fit for this kind of work. display tags are difficult to use.

Enrico

• improving the pretyping : elpi as a programming platform for studying the algorithm
• elpi is now a scripting language for Coq to write tactics and commands
• soon: derivation of boolean comparisons and their correctness proof.
• hope to use it as a hierarchy scripting language: Cyril, Sophie, and Enrico should work on this (visibly Florent should be included in this discussion because he has his own hierarchy)
• for coq 8.8 hopes to work more on the ssreflect language, especially the new intro patterns (Maxime thinks it is critical to make this code easier to understand) there is work on documentation to do too. Enrico will be available for this starting half January.

Maxime highlights that maintaining the code of the ssreflect plugin is a daunting task. Assia says that it is important to ask Georges what his plans with respect to this code.