Coq Call 2021 09 01

• September 1st 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• turntable on ongoing topics, roadmaps updates (Matthieu, everyone)
• https://github.com/coq/coq/pull/13837
• Clean up of scheme generation, see https://github.com/coq/coq/pull/14740 (Ali Caglayan)

Notes (from Matthieu)

• Ongoing topics.

  • Hugo: focusing on usability issues esp for mathematics.
    • Section variable names (clearing etc...). Depends on functionalization of the environment.
    • Unification issues. Difficult to improve due to non-commutative heuristics. Heuristics apply sometimes outside the pattern fragment, being non-canonical. We parameterize unification so that it uses some non-canonical rules optionally.
  • PMP: dnets and hint databases cleanups. Side-effects in the kernel / functionalization. Problem with modifying the STM's handling on state.
  • Guillaume: still the same PR blockers. Dune ./configure -prefix etc. blockers https://github.com/coq/coq/issues/14468 https://github.com/coq/coq/issues/14232
  • Emilio:
    • refactoring of configure https://github.com/coq/coq/pull/14189
    • https://github.com/coq/coq/pull/12425 CI for windows. Removing worker for windows 64. Remember about the signing issue.
    • SERapi improvements
  • Enrico:
    • ELPI doc using Alectryon (improvements to it as well)
  • Maxime:
    • Back on VSCoq.
    • Nametab functionalization to separate parsing and execution. Requires handling the parsing extension of require Import separately from the whole execution.
  • Théo:
    • Ongoing: Coq Nix Toolbox
    • Upcoming: Survey preparation and roadmap.
  • Matthieu
    • Survey preparation and roadmap.
    • Typeclass-related PRs for 8.15
    • Working on MetaCoq proofs... for the new case representation.

• Scheme generation: Matthieu should have a look