Minutes 2024 04 03 - math-comp/math-comp GitHub Wiki

Present: Cyril (chair), Georges, Reynald, Quentin, Yves (secretary)

  • update on finmap integration

Georges Gonthier worked on finpred recognition. There is a second unification mode in Coq where one needs that Coq recognizes finpred, but it happens in a state where Coq unfoled many definitions. Georges managed to find a solution that relies en canonical structures, but the same scheme should be usable for a coq-elpi based implementation.

Georges also signaled a problem where he wanted to work on dependent pairs, trying to package a HB structure ins a submodule. The #local flag does not seem to be handled by HB in ways that Georges expect. Cyril describes a solution, and the documentation should be in the structure.v file of HB.

While debugging Georges seems to have found a place where the current algorithm provokes unnecessary computations. Unification traces seem to be way to big when the problem is to find the value of val. In this case, it seems that the algorithms attempts to recognize a subtype structure 3 times in a row.

When a type is a subtype, it is more logical to compare objects on the base type, and it is never the case that a base type would not be an eqType while the subtype is. This should be used.

Follows a discusion about what computation happen and what parameters are unified when trying to solve a unification problem for val, and a question is raised concerning whether a certain mixin is a canonical structure or not. It may be that a bug has been detected and Cyril asks to see a more detailed example.

In the current stage, Georges Gonthier circumvented the problem by constructing a bespoke mixin with no named fields, also ensuring that the names of the projections for this mixin are not in the global name space.

The summary is that Georges thinks he can a version that works partially in about a week, but make the whole library work on that solution will take much more time. Still, there is a good separation of work between the porting activity that happened in higher files, while Georges is only modifying lower files (than the one where finpred is defined).

  • How to incite people to integrate their additions to math-comp

The question is about collecting from all the developments based on math-comp the general purpose theorems that are actually missing in math-comp and should be shared among all members of the community.

Should there be a dedicated coding sprint. Reynald expresses that our current way of working may be intimidating. People do not volunteer their work because it feels that too many questions of style and rigor will be raised and they would rather not have to give an opinion on these aspects.

Yves suggests that we could make voluntary visits on existing developments (the ones we are aware of) and propose integrating their code into math-comp to authors.

Reynald suggests we should set up a regular day (once a month) where math-comp experts would promise to be available to answer questions and discuss topics orally, especially on this idea of integrating code in math-comp. The discussion of people present leads to thinking this could be done the last Wednesday of every moth. There is a small discussion about how to choose a name for this event "math-comp sharing day" looks good.

  • How to set up one's computer to study and work on a pull request

There was a recent discussion on how to set up a working environment to have a version of Coq suitable to study a PR and compile the files of that PR.

Cyril suggest adding a "dev-container" based on docker so that people have an easy path to run Coq on math-comp (and a PR). He makes a demo, based on vs-code in the browser.

We have a to find a way to produce a documentation on how to re-use all this preparatory work, but Cyril himself feels unfit to write this documentation, because he know too much about how to make all these things work.

  • A discussion on a cleaner version of the "subst" tactic for use in math-comp

There was a recent proof (concerning matrices) where it felt natural to substitute all occurrences of a variable in the context with a value described by an equation. This is something that the subst tactic does well in vanilla coq, but subst has the default of being too unpredictable to be used in the math-comp library, where maintainability is an important design driver.

It has been agreed in a zulip discussion, that a clean version of subst could be added to the set of ssreflect tactics, taking a similar tactic in EasyCrypt as example. All participants of the discussion in the zulip stream seem to have agreed on a solution which is discussed in this meeting. Georges Gonthier asks for clarifications concerning the interaction with the "+" intro pattern.

While it is agreed that the benefits outweigh the costs of introducing this tactic, it is agreed that the syntax chosen for this tactic should not encourage its usage intensively, the same way as subst was meant to be used in vanilla Coq (as an automation workhorse). We converge in the direction of a {x in * |- *}-> , where the equation used for substitution is top of the stack (first hypothesis in the goal).

  • PR1179

This PR is now ready, it should be merged, Cyril will work on it.