Adding support for dune builds in coq-community projects

[palmskog]

The dune build system solves many problems with make and coq_makefile for Coq libraries and plugins, not least flaky plugin builds. The tooling around dune, such as dune-release also automates many tedious maintenance tasks, e.g., creation of OPAM files and submitting pull requests to OPAM repositories.

Dune support for Coq projects is still experimental, but is expected to stabilize during 2020. Dune is also expected to become the default build system for Coq itself for version 8.12.0 (tentatively planned for release in mid-2020). Possible future extensions to dune for Coq include support for handling extracted OCaml code and for running alternative checkers such as coqchk.

I believe Coq-community projects should start to add (optional, non-default) support for building with dune. This has the benefit of helping dune developers to find Coq-specific issues, preparing projects for the official dune support for Coq projects, and increasing automation for coq-community maintainers. For Coq plugin projects, there is already a tutorial for adding dune build support.

Finally, there is now also a section in the dune manual defining Coq-related build options.

[palmskog]

To the best of my knowledge, as of December 2019, dune support for Coq has the following limitations:

• lack of support for Coq native compilation
• no way to access the Coq version in dune build scripts (planned to be exposed as %{coq_version})
• due to build hygiene imposed by dune, all .vo files show up in a subdirectory and are thus not easily accessible by interfaces such as ProofGeneral (which looks at the _CoqProject file)

Consequently, we initially aim to use dune for batch/installation builds, e.g., in CI.

[palmskog]

@ejgallego for coq-community project releases that happen post Coq 8.12.0 which have dune support, do you see any reason against having the corresponding opam packages in the Coq opam archive use dune for building? (Assuming native compilation is not an issue.)

Moreover, do you currently recommend any specific bounds on the dune/language version? For example, is the following reasonable:

(lang dune 2.5)
(using coq 0.2)

[ejgallego]

Hi @palmskog , I think that would be a very interesting experiment; the bounds you propose are fine IMHO, however we still expect the Coq build language to evolve before the "1.0" release, so certainly maintainers should expect to have some churn. A few things that will change:

• we will support inter-project composition, that could have some implications we still ignore
• (include_subdirs ...) will be made per-lang [this will help extraction for example]
• helpers for Proof General, coqdoc, etc... will be added
• multiple bindings of the Coq dirpath will be supported [as outlined in our zulip discussion]
• native / quick should happen, however there are still some unknowns as to what is the best way to support that, for example recent Coq seem to have trouble with some particular combinations.
• some variables such as %{coq:config} should appear so it is easier for people to support different Coq versions.

Moreover, when we reach 1.0 , we will likely deprecate all other lang versions, and give like 3/5? releases for people to adapt.

On the other hand developments picking the dune + dune-release toolchain is essential as to get a good amount of feedback towards the 1.0 version of the language, so that effort would be really appreciated.

[Zimmi48]

@palmskog Should we close this as a duplicate of coq-community/templates#38 / solved issue?

[palmskog]

Unfortunately I consider this issue far from solved. For the longer term, I would really like to use dune everywhere in coq-community, including in all new packages for the Coq opam archive.

However, if we use Dune before 1.0, based on what Emilio says above, it seems we are setting ourselves up for future compatibility issues. coq_makefile will basically "always work", while a package using Dune 2.5 / Coq-0.2 may need its Dune version restricted in the future, or require patching. So my current stance is something like:

• do parallel Dune and coq_makefile support in all coq-community projects (not done yet)
• use coq_makefile in released packages until Dune Coq support reaches 1.0, then switch to Dune
• use Dune in dev opam packages
• use Dune in CI always

[rgrinberg]

some variables such as %{coq:config} should appear so it is easier for people to support different Coq versions.

Is conditional compilation something that is often used in Coq projects? We could add conditional compilation in the style of OCaml for Coq in dune.

[palmskog]

Is conditional compilation something that is often used in Coq projects? We could add conditional compilation in the style of OCaml for Coq in dune.

I think conditional compilation is currently underused because it's so hard to script for in build scripts - figuring out the current Coq version in a Makefile accurately is very hard. The most high-profile examples I can think of are CompCert and VST, whose releases were patched by Michael Soegtrop to work across several versions of Coq by manual patches, see some of this work in the Coq Platform.

[palmskog]

