Minutes April 06 2022 - math-comp/math-comp GitHub Wiki

Participants: Reynald, Enrico, Laurent, Pierre, Yves, Cyril, Enzo, Kazuhiko

policy for version support of coq-community/fourcolor (YB):
- now that the repository has moved to coq-community, are there rules that we want to keep with respect to backward compatibility, or merely suggest?
- many warnings produced by fourcolor
- see PR #41 https://github.com/coq-community/fourcolor/pull/41
  - to have a warning-free compilation with the most recent version of mathcomp
- master should support at least the version supported by mathcomp
- master of fourcolor supports 8.11 and 1.11
- Reminder: mathcomp should be at least compatible with the last three versions of Coq
demo of POC of lra tactic for MathComp (Pierre)
- https://github.com/math-comp/algebra-tactics/pull/54
- still problems with large constants (as mathcomp uses nat)
- backtracking in elpi may be slow (particularly when lra fails) but is currently needed to handle disjunctions
- trackt: preprocess Coq goals before calling tactics, based on declarations of mapping between source and target symbols
  - https://ecrancemerce.github.io/trakt/#/presentation
- problem with introduced dependencies with large parts of the standard library?
About the language of patterns for rewriting (YB): introduce pattern disjunction and make it possible to incrementally extend the pattern associated to a given name
- https://github.com/math-comp/math-comp/pull/869
- we can add new theorem to multi-rules, can't we do that with notations?
- which symbol? use "LHS of something"? like
```
rewrite [LHS <]foo
[LHS ==]
[LHS +]
[LHS ==%B]
```
  Notation LHS head := (... X in head X _). E(?) = (X in E(X)) [? < _] [here < _] (not much shorter than [X in X < _])
- needs to hack ssrmatching.v?
- use U+1F78B?
KS: If we will move most repositories in the MathComp organization to the Coq Community, I'd like to move Algebra Tactics (and Mczify) soon. So I'd like to hear about the experiences with moving fourcolor and apery to the Coq Community. Since a paper about Algebra Tactics has been accepted, I want to avoid changing the URIs of the repo after submitting the final version, although the old URIs will be automatically redirected to the new URIs.
- with the fourcolor theorem, it turns out that Karl did much work
- maybe keep it on the math-comp side if it is active
next math-comp project to move? Coq-combi? Let's discuss the case of mathcomp-analysis in a mathcomp-analysis meeting.