Coq Call 2019 11 13 - coq/coq GitHub Wiki

November 13th at 4pm Paris time. Add topics you would like to see discussed.

Topics

• Consistent formatting of wiki pages for Coq Call
• Behavior "loading vos then vo" (https://github.com/coq/coq/pull/11075)
• Summary on apply/typeclass resolution solving (Matthieu and Maxime) (Maybe not completely resolved? https://github.com/coq/coq/pull/10762) Related to https://github.com/coq/coq/issues/6583 Also, https://github.com/coq/coq/pull/10858 should alleviate problems with arbitrary resolution order (e.g. before or after unification with a goal type).
• Hearing about unifall status, some ideas of where we can go and how? (question by Hugo)
• Hearing about who is interested in the reference manual refreshing project? (question by Hugo)

Notes:

• TOC and format Advertise the call as well

• Agreement on the PR from Arthur, Emilio needs to finish his review.

• Bugs related to typeclass resolution "scope". On which evars to launch resolution? Should check about the VST perf.

  • Find some primitives to control typeclass resolution from the user side
  • Why use apply and not refine?
  • Trying out https://github.com/coq/coq/pull/10858

• unifall apply: First needs to fix https://github.com/coq/coq/pull/7825 to make appear We don't expect much CI breakage on https://github.com/coq/coq/pull/991 Hugo proposes to rebase 7825 and see what happens

  • Will need to evaluate performance precisely before going further. Already appears in the unify PR. Pierre-Marie and Maxime?

• Doc: Jim, Théo and I on the refman, will present at the next Coq WG (CEP before that).

• PR #10966 on its way, the rest of the PRs are postponed to next week.