Based on the problems encountered by downstream maintainers when the Multinomials project switched to using Dune, in particular for opam releases (math-comp/multinomials#41), I think we should for the foreseeable future avoid requiring Dune for any project releases. In other words, as of fall 2021, Dune support in coq-community repos for CI and local developer use continues to be a good thing, but coq_makefile based build scripts should be retained whenever possible, with coq_makefile builds used in opam files for releases submitted to the Coq opam archive.

[Zimmi48]

But what to do for monorepos then (hydra-battles, topology...)?

[palmskog]

Well, this is why I added the qualification "whenever possible", which should be read as "we continue to use Dune for releases where coq_makefile is practically infeasible". Also, both hydra-battles and topology are projects with seemingly no current downstream users.

[strub]

@palmskog Do you have an example of a project that uses both system (dune for the dev & coq_makefile for opam)?

[palmskog]

@strub here are some examples, we have a lot of these in coq-community now (I use this approach for nearly all the projects I maintain):

• https://github.com/coq-community/reglang (Dune in CI and used by me, Christian still uses make)
• https://github.com/coq-community/huffman
• https://github.com/coq-community/aac-tactics
• https://github.com/coq-community/sudoku (js_of_ocaml extraction and compilation both using make and Dune)

[strub]

Ok, I'll take the first and use it as a template.

[Zimmi48]

IINM, all these examples use Dune in the .opam files committed in the repository, so this means that there will be a temporary desynchronization between that and the opam-coq-archive repo.

[palmskog]

Well, there is desynchronization between opam files for releases and the opam files in the repos (the former use coq_makefile and latter use Dune). I still have the repo opam file in synch with the extra-dev opam file in the Coq opam archive.

[palmskog]

An updated summary of how I view Dune use in Coq-community after the release of the 0.8 lang version with composition with theories installed in Coq's user-contrib ("Dune-Coq 0.8" vs. the old "Dune-Coq 0.3"):

On one hand, Dune-Coq 0.8 enables using Dune in the same way inside opam packages and locally - user-contrib is "just" another place where .vo files can reside. On the other hand, Dune-Coq 0.8 forces declaration of Coq logical path prefixes of all transitive dependencies, as in the following example:

• opam package coq-foo depends on package coq-bar (path prefix Bar) which depends on coq-quux (path prefix Quux)
• coq-foo content does not depend on Quux, i.e., has no From Quux Require Import ... or similar
  • coq-foo needs to have (theories Bar Quux) in its dune file

This requirement of specifying transitive dependencies can easily lead to breakages if used in released packages, for example:

• coq-bar does a new release that doesn't depend on coq-quux/Quux, but leaves everything that coq-foo depends on the same
• coq-foo breaks for all new opam installs since Quux via coq-quux doesn't get installed, and (theories Bar Quux) forces it to be present

Due to the possibility and likelihood of such breakages, I don't think Dune-Coq 0.8 should be used by any Coq-community project release, i.e., as a build system used in an opam package based on a release archive. Using Dune-Coq 0.8 in CI is still fine, if maintainers are willing to update their project's (theories ...) every time a transitive dependency changes.

Projects that use Dune for monorepo packaging (several dune files in subdirectories) should stay on Dune-Coq 0.3 as long as possible (Dune maintainers have deprecated Dune-Coq 0.3).

[ejgallego]

Thanks for analysis @palmskog ; we will implement implicit transitive theory deps for 0.9.

I'd like to note however that implicit transitive dependencies are not inmune to breakage, they suffer the dual problem: injection of ghost dependencies. So your project depends on foo, which pulls library bar. Then foo decides not to depend on bar, your project fails to build as you didn't declare the dep.

That's possible to address with some linting "warning, shadow dep detected", but tricky (hint hint, let's write a paper folks)

IMHO experience in the OCaml world suggest we should be cautiuous as to assert what kind of breakage is more common, the data is unclear, def we have seen both kinds.

But in principle I agree that caution must be used with the current default, tho I think there are many other multi-package cases where the deps are under total control of the maintainers, so IMHO in these cases testing could help a ot the projects.

I think the way this kind of issues are handled are similar tho: when the CI fails, a version bound is added prior to the merge of the new package.

[palmskog]

@ejgallego I'm aware of the ghost dependency problem, and have addressed it recently in several MathComp-related packages (that now should depend directly on Hierarchy Builder). However, in my experience the ghost dependency ("underdependency") problem is less serious in practice than "overdepending" and requires less manual intervention

[ejgallego]

However, in my experience the ghost dependency "underdependency" problem is less serious than "overdepending" and requires less manual intervention.

Interesting, how it is more serious / requires more intervertion, do you have an example?

I can see how it can be more common if we assume that packages grow their deps in general, which is not actually a trivial assumption, but reasonable.

[palmskog]

Interesting, how it is more serious / requires more intervertion, do you have an example?

In Coq-community, we have seen underdependency issues related to MathComp, e.g., a package only depending on coq-mathcomp-algebra when it should also depend on coq-mathcomp-fingroup. However, if this becomes a problem, we just add in the missing dependency into the package definition. In the scenario with coq-foo/coq-bar/coq-quux, the only way to fix the situation is to (1) conditionally patch the sources of coq-foo or (2) add a dependency to the new coq-bar package or to the coq-foo package that it doesn't need. Both are in my view invasive.

[ejgallego]

In Coq-community, we have seen underdependency issues related to MathComp, e.g., a package only depending on coq-mathcomp-algebra when it should also depend on coq-mathcomp-fingroup.

I'm not sure I follow, coq-mathcomp-algebra pulls coq-mathcomp-fingroup, so why did the package had to add this dep?

[ejgallego]

If you mean the other case, I'm afraid you'd have to patch the source code too, if algebra drop the dep on fingroup dune, even if it has transitive deps, won't register that dep.

But you make an excellent point about package / build definitions being redudant (and that's in the way to be fixed I understand)

[palmskog]

But let's say that my package, coq-baz, depends only on coq-mathcomp-algebra at opam level, but at From X Require Y level, it also depends on coq-mathcomp-fingroup. If coq-mathcomp-algebra drops the dep on coq-mathcomp-fingroup, then coq-baz breaks because the coq-mathcomp-fingroup dep is still needed. However, all I'd need to do is edit the coq-baz package definition to include coq-mathcomp-fingroup and it should build again.

[ejgallego]

However, all I'd need to do is edit the coq-baz package definition to include coq-mathcomp-fingroup and it should build again.

Not in the Dune model, right? You'd need to update the dune file too.

Thanks for the examples because this is the only way I can check if things do work.

We have 4 cases indeed:

• Case 1: library depends on field, and group is added implicity, then field drops the dep.
  • Case 1.A: No implicit deps at the dune level: You need to fix only opam
  • Case 1.B: Implicit deps at the dune level: You need to fix both opam and dune files
• Case 2: field doesn't depend on group, then it adds the dep to group
  • Case 2.A: No implicit deps: update to 2 files
  • Case 2.B: Implicit deps: update only to opam

So indeed the problems are dual, so what the best default is depends a lot on the dynamic behavior of the deps over time.