CoqWG20150915
The WG was held in Paris, on Sept. 15th.
Matej Košík, Maxime Dénès, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Pierre Courtieu, Julien Forest, Matthieu Sozeau, Yves Bertot, Enrico Tassi, Guillaume Melquiond, Hugo Herbelin, Pierre-Évariste Dagand
31 bugs considered critical for 8.5 beta 3
- Universes: 15 bugs
- Compilation issues: 4 bugs (2 of them related to native compute)
- Modules: 2 bugs
- Print Assumption: 2 bugs (Print Assumption forgets to tell you that some axiom was used)
- Coqchk: 2 bugs
- STM: 2 bugs
- Records: 1 bug
- Compatibility: 1 wish (considered bad idea by Guillaume Melquiond)
We lack manpower from experts of Modules, Print Assumptions, Coqchk
Hopefully, at the end of this day, we should have clarified what will become of most of these bugs.
What date are we targeting for a beta3? Matthieu is hoping the end of September.
Hugo: for the Universe bugs, do they all have the same origin?
- No, some of them are technical Ocaml stuff, but some of them are inconsistencies
- Greg Malecha is looking at one of the bugs at the interface of vm_compute and universes
- Building on the feedback that Yves got a few months ago, let's try to improve the development organization.
About shorter release cycles, is 6 months okay? Should we announce release dates very early?
Pierre Marie: changing the process on release, also means changing the process on branch management.
Do we still release PL for most serious bugs?
- Maxime advocates decorrelating what is in trunk from what is going to appear in the release, and make sure we have a lot of branches.
- The solution advocated is a lot of work for the person integrating the release.
- Enrico thinks that the integrator should actually be helped by the branch managers, so that most of the merge conflicts have already been studied by each of the branch managers.
This solution makes that when you merge there is less fear to merge wrong stuff, because you know it is still going into a draft.
Enrico thinks that people working on academic schedule would be ill at ease with releases every 6 months, because their schedule is more constrained by a year cycle.
Enrico: if we produce a release every 6 months, we have to expect that users are going to follow us. This depends on how much things we break at each release.
It is not clear whether users will prefer to have something that breaks often in small ways.
Use of the Jenkins platform works fairly well. There are random problems with the windows slave.
We can all start tests on Jenkins
Jean-Marc Notin is also working on a tool to display bench results. Maxime: it is realistic to make Jean-Marc's stuff work under Jenkins.
Future work is to design a good benchmark.
It is the case that all contribs are now available using the OPAM git repository. The one missing part is a good documentation.
Advertisement is missing. The Coq web-site still points to the old page.
Do we know if we still want to define a new tactic language
Maxime discussed about Ltac with Adam. Hugo thinks that Ltac can be kept as a legacy, but new things can still be designed.
The failure of Ltac is the fact that we don't have a clear semantics.
Pierre-Marie thinks that the problems of Ltac are fairly simple, they could be fixed easy, but the change would still be disruptive.
We should switch to a mode where people are invited to work with many tactic languages, instead of trying to have Ltac as the sole solution.
Maxime: this is a research problem, who is going to work on it? According to Hugo, there is Yann.
Enrico: if this is research then we cannot promise anything about it.
It is not written that Ltac cannot be supported.
There was a great talk by Matthieu at ICFP about the unification algorithm, and Matthieu says this algorithm is expected to become the single unification algorithm for Coq. Hugo reminds us that the integration of the current useful heuristics is still an open problem. The question is whether the strategy is documented enough for users to predict what is happening.
Enrico explains that he also had plans to embed in Coq a scripting language in which unification could be written, so that the algorithms would be easily extensible. So extensions could be local.
Maxime thinks that the most recent changes on unification by Hugo introduce more postponment, while the proposal by Matthieu et Beta has very little postponment.
Should the reals library be shipped separately. Guillaume has a question about the libraries. For compatibility between packages, it might still be useful to keep the axioms. Hugo thinks the main point is to advertise correctly where the libraries are. Trusted extended libraries.
HoTT: There are several people working on this. Something like Cubical sets
Extensionality: dependent programming, to make it work in practice. Human think of equality as being extensional, but the proof assistant only provides intensional. Pierre-Marie adds that we see a lot of work providing systematic proofs.
Verified kernel. The work on verified kernel should be continued, maybe by Maxime in his new job.
Reviewed the bugs blocking 8.5 https://coq.inria.fr/bugs/buglist.cgi?query_format=advanced&order=Importance&resolution=---&target_milestone=Next%20patch%20level
and the pull requests on github https://github.com/coq/coq/pulls
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.