CoqWG 2019 10

Quick Links:

• Organization
• Participants
• Notes

Organization

The Coq Working Group was held Salle du Conseil (Bât 34, room 404), on Nantes Campus on October 1st and 2nd 2019, Google Maps. See the WG Page for information on all Coq Working Groups.

• Tuesday:

  9am-10am: Hacking session.

  Morning talk by Damiano Mazza at 10.30am, room ABC, ground floor of building 34. "Backpropagation in the Simply-Typed Lambda-Calculus with Linear Negation".

  11.30am-1.30pm: Lunch (in the WG room)

  Hugo won't be there on Tuesday. In the afternoon:

  • 8.10 update - Vincent (Notes), Matthieu (10min)

  • 8.11 plans - Pierre-Marie, Matthieu (30min)

  • needs:discussion PRs Each PR to be discussed should have a discussion leader present (who looks at the PR and can present it in advance): the goal is to come to a conclusion that allows removing the needs:discussion label at the end of a (set!) time. Add the PRs here so we can schedule. https://github.com/coq/coq/labels/needs%3A%20discussion

    • 10633 Ltac2 substitution - Pierre-Marie (??min)
    • 9897 Ignore the hidden boolean when comparing projections and fix micromega wrt projections - Vincent L (10 mn)
    • 10478 Remove "VARIABLE" object, Print All, Print Section, Inspect - Gaëtan (<15 min hopefully)
    • 8228 (Partially) Revert "Make Environ.globals abstract

  • SProp + UIP (Gaëtan, Pierre-Marie and Matthieu, hacking session)

  • Moving from template to full universe-polymorphism in the stdlib (Nicolas, Matthieu, anyone interested?, hacking session)

Diner supported by the WG funding as well: 7:30 pm at La Cigale

• Wednesday:

  10am:

  • Multiple universe hierarchies / handling sorts (Gaëtan, PMP, Matthieu, Hugo, design working group, 30min discussion, led by Matthieu)

    https://github.com/coq/coq/wiki/Multiple-Universe-Hierarchies

  • Reals (Vincent Semeria, Cyril and Kazuhiko remotely, maybe Bas remotely, discussion, 30min)

  • CI: tooling & allowed failures (Enrico, 20 minutes, mostly questions/requests for CI folks)

  12-2pm: Lunch

  • Coq Platform (Michael Soegtrop, 20min, remotely)

  • Coq opam repository (current status of packages and test system, Guillaume Claret, 5min)

    • test platform https://coq-bench.github.io/
    • Gitter channel for opam bugs https://gitter.im/coq/opam-bench-reports
    • by Erik Martin-Dorel: setup free CI for personal projects on GitHub: https://github.com/coq-community/docker-coq/wiki/CI-setup

  • CoqMT reloaded (Maxime, Matthieu, Nicolas, Bas?, P-Y will be there in Nantes, design/planning working group, ??min)

  • HoTT, Math-comp & Equations integration progress report (Andreas Lynge, Matthieu Sozeau, 10min)

  • Ltac2 ? Binding ? (Hugo and PMP, discussion, maybe PMP can remind us exactly what Ltac2's semantics related to binding are in ??min)

Participants

• Matthieu Sozeau
• Hugo Herbelin (Wed)
• Alexis Saurin
• Maxime Dénès
• Enrico Tassi (both arriving at noon Tuesday)
• Gaëtan Gilbert
• Assia Mahboubi
• Simon Boulier
• Vincent Semeria
• Nicolas Tabareau
• Pierre-Yves Strub
• Pierre-Marie Pédrot
• Cyril Cohen (remotely)
• Kazuhiko Sakaguchi (remotely)
• Yves Bertot (same as Maxime and Enrico)
• Vincent Laporte
• Andreas Lynge
• Michael Soegtrop (remotely, partly)
• Guillaume Claret
• ...

Notes (from Matthieu)

8.10

• Started in April
• Ready in May
• Beta in June (CoqIDE fixed on Windows)
• Beta2 in September (With template-poly fix)
• Should have released earlier!
• README.md updates of the dates / on github and the issue associated to the release Update the issue regularly / for communication with release managers. The release plan .md should be fixed and update

8.11

See https://github.com/coq/coq/wiki/Release-Plan---8.11

• vos, first version should get merged soon (cleanup of a patch of Emilio, Maxime is on it)

• Dune / Make issues (does not seem ready for 8.11, unless test-suite/refman issues get fixed soon)

• VSCoq toplevel and CoqIDE toplevel AND Coq/STM sync? Do we have the resources for maintaining CoqIDE w.r.t changes in the STM?

• UIP in SProp: still remains to check if vm/native can be updated

• Arrays: branch exists, but not the top priority of Maxime.

• Global env cleanup w.r.t. universes (seems top priority for 8.11 for Matthieu and Pierre-Marie)

• #9897: Have to plan this with Maxime, Pierre-Marie and Matthieu to give a proper solution to primitive projections.

Multiple universe hierarchies (Matthieu Sozeau)

See [Multiple Universe Hierarchies](Multiple Universe Hiearchies)

Reals (Vincent Semeria):

• classical reals easier to work with (Coquelicot-based)

• constructive reals locked in C-Corn, no classical communiccation

• 3 axioms: LPO, funext, excluded-middle of negation Move from constructive to classical reals. Constructive subset of classical.

  Questions: What are plans regarding libs?

  • mathcomp
  • stdlib
  • C-Corn

  Integration in stdlib of fast reals of Russell O'Connor 16000 LoC Or a separate library for fast reals?

  Arithmetic in Coq / Analysis outside ? Assia: Signature is strange ? Lower-bound/upper-bound axioms are strange.

  Dependent choice and funext is also a basis

  Question of Assia: how would the common basic spec of classical reals be phrased: record or set of axioms?

  Michael advocates for more things outside the library, because it's much less usable with the stdlib methods. Vincent agrees.

  Is it possible to have a common API? Differing views on the matter. Classical/constructive split makes different APIs? Assia: Classical does not mean non-computational. Maxime: the converse is true too.

  Vincent and Michael think it should be able to lift constructive results to classical reals, Maxime says so too. Pierre-Marie and Cyril point out that porting theorems from constructive to classical has its problems for education. Seems to be a contentious point. Guillaume points out that the arithmetic part is indeed translatable. But Cyril points out that for the more meaty analysis part it's not clear.

Coq Platform (Michael Soegtrop)

Sound/video recording available here for the whole afternoon: https://youtu.be/S2aRl0Axsbk

• Improvements for users:
  • installation easyness (e.g. for Summer Schools)
  • completeness

Beta releases for the platform, following releases with a 1-3month delay.

• Improvements for devs:

  • Easier development

• CI overhead:

  • can we move packages to the platform CI?
  • CI is inefficient w.r.t. dependencies

• Inclusion requests on github:

  • reasons given to add a given package
  • inclusion implies duties on the author
  • exclusion if lack of maintainer response

• Technically:

  • github repo
  • installer scripts
  • developer tools (Coq dev environment)
  • patch files for packages
  • discussions on issues

• Package description should be enough to derive opam packages

• CI issues:

  • sensitivity of PRs make the (almost) whole CI necessary.

opam packages and bench (Guillaume Claret)

• opam-bench working well and up-to update
• Some issues with Makefiles (might get solved when moving to dune)
• Karl Palmskog: test-CI, advertise it!
• We can investigate more servers to run the bench there.

Universe Polymorphism, HoTT & math-comp (Andreas Lynge)

• Many universes, currently working-around with monomorphizing
• Fixing elaboration to use less cumulativity Andreas & Matthieu together
• Main source of blowup: inductives and canonical structures.