Coq Working Group 2019 12 16
- Maintainers update [Théo]
Lunch
Armaël Guéneau's PhD defense at Inria Paris.
Hacking session, afterwork+diner in Paris at l’Encrier 55 Rue Traversière, 75012 Paris, at 7.30pm
- Next Coq IW, we may need to act now [Emilio, 2']
- Open recursion pretyper [Pierre-Marie, 30']
- Coq and Machine Learning [Emilio, 30']
- Incremental type-checking [Emilio, 30']
- Lunch
- Coq and OCaml [Emilio 15', GMM 15']
- Status of build automation for Coq projects [Karl, 10']
- Integrating Scala as a new extraction language for Coq, see Scallina [Joseph, 10' on my side].
- Poll about corner cases in implicit arguments and notation (anonymous implicit arguments, inheritance of implicit arguments and scopes in notations, ...) [Hugo, 10' on my side]
- Primitive projections for positive tuple types [Hugo, 10' on my side]
- Deprecating coqdev in favor of https://coq.discourse.group/c/coq-development (Théo, 10-20 minutes)
- Refactoring the refman [Théo and Matthieu, 30-45', as late as possible so that Jim can attend]
- needs:discussion PRs
-
Updating maintainers (Théo)
Done! See CODEOWNERS file. Questions remaining:
- Should we revise the 5-days w/o response from the maintainers rule?
- Reviewing is done as a member of all your teams (not optimal yet)
-
Aside: should we remove coq-tex?
Pierre-Marie was ready to organize it in Nantes or closeby (should be careful about connection from e.g. Nice). PMP: do you confirm?
Zero cost, allows to make variants of the pretyper. First step is "easy" and backwards compatible. Second step is to functorialize w.r.t environements and return type, providing EnvLike "interfaces" and more work. Emilio fears we will need more thinking about composition and maintainance, if we let users modify it arbitrarily. General agreement on doing the first step.
Emilio presented his projects on combining proof assistants and ML, in particular based on the SerAPI infrastructure. Slides? Part of an "Action Exploratoire" that could become his main subjects in the coming years.
Idea: more fine-grained dependency analysis to have a build system on top of Coq (for coq objects: lemmas, definitions, ...), inspired by dune. Prototype to appear in the coming months, should allow really fine-grained dependency checking. Very hard problem though, requiring much more functionalization.
=> Idea of a task force on functionalization together with Hugo, Maxime to finish that?
native-compute (easy). stdlib -noinit close as well
(per-file flags in dune now). See PRs on dune for updates.
- Lunch
-
Fix signal polling for OCaml 4.10 #11123 We need to integrate so as to be compatible with 4.10, but cannot close the bug: there is still a memory corruption bug in the VM. Guillaume MM thinkg the 4.10 version of the patch is the right way to do it, and the bug lurks somewhere else in the VM. It will take time to diagnoze the source.
-
Locks and coordination issues: how do we coordinate large-impact changes (e.g. to move to MultiCore at some point, to finish functionalization...)
-
Backtraces and exceptions: Emilio and PMP seem to disagree about the effect of Emilio's PR.
-
Asynchronous exceptions and resource usage: multicore is apparently set to remove them. Algebraic effect handling is leaky in presence of asynchronous exceptions. GMM is trying to improve the situation there, in ocaml. Emilio suggests planning meetings on ocamllabs' slack about ocaml-multicore and coq-multicore.
-
OOM killing/Out_of_memory exception recovery. Blog post by GMM on discuss.ocaml.org. JH Jourdan is adding support for checking out-of-memory errors: we should see how it applies to us.
- dune for Coq packages. First needs a coq-dune.1.0 version: Should have a meeting in february about the installation of libraries. There will be a dune retreat in febraury. Emilio mentions current discussions in dune on implicit transitive dependencies. Anton asks about: Is there any progress on Dune support in PG or CoqIDE?
Integrating Scala as a new extraction language for Coq, see Scallina [Joseph, 10' on my side].
Joseph presented his PhD work on translating Coq to Scala, including GADTs + path dependent object types. So extending extraction to handle higher-level features. Prototype implementation in scala, starting from source syntax of Coq. Discussion of targeting more typed languages.
-
Implicit arguments: about corner cases in implicit arguments and notation (anonymous implicit arguments, inheritance of implicit arguments and scopes in notations, ...) [Hugo, 10' on my side]
-
Primitive projections for positive tuple types [Hugo, 10' on my side] Proposal to make finite positive and negative types use match and proj interchangeably. In theory, this should be possible. What happens in conversion is that
match x in prod _ with pair x y => b end = b[fst x, snd x],
for inductives with eta (Bi-Finite ones). PMP: we need a proof of concept and good arguments that it does not break the theory.
- Théo laid down the initial plan (we will have a CEP summarizing this soon). We want a reference manual that is close to an expert user manual, with the most exhaustive specs as possible. Also refactorings of the existing doc that are sorely needed. https://hol-theorem-prover.org/ for example splits into Tutorial (for beginners), Description (for users, quite close to our refman) and Reference (very exhaustive list of tactics). Emilio suggests maybe hiring a technical writer, Théo thinks it is a bit late to involve it for this project.
- Matthieu Sozeau
- Arthur Charguéraud (remotely)
- Jim Fehrle (remotely in the late afternoon sessions)
- Enrico Tassi
- Théo Zimmermann
- Karl Palmskog (remotely for some topics)
- Emilio J. Gallego Arias [not available Mon 16th 10:30--11:30]
- Hugo Herbelin
- Joseph Bakouny (on Tuesday 17th)
- Gaëtan Gilbert (remote)
- Anton Trunov (remote)
- Pierre-Marie (maybe remote)
- Vasily Pestun
- Maxime Dénès
- PUT YOUR NAME here, for security reasons we must provide Inria with the list of non-Inria participants BEFORE the working group
- is it possible to dump a state from coqc when reaching an error, to allow loading this state into the IDE instantaneously? (Arthur)
- mechanisms for loading hint data bases locally so that eauto use them by default (Arthur)
- features with implementation problems:
Letabstract
- Coq Platform
- development process: ownership, PR processing, topic branches`
- in particular how to improve merge speed? the assignee system is quite blocking in context of long-term efforts / refactoring
- some other large projects refuse to open the dev process due to these kind of issues
For the 16th: we'll use coq-working-group1@visio.inria.fr
For the 17th: "Visioconférence 10 (310#9136, visio.inria.fr)" siege-visioconference_10@zimbra-local.inria.fr (URI: 310@visio.inria.fr - PIN: 9136 - Tel: +33 4 92 38 77 88)
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.