Coq Call 2019 11 13
November 13th at 4pm Paris time. Add topics you would like to see discussed.
- 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)
-
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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.