What do you think about replacing the current system of coq_makefile with a custom Coq build tool? Many languages rely on their own compiler to manage dependencies for builds rather than using make for this purpose (eg, Rust, Go, Haskell, OCaml’s ocamlbuild).
make solves the problem of building things in dependency order, but little else (for example, it can’t discover dependencies dynamically and cannot encode a dependency on the Coq version). Using it requires a complex program to put everything into a Makefile, which is a complex intermediate language.
I think a custom tool would liberate Coq projects from the awkward structure of what auto-generated Makefiles can do, for example treating the Coq version and set of flags as dependencies. I think we’d also have an easier time making sure the system is correct (makefiles are extremely difficult to debug) and adding features (such as better support for incorporating extraction into the build, or the recent effort to support a new signatures-only format to replace vio files).
While the tool there is functional, a new tree implementing some improvements is almost ready and I shall post an update ASAP, I just need to find a few hours to work on it, but I am a bit constrained as of lately.
That looks like a great step in the right direction, but I’m not familiar enough with dune to understand what constraints it imposes vs the benefits.
I’m rather wary of co-opting OCaml tools for Coq. The use of opam for Coq has been incredibly buggy and frustrating to me; opam had a bug in the fish support which broke the shell for years which has scared me from relying on it (the move to opam 2 may make things better, but that migration has been scarily slow). Ultimately I’m not sure that these tools will be maintained for Coq’s use case.
How would dependencies on external libraries work in dune? Would we get versioned dependencies on Coq opam packages, which are built standalone against a fixed version of Coq and shared among multiple projects? Rust’s cargo has all of these features in a sane way. Coq does have the extra burden of needing a _CoqProject so that editors can find all the dependencies - will dune handle that as well? Even without dependencies, warning configuration should probably be propagated to editors via _CoqProject. Is dune flexible enough to make Coq warnings expressed in a custom syntax within the stanza? What about integration with Coq so warnings are checked to actually exist?
What about depending on a version of Coq itself? Will we finally be able to seamlessly support local builds against multiple Coq versions (this requires an output directory of *.vo files per Coq version)? Compatibility across Coq versions is hard for other reasons in Coq (particularly the lack of conditional compilation), but this would bring things one step closer.
This is a lot of questions, so feel free to respond to any subset of them. I just want to encourage some discussion so this feature is more likely to address my use cases. Currently I’ve abandoned coq_makefile in favor of a custom solution, and it makes me sad to not re-use the Coq devs effort, and to be using make at all. I’m totally willing to write a build system just for own internal use, and it would be a bonus if the Coq developers were on board with that plan.
I am not sure what to say, as the effort of Dune + Coq has been already the subject of a few thousand messages.
All that I can say is that I am not fan of coq_makefile, but it is an instance of “rolling your own build system”; indeed, I think you underestimate the difficulty of writing a build system. At the very least, it ranges from a large to a huge effort, for sure in Coq we don’t want to roll our own.
Dune has a few unique characteristics, and in particular it may get Cargo-like support for dependencies, but that’s a complicated matter tho. You can get an idea of what’s going on by peeking on Dune’s githubs repos.
Well that’s an interesting deduction, however I wonder on what it is based tho, and above all how a custom tool may be better maintained with less manpower available than a more general, widely used one.
That’s cool, however note that development discussion [at least for the Dune efforts] will keep happening in GitHub / Discord / Slack [that’s already too many channels]
I am personally not on board, but I am talking for myself of course, maybe some other people is interested. Dune provides some excellent technical foundations which are very well suited for Coq IMO, so that’s the way I’ll go.
Note that in order to build Coq libraries you need to know how to build OCaml libraries; that gets ugly quickly.
That seems fair, thanks for the perspective. I’m absolutely on board with using dune to build Coq itself - that Makefile was an even more complicated custom build system than coq_makefile from what I could tell. However, until you mentioned it I was not aware that the Coq developers intended to move from coq_makefile to dune for building Coq developments themselves. I actually rather support such a move; the need to support plugins is a persuasive reason to use an OCaml build system, and dune is easier to program than make.
For now I think dune actually solves my dependency problem, since we’re just including dependencies as git submodules and it looks like dune was intended for this use case. However, from what I can tell dune relies on opam for managing globally-installed dependencies and solving version constraints, so we’d still have to adopt opam to get globally installed and shared packages.
That information is a bit outdated in a sense. The ocamlbuild tool was a very nice tool but it never managed to be good enough to be the universal OCaml build system. This is now the Dune era and it is taking over the whole ecosystem at an insanely high speed (for very good reasons).
Don’t be afraid. First, I’d argue that using opam for Coq was still a good decision, even if I’m not even personally an opam user, and if it had shortcomings. To be fair, you need to compare it to what the situation was before. Second, there are good reasons to think that the issues with opam are not going to be repeated with Dune (and are even incrementally being solved in opam). There is a very good communication with the team behind Dune, and they do take much more care in providing a reliable tool, that works well on all platforms, etc. And even if opam was a pain in the beginning, the situation has much improved since opam 2. And compare it to the atrocity that cabal was (at least a few years back, I haven’t used it for close to five years). At that time, opam was still good enough, in comparison. The not-invented-here illness has led to a vast collection of broken package managers. It is much more efficient to reuse existing tools and bring manpower to upstream to make them better.
BTW, I’d recommend you to give a chance to opam 2. If you are not happy with it or want to try something else other interesting solutions are esy https://esy.sh/ (which leverages the opam ecosystem), and Nix Nix & NixOS | Reproducible builds and deployments (which is a universal package manager, with its own package repository, which already contains a lot of OCaml and Coq packages).
The Dune team is super interested in the Coq use case, and Coq has been a great source of feedback for them since the beginning. The Coq support will be first-class and the Dune authors are going to help maintain it ([meta] coq/build-maintainers team · Issue #9747 · coq/coq · GitHub).
Two things:
The _CoqProject file has nothing to do with finding dependencies. If you are using it that way (e.g. with several -R or -Q), then you are using it wrong (telling Coq where to find dependencies is the job of COQPATH). The only -R or (better) -Q flag that _CoqProject must contain is the one corresponding to the namespace of the project you are currently building. It also has to do with listing other flags that are to be passed to coqc. I may be exagerating a bit here, in the sense that passing several -R or -Q file does actually work but this is not the normal workflow. With Dune, finding dependencies is very well handled, whether they are installed globally, or they are vendored (i.e. copied in a sub-directory).
The _CoqProject file could very well be generated by Dune like it already generates .merlin files. IIUC this won’t be the case in the very first version but it could be added pretty quickly. I hope this will be the case. Nonetheless, the move to Dune (and the work towards supporting LSP at the same time) is an opportunity to reconsider the _CoqProject format, and maybe support better other Coq flags (currently the way of setting warnings in _CoqProject that is compatible with both PG and CoqIDE is to use twice the -arg generic flag, as in Addressing Coq warnings · coq-community/manifesto Wiki · GitHub). This can also be an opportunity to design a general mechanism for setting project-wide options and flags Project level option system · Issue #9295 · coq/coq · GitHub.
It’s flexible enough for OCaml warnings so there is no reason why this shouldn’t be the case for Coq.
Yes. Note that Dune builds are already hygienic and support multiple profiles. The scenario of building with several versions of the OCaml compiler is already natively supported in Dune, but this depends on opam for getting the various versions for now. Adapting it to Coq should be easy (especially with OPAM: try out coq as a compiler · Issue #595 · coq/opam · GitHub).
My general feeling about this is that it’s a bad idea. Dune has received careful design and much manpower. As Emilio said, a build system is not something that you can quickly hack (if your ambition is to be better than make of course).
I don’t think the idea is “to move” in the sense that coq_makefile should remain supported for a long time I think.
Note that Dune doesn’t have an intrinsic dependency on OPAM, even if as of today it is a fact that you need to use it; but Dune is fairly package-manager agnostic and you can have Dune run today without OPAM at all.
It is quite pleasant to program with their API. That PR provides quite small functionality [as it touches the core so it needs careful review], but PRs implementing functionality until completing the build of the stdlib are ready to get in once this one does.
The main remaining question is what should the Coq library model be? Indeed, this is still not clear to me, but I will open a Github issue so we can all discuss.
The main support for building Coq libraries and plugins is already in Dune master, I am still not calling for beta testers as I think I’ll enable vendoring before I ask for wider feedback, but feel free to use in your projects / report back.
What do you mean by a compositional build? We currently include dependencies as git submodules and build them as if they were part of the project, using a -R directive to put them in the right module path; dune almost wouldn’t have to know about any of this, other than our -R flags.
In any case I’m working towards a deadline so I’ll start exploring this in a couple weeks.
Let’s say that you have two projects A and B. B contains an exact copy of A (e.g. using a git submodule). Projects A and B are both built using Dune (or at least they both support this build method). It means that they both contain a dune file (possibly in their theories/ sub-directory if such a sub-directory exists) and a dune-project and a (possibly fake) name.opam file at the root of the project. This name.opam file can be empty but is used by Dune to mark the root of the project “name”.
A compositional build would mean that Dune can detect that B’s dependency A is present in the tree and can be built from there. This is not supported for Coq in the version of Dune that was just released but should come soon.
The model where you build A as if it was just part of B doesn’t work with Dune unless you can modify the Dune files in A (and thus it is not anymore an exact copy). You would need to:
remove a.opam and dune-project;
change something like (public_name a.A) into (public_name b.A).
Indeed, thanks @Zimmi48 for the explanations; using -R or -Q in Dune will become an error, the whole point of Dune is to allow it to manage dependencies so users shouldn’t have to care about low-level flags.
So in your case @tchajed you would just add to your (coq.theory ...) stanza (theories foo.bar moo.meow) and all the magic should be done for you.
The PR for compositional buils has been submitted https://github.com/ocaml/dune/pull/2053 , but it is still in a bit of a flux, so I recommend it only to people that is willing to live on the edge.