Minutes February 10 2021 - math-comp/math-comp GitHub Wiki

Participants: Assia Mahboubi, Christian Doczkal, Cyril Cohen, Enrico Tassi, Kazuhiko Sakaguchi, Laurent Thery, Pierre Boutry, Pierre-Yves Strub, Reynald Affeldt, Yves Bertot.

Changing videoconferencing system

(Ideally zoom or BBB, but only a few of us have an account)

Switching to https://rendez-vous.renater.fr/mathcomp at least for the two next weeks to try it out.

Update on fixing simpl never

Yves has been working on it. https://github.com/coq/coq/pull/13448

There are few places which break in Coq CI. Sometimes it was because the fix was wrong and some places where simpl never might not be used correctly.

Does it make nosimpl obsolete? No because inside proof scripts there is no way to use vernacular commands.

More generally would it be possible to have access to arguments, canonically, etc inside proofs?

Coq's development may be going in the opposite direction.

Let us meet on Wednesday Feb 17, 10:00-11:00 and make a case for this to expose in the Coq Call at 16:00 the same day. A mail will be sent on mathcomp-dev about that.

PR 682

Assia asks the motivation: what benefits does it have on mathcomp and side projects? Right now it is not visible.

Cyril says it makes Sophie's development about transcendence of e and π portable to to current versions mathcomp. It was also meeting needs of mathcomp-analysis, linked to adding ceiling to the interface as Pierre Roux asked. Kazuhiko needs it for factoring code in quantifier elimination in linear arithmetic and real arithmetic.

Reynald: Why does it not use HB? HB not ready? HB port to mathcomp is not finished.

One should summarize the uses of this PR in the original post.

A question of priority: should we put all of our time in HB?

PR 464

Cyril: this has the same problems that we discussed with 682, but with even more overhead.

The question:

  1. Should we keep modifying the hierarchy while waiting for HB?
  2. Or should we freeze the hierarchy (e.g. PRs like 464 and 682) and work heavily on HB?

A poll for a meeting to join forces in porting mathcomp to HB will be sent on the mathcomp-dev mailing list, in order to evaluate this.