Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[dune] Switch to a Dune-based build system.
Over the last months we have added support to build Coq with Dune, I feel we have reached a point where we can start to discuss if we should replace the make-based system with a Dune-based one. The *main rationale* for the switch is that maintaining two build systems is hard, and Dune seems superior to make in almost every aspect. Indeed, I think it is going to be hard to find technical arguments to defend the make-base system. Dune outperforms it on almost every possible metric. Additionally, the make-based system has grew organically over the years, and these days we are spending significant developer resources on it. The number of bugs that would be fixed by Dune is large [see coq#8052]. It is not a coincidence that few large projects do use `make` anymore, but most have moved to `CMake`, `Ninja`, or some other alternative. On this side, Dune provides a well-defined model that seems to git Coq's present and future necessities well. *Blockers*: the single blocker for a merge as of today, apart from the depending PRs, is the lack of native-compute support. This is due to a technical limitation wrt targets and can be solved in several different ways. Also, it is likely that a smooth developer profile is not possible until ocaml/dune#1155 lands in Dune itself. ocaml/dune#1377 may be convenient for the reference manual but we can have a small workaround to generate the install file for now. *Risk analysis*: it is important to understand the risks that such a move would entail. After Dune support is merged we could always go back to a make-based system, however we are very likely to depend on Dune-specific features that would be hard to replicate. The main risks are: - lock-in: indeed lock-in risk is significant and Coq's source code may depend on some Dune features. On the other hand, Dune is strongly poised to be the standard build tool for the OCaml platform and ecosystem, and more than 50% of OPAM packages use it. It is safe to say that if Dune would become unsupported in the future, there would be more important problems than Coq itself. - lack of in-house knowledge: indeed, Dune requires some specific training in order to understand its build rules, which may become a problem. This risk is mitigated in 2 different ways and attenuated by an additional consideration: first, Dune rules are fairly simple and declarative and it is reasonable to expect developers get to know them without too much effort. This is one of the reasons for the high adoption numbers in the ecosystem. Second, Dune developers are very reactive and care about Coq, thus it is safe to assume that we would get external help if needed. The additional consideration that may make this less of a problem is that our in-house knowledge of make may be even worse than Dune's. A non-negligible number of developers have expressed discomfort with make and the amount of required knowledge to master make seems way higher than what you need to use Dune. - lack of flexibility: indeed, Dune is way less flexible than make. Dune only knows how to do well two things: building OCaml executables and libraries. However, that is basically 99% of what building Coq entails; building other parts [documentation or Coq libraries] is fairly straightforward and seem to pose not a problem. - lack of maturity: indeed, Dune develops fast, it is not free of bugs, and some amount of adaptation is expected from us. This risk can only be mitigated if there is continued developer interest. In the worst case, Coq could become stuck in a particular Dune version. - bootstrapping: this is not a problem as witnessed by coq#8615, Dune can be bootstrapped very easily as it depends only on OCaml and it is designed to do so.
- Loading branch information
