Coq Call 2021 02 24

• February 24th, 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Coq Platform 2021.02.0 announcement.
• Dune update [see notes]

Notes

Coq Platform release

Current Non-features

• There is currently no open source package for CompCert 3.8 because the required changes in the Makefile have not been integrated. We need to discuss what to do about this.

• There is no Mac installer (ToDo)

• One might want to add MacPorts and Homebrew packages for Coq Platform

• There are a few remaining opam patch packages for Windows which I didn't get into the upstream repo (they do some hacks which wouldn't work on Windows if there would be a sandbox - since there isn't one on Windows I don't see the issue but the repo maintainer didn't like it anyway, although the existing package has a very severe bug). There is a new mechanism in opam to have opam switch local package config files which would allow to do this properly - or I sit down and create proper Cygwin packages (the relevant packages currently don't have a Cygwin maintainer). The status quo means one cannot create an opam package for Coq platform - at least not one which would work on Windows, but one could explicitly exclude this with a hint why.

Discussion of Non-features

• CompCert: no strong opinions

• Mac DMG installer / MacPorts / Homebrew package:

  • Théo: many students don't have MacPorts or Homebrew installed, so a DMG package is important
  • Théo: download numbers are high for the current DMG package
  • Théo: we currently have a DMG package, so not having one would be a regression
  • Michael: will priorize DMG installer over additional packages - this should be mentioned in the beta release annoucement
  • Michael: at first it will be a simple DMG package, e.g. no way to select individual packages

• Coq platform opam package:

  • Théo: using the scripts is preferable over an opam package, even for people already using opam, e.g. cause creation of a switch with a well defined name, ...
  • Conclusion: questionable if we should have a Coq Platform opam package at all - wait for user feedback

Options for releases

• do a 2021.02+beta release now
• do a 2021.02.0 release now
• do a 2021.02.0 release as soon as .DMG package is finished

Discussion:

• Enrico: snap package stream for 2021.02 already created, so there should be a release in February
• Michael: consensus from previous discussion: release should have DMG package
• Enrico: what were the rules for minor releases?
• Michael: adding new packages is OK, but the versions of existing packages should only change to fix critical bugs
• Michael: plan is to make minor releases about monthly after the first release adding new packages

Conclusion

• make a 2021.02+beta release today
• implement DMG
• make 2021.02.0 release as soon as DMG is ready
• beta release will be publicly announced
• Enrico drafts the announcement message and aligns with Michael via Email

Dune build system update

Immediate plans for Dune migration

The current plan for having Dune build the OCaml part of Coq was detailed:

• we first discussed the stale "Switch to a Dune-based build system" https://github.com/coq/coq/pull/8729 , which didn't proceed well. The PR has gone too stale and we shall close it, however Emilio thinks the original plan sound and would be have been a bit more pragmatic, we would have saved loads of time for everyone, not to mention bugs.

• first step in the is to merge the "Split stdlib" https://github.com/coq/coq/pull/12567 PR, which does ease containing the OCaml part to its own package, and among other advantages, much simplifies the build with Dune of only that part.

  The PR is mostly ready, there were some questions about the advantages of such split are, and if Coq works standalone. The split was requested by quite a few users, and its main advantage is modularity and flexibility in terms of Coq vs the Stdlib and other projects such as tactician, HoTT, or stdlib2.

• next step is to merge "Use Dune for OCaml" https://github.com/coq/coq/pull/13617, which provides a bridge to Dune, so only the .vo files are built. This allows to remove a lot of complex make build system logic; main user-visible change, is that the build objects are out of tree, plus the dependency on Dune.

• For 8.14, we should also remove the leftover makefile for the stdlib and use coq_makefile instead https://github.com/coq/coq/issues/13888

After-merge plans

Once the ML part is built using Dune, we can perform many other interesting things, in particular, we plan to:

• refactor all the code pertaining to loadpath handling to a coq.boot library which is shared by coqchk, coqc, coqdoc, coqnative, etc...
• add ocamlfind support for the linker, solving https://github.com/coq/coq/issues/7698
• improve configure script, make it a proper binary
• "Enable Native Compilation" https://github.com/coq/coq/pull/12974 , but we will likely wait for https://github.com/coq/coq/pull/13287 first, unless packagers want it in.
• test-suite: work is under progress https://github.com/coq/coq/pull/13364 , with a bit more effort we should be able to get it ready.

General comments

• Emilio notes that we all need to understand that things may not be perfect at first, but the effort will pay off.
• dune 3.0 is underway, it will improve dynamic rule generation and maybe provide a plugin API which would be very convenient for us