Coq Call 2020 03 25 - coq/coq GitHub Wiki

Notes

  • PR #11896: evar instances represented as lists

    Much better suited to our manipulations (e.g. consing and looking at the head). One big slowdown in Math-Comp that should be solved by a better (less eager) substitution/reduction as part of w_unify. Hopefully the cbn/refolding code can be split from the reduction used in unification to be less reliant on this code.

    Question of delaying let-binding/substitutions in high-level constrs, e.g. EConstr.t + suspended substitutions. Generic problem of adding information to constr nodes: e.g. closed? evar-free?

  • PR #11832: Use doc-comments=before style. (Théo) Agreed to use =before. The introduction of ocamlformat should have been more clearly publicized. TODO schedule a later specific call once there is a style to discuss. Some worry about ocamlformat/odot not being very stable.

  • CUDW: probably postponed to the end of the year or cancelled.

  • Typing rule for let-bindings (PMP) let x := t in u : U[t/x] -> change to let x := t in u : let x := t in U to preserve sharing. Problem is ugly types (by default). Unclear to Enrico and Matthieu why in the case of no type dependency we could not remove the let (linear scan of the body's type). Just done in the kernel. Compat issues for Definition foo (n : nat) := let x := 0 in n and the difference with Check. Bedrock2 exhibits some quadratic behavior that might be linked: e.g. when proving an n-conjunct (for large n) involves a lot of duplication in terms. let-binding the type parameters helps in that case. Jason point to structural inductive types as a solution to that problem.

  • Issue #11894: CoqIDE does not highlight some assumptions with yellow (related to modules and module types). Not sure how to deal with it. Seems like a corner case.