Coq Call 2019 09 18

Notes from the Coq Call:

8.10 (@vbgl)

• 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 refine and treatment of evars (@mattam82 is on it)

Roundtable

• Vincent: working on stdlib2 and the basic infrastructure (issues with CS hierarchies and primitive projections)

  • evar-conv primitives (?)

• Guillaume:

  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

• Jim Fehrle:

  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

• Hugo Herbelin:

  Working on notations and being pretty busy elsewhere

• Maxime Dénès:

  • 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).

• Enrico Tassi:

  • 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.

Karl Palmskog:

• 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.

Gaëtan Gilbert:

• UIP and SProp work #9779. Topic for the next WG (@maximedenes and @ppedrot are in)

Kazuhiko:

• 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.

Discussion:

• 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)