Coq Call 2020 06 17

• June 17th 2020, 4pm-5pm Paris Time
• The link to the visio room: https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• universe minimization to set based on Prop <= i (Janno, Gaëtan, Maxime, Matthieu?, Pierre-Marie?)
• discrimination trees for typeclass search (Janno; trying to figure out what's there and what could be improved)
• conversion checking flag for plugins (Gaëtan) (https://github.com/coq/coq/pull/11456)
• needing help to sign the 8.11.2 MacOS package (PMP)
• proof engine state & evar_map

Notes

• universe minimization to set based on Prop <= i (Janno, Gaëtan, Maxime, Matthieu?, Pierre-Marie?) https://github.com/coq/coq/pull/12449

  We face a problem with the unification/minimization heuristics, and need to make a larger plan and clarify the workings of the universe elaboration phase today and how to improve it. Janno will report on the PR's effect to see if it is worth pursuing.

• discrimination nets:

  Janno reports a strange behavior of typeclasses eauto that does not seem to use discrimination at all. We will need to see an example of the issue, it sounds like a bug.

• conversion checking flag:

  ppedrot reminds us that we should update the checker w.r.t. unsafe typing flags. It seems the granularity of admitting the conversions is too fine and we should rather allow admitting whole terms in the environment.

• need a MacOS specific team for testing packages and also, streamlining the dmg release process.

• evar_map & engine

  We will need to put the shelving state of goals in the evar_map so it's accessible by the proofview/engine and unification. Hopefully we can make it abstract enough so it can move back to the proofview once pretyping and unification move into the prooofview monad themselves.