Coq Call 2019 09 18 - coq/coq GitHub Wiki

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)