Coq Call 2019 09 18
Notes from the Coq Call:
- Template poly is fixed in coqtop and beta-3 is out
- We accept to have still a known soundness vulnerability in the ML side and checker for template-poly, which would require a large API change of the environment (see PR #10616).
- We still must resolve #10298 about
notypeclasses refineand treatment of evars (@mattam82 is on it)
Vincent: working on stdlib2 and the basic infrastructure (issues with CS hierarchies and primitive projections)
- evar-conv primitives (?)
Working with Erik Martin-Dorel and Pierre Roux on primitive floats. Pretty confident about the axiomatisation (stress-tested already in Coquelicot/Flocq/CompCert) Now on coq-interval integration They should make it to 8.11
Working on documentation (cleanups and refactoring). Waiting on @Zimmi48 and @mattam82 to implement a larger plan of refactorization of the refman. Waiting on PR #10489 to be merged (dependent evars line) for more PRs to come depending on it
Working on notations and being pretty busy elsewhere
- Separation of parsing and exec (for proper document model handling in the future)
- VSCoq hacking: now maintained by @maximedenes, functionality ~ as good as coqide
- Responding to coq-consortium issues
- Gave a try to rebasing CoqMT, making use of the new "primitive" support. Some limitations (I don't remember exactly what that refers to) We should have a call with Pierre-Yves Strub & Bas Spitters who are also interested in this (and apparently Pierre-Yves would not do it the same way today, from what I understand)
- Import/Export bugs (2 months to fix the CI, maybe it's time to be more selective and move some developments out of the CI).
- ELPI in Coq (should have a usable release this year). Goal: write a (configurable) refiner for Coq purely in ELPI.
- Collaborating with Kazuiko and Cyril on higher-level structure/hierarchies specifications
- Collaborating with Maxime and Emilio on STM fixes and separation of execution/scheduling of tasks from parsing of documents. This should enable more incremental checking.
Emilio Gallego Arias:
- Working on cleaning declaration paths / making parsing more functional
At the level of the interpretation now (from parsing): #10365 on making
engine/use functional state Many more PRs by Emilio should follow on top of that. One idea is to use a different notion of global env for proofs (@mattam82 AFAIU).
- Proof API cleanup #10727, #10681 on making proof_entry abstract
- Discussion with Maxime and Enrico: Require Import requires parsing action of notations registration (@mattam82 is that the only side-effect?)
- Postponing more work on dune with @Zimmi48 to early november when Emilio is back from vacations. They will propose a new Coq library model at that point. In the meantime, should propose a PR to fix the blocking issue with test-suite building in dune (due mid-october). Then the Makefile-based system should be slated for removal.
- About Arthur's vos/voi/vok still some duplication of functionality but should be good to merge anyway after @maximedenes' cleanups.
- Working on cleaning declaration paths / making parsing more functional At the level of the interpretation now (from parsing): #10365 on making
- Presented mCoq a "mutation proving" framework. One goal is to make it run on users CIs, question of performance / integration with incremental checking and vos/vio infrastructure.
- UIP and SProp work #9779. Topic for the next WG (@maximedenes and @ppedrot are in)
- Fixing extraction bugs (in the simplifier/optimizer part in particular)
- Module extraction (@mattam82 ?)
- Discussion on relation to MetaCoq's erasure: we need to interface with Malfunction to link the verified MetaCoq erasure to OCaml code. Then we can compare with Coq's extracction.
- We need to set a time for PR discussion at the next WG in Nantes
- We decided to continue the short Coq calls, and put a notepad for topics to discuss. Next time (sept 25) we'll use visio.inria.fr (should be compatible with Inria's videoconference room infrastructure AND non-inria collaborators)