Hi all, I am opening this topic for the "user-side" discussion related to the PR https://github.com/coq/coq/pull/13617 , which will switch the build system of Coq OCaml's parts to Dune https://github.com/ocaml/dune
Dune is a much more capable tool than our current make-based build system, but indeed there will be some changes to the workflow, most of them for the best. The main significant change is that all build objects are now placed under _build
, so those looking for the binaries may need to update the location; moreover, some other common workflows in the make-based system such as byte-only compilation are handled differently depending what your goals are.
Please don't hesitate to ask questions, and read the documentation at: https://github.com/coq/coq/blob/master/dev/doc/build-system.dune.md
There is some kind of an aura that dune is "complicated"; this is not my experience, it is different to make indeed, but once you get used to the workflow, it just doesn't get in your way, you press a key, the build happens, usually fast, and many of the worries you need to take care in make are gone.
So you wrote in https://github.com/coq/coq/pull/8729 that it was a huge failure, can we get some more information on this?
@Ali Caglayan yeah the transition got stuck and required 2 orders of magnitude more effort than planned, I'm convinced we could have adopted a much easier plan there, but we did many mistakes; turns out the problem we did face are pretty common c.f. https://www.listennotes.com/podcasts/signals-and-threads/build-systems-with-andrey-4Ttsi2KV51l/
Anyways we are pretty close to do a super large step soon, @Gaëtan Gilbert @Théo Zimmermann , it'd be great if we could process https://github.com/coq/coq/pull/13617 , would you be interested in being assignees?
Sorry, I didn't see the update until your ping (my GitHub notification inbox is pretty full). I can be the assignee (I'm definitely interested!), although if @Gaëtan Gilbert is available he might be a more competent one.
Great, thanks a lot @Théo Zimmermann !
Main issue seems documentation, I will do a pass soon, but it seems people is confused about using make
vs make -f Makefile.dune
which are indeed two incompatible paths for now. I'd like to make the make -f Makefile.dune
the default once coqnative
+ Dune 2.9 is released [as Dune 2.9 will include support for coqnative, coqdoc, and dune coqtop
replacing the shims] , but that may take a while.
I wonder what would the best way be to document this distinction.
Is there any way to make the two "compatible" by, e.g., using a different profile?
That is likely to never work well, IMHO you wanna make a choice to work with one build system or the other
To make them compatible the make-based system would have to learn quite a bit about profiles, dependencies on envars, ocaml compiler, etc...
Seems like a lot of work for little gain IMHO.
The thing is that the current make system always builds without opaque, this is very slow for native objects as modules do depend on implementations as they don't use opaque, and this is not semantic preserverving for example w.r.t. inlining
So the idea of the PR is that if you type make
you get a build like before, without opaque
which is ready to install
OK
IMHO this can always be refined later based on experience and feedback.
Let's hear from @Guillaume Melquiond
we could indeed add the notion of profiles to make so we have make dev
and make release
, at this point you will get sharing of object files but not fully guaranteed in some cases such as when you are instrumenting etc...
Emilio Jesús Gallego Arias said:
So the idea of the PR is that if you type
make
you get a build like before, without opaque
how does that work wrt the plan of switching to Makefile.dune by default?
@Gaëtan Gilbert makefile.dune doesn't profile a make install
target so indeed it is documented that if you need to install you need to do make release
make -f Makefile.dune help-install
tries to provide an overview
We can have configure generate the profile name if you think it is useful, I'm not so sure tho
@Théo Zimmermann I have done another pass, it seems like I broke something silly in Nix but the rest is looking good, and I've fixed some more bugs.
I'll have a look.
Merci Théo ! I will be around to discuss needed changes [except from 17-18h] , I am citing @Guillaume Melquiond too so we can discuss his concerns [I cited him a few days ago but likely notification got lost] , I'd like to understand them better.
Hey @Emilio Jesús Gallego Arias, I'm replying to a student and I'll be there.
Hey @Emilio Jesús Gallego Arias, I'm back.
So, it seems clear that there are two main use cases for the build system(s):
For the first group, it is good to keep supporting ./configure -prefix /foo && make && make install
.
For the second group, it is clear that Dune brings benefits and there should be only one recommended build method.
Keeping ./configure -local
or ./configure -profile devel
around without binding it to the new (and recommended) build method would send the wrong signal, and would lead some contributors to use a build method less suited for day-to-day development.
So it seems reasonable to keep -profile devel
(while maybe removing -local
) but to make it automatically rely on the dev Dune profile.
Furthermore, regarding the documentation targets, Dune doesn't bring many benefits there. Especially as it has some limitations regarding where targets can be located (which means that I could never provide as good a support in Dune than in make for the doc_gram targets).
So what I would really appreciate after this PR, would be to be able to just run make doc_gram
or make doc/tools/docgram/fullGrammar
and for it to work while keeping the benefits of the dev Dune profile.
I don't mind if I have to explicitly call ./configure
first.
Especially given that these are developer-only targets, and that we would like to generalize their use soon.
Thanks for the write up @Théo Zimmermann , what do you specifically mean by "keeping the benefits of the dev Dune profile"?
By the way, it should be possible to much improve the doc_gram, only thing preventing me from doing so is time
I mean, I would appreciate to having to go back to the build system that is unfit for development so that I can run these doc_gram
targets.
I see
Emilio Jesús Gallego Arias said:
By the way, it should be possible to much improve the doc_gram, only thing preventing me from doing so is time
Sure, but this is a bit of a side-question here, since it already works correctly as of today.
So if it works fine, why you have to go back?
Oh, I think we are misunderstanding each other here. I meant the legacy makefile targets work fine.
Not the Dune ones in this case.
Ok, so fixing the dune case would actually solve your problem?
I mean, we could add a switch for the profile [that's fine], however you still would be using the make-base setup for the vo files
I see.
so we would solve little, other than making the switch between the two systems a bit more seamless
Well, I guess it's already worth doing.
so indeed I will add the dune profile as configure variable
but you still have the problem then
Emilio Jesús Gallego Arias said:
Ok, so fixing the dune case would actually solve your problem?
This would be great but after having a close look at these, I don't believe it's doable.
Why not?
Because the targets that you need to promote are all over the place (all the rst files in multiple subdirectories of doc/sphinx).
So currently, what works properly is the promoting of fullGrammar
and orderedGrammar
.
We can use a little script + subdir to achieve that
(You have to call the Dune target twice though, which is a bit annoying but not a real issue.)
Emilio Jesús Gallego Arias said:
We can use a little script + subdir to achieve that
Oh, but then the script would live outside Dune, wouldn't it?
https://github.com/ocaml/dune/blob/main/plugin/jbuild_plugin.mli
Would live in a dune file but using the jbuild_plugin
module
likely some mangling would be needed, I need to look at the tool more closely
Dune 3.0 will have a much better workflow for this as you can have rules generate dune
files
this, + (subdir ..)
should suffice for a lot of cases
Yes
not the cleanest thing, but is is the way many other systems work
there is also discussion about having a true programming language in the configuration of dune
I don't like it too much, but your use case seems simple enough as to be OK
so, looking at the makefile.doc
indeed
what are the targets that are not declared?
already that code in makefile seems pretty broken IIUC
in the sense of the dependency graph to be sound
What do you mean?
Anyway, just to further clarify, my original idea was that depending on the selected profile, make
would build with Dune all the way (including the theories) or not.
I mean that calling doc_gram seems to produce a lot of files
however these files are not declared in the make rules
Anyway, just to further clarify, my original idea was that depending on the selected profile, make would build with Dune all the way (including the theories) or not.
I'm afraid this cannot work well, first dune doesn't even require calling configure, and the build systems are just too different IMHO as to do like that.
And I'd rather avoid the top-level makefile depending on configure-generated values
Emilio Jesús Gallego Arias said:
however these files are not declared in the make rules
That's correct, but I think that's on purpose: the rst
files are updated by these targets but so far calling this is optional.
After looking at doc_gram, I'm afraid that tool is gonna be very hard to maintain :(
2000 lines of ocaml code and not a single comment....
This is irrelevant to the current discussion, isn't it?
Even if we had to delete that tool at some point, it would already have helped make the documentation better.
It's not like it was an actual part of Coq.
Well, a whole lot of work is now blocked on trying to udnerstand the tool
I have been looking at it for 30 mins and still can't understand a single thing of what it does
:(
I can't even make sense of the makefile rules
Why don't you ask me? I know what it does.
And my requests are in no way blocking BTW.
How many calls to the tool happen?
Two ?
And my requests are in no way blocking BTW.
we should fix all use cases, otherwise we will never end the migration
right
First call already works in dune, right?
so second call is just to update the files?
so we need to add a rule for patching mlg files?
one quick way to do this is to add one rule per mlg file
not the best, however it is easy
mlg files are never modified by the tool
did you mean rst files?
sorry, rst
yes I mean that sorry
OK
so in the make setup, the tool was intended to be called only once
even if it has multiple phases
it has different options to stop at one given phase
but we could also change it to perform the different phases independently if that would help
So the first phase is to generate fullGrammar
from the mlg
files.
It works fine in Dune.
The second phase is to generate an editedGrammar
that we decided not to commit in the repo but I think it still generates the file.
This phase takes the fullGrammar
and the common.edit_mlg
files as input.
The third phase is more tricky: it takes the editedGrammar
file and the preexisting orderedGrammar
file and modify the orderedGrammar
file with the new / edited rules, while using the orderedGrammar
file as a reference for the order (orderedGrammar
and editedGrammar
being otherwise identical).
The last phase copies the relevant chunks into the rst
files.
Currently, the dune rule does the full thing, but it only promotes the fullGrammar
and orderedGrammar
files.
However, if you do a cp -R _build/default/doc/sphinx doc/sphinx
, you get the edits to the rst
files as well.
I see thanks
I guess we need to let dune know about the patching, how tricky is this going to be I don't know
A bit of the problem seems indeed that the tool could be a bit more modular
but indeed that's the classical tradeoff on whether to put file logic
in the build system or in the app
One question @Théo Zimmermann , so if you add to Makefile.dune
:
docgram:
dune build @docgram
rsync $BCONTEXT/doc/sphinx doc/sphinx
would you get a working env?
Yes, something like that should work. Although you still get the inconvenience of having to re-run the target twice (or even three times actually) if fullGrammar
has changed. And Makefile.doc
provides additional targets.
I see; I suggest we open an issue to summarize this discussion; AFAICS there is not real reason we cannot support this kind of patching in Dune, tho it may require some changes to the tool.
The current state of the PR tho makes possible to call make docgram
from the dune build without issues anymore, so IMHO that is good for now
Yep, this is perfect. (Though, I still need to test it by myself.)
It seems to me the PR is looking good, tho we can still apply a few optimizations, IMO most concerns raised have been addressed. My testing of docgram looked fine. Note that even for the pure dune build, after looking at the trace we can indeed improve build times for about 20 secs [I have a PR for dune that does this]
I'm ccing @Guillaume Melquiond again here to be sure all his comments have been properly handled.
IMHO it'd be good to consider the merge date then, so we can move forward with a few other things, most importantly coq.boot PR that will solve some important bugs, and coqnative which can use coq.boot too.
Of the plan we discussed for 8.14, then only feature I don't see on schedule is the one to use findlib for loading plugins, the PR works fine for loading already built things, however when building mixed ML / Coq code, the META for the ML code is properly setup so I need to think a bit more how to best solve this, it could involve using Dune's sites support so that would complicate things.
ping @Théo Zimmermann ; IMVHO we have given enough time for comments, we should move forward with this as it is likely there will be some issues, but next week I should be available so I can help solving them.
Agreed. I was just lacking time to do a proper review (I started one yesterday though).
Oh, thanks a lot!
Ok, I did another revision, there were quite a few bugs remaining in the bridge, but my understanding of make improved so IMHO it looks quite better; HoTT overlay should not be needed anymore, only impact is the coq.META -> coq-core.META
change, IMHO it is OK to do it.
There was indeed a problem in the bridge, some deps were missing, when adding these deps we got some rebuilds, actually that is because we need to weaken dune build foo
to dune build foo + touch foo
, otherwise make will get confused, as dune may decide foo doesn't need rebulid [no changes in hash] however make may [changes in mtime]
This topic was moved by Théo Zimmermann to #coqbot devs & users > CI minimization feedback
Ok @Théo Zimmermann , I have implemented what you suggested w.r.t. the overlays, maybe it'd be good to send a quick message to coq-dev before merging. I have further work that simplifies the setup (IMHO) quite a bit, for example I have realized that the best structure for _bulid_vo
is actually one that mirrors the installation layout such as the one in _build/install/default
when in Dune.
This is implemented in the -local
deprecation PR, but after that we can remove quite a few conditionals everywhere [only difference is that either you have _build for a pure dune build, or _build_vo for one with coq_makefile + dune]
cc: @Gaëtan Gilbert
Seems the biggest problem users are having is the confusion about the two build setups being exclusive. How could we really make an XOR here?
It is not possible to support this, except for a few controlled cases [like test-suite, or doc_gram which I'm willing to support to be called from Makefile.dune]
We could add some checks, but it feels sad that we have to do an anti-cleanup.
The migration to dune broke my build script; I'm now getting
make[2]: Leaving directory '/<<BUILDDIR>>/coq-8.master~git~202104280013+22250-0~daily342'
/usr/bin/make DOC_TARGETS=doc/stdlib/html/index.html doc/stdlib/html/index.html
make[2]: Entering directory '/<<BUILDDIR>>/coq-8.master~git~202104280013+22250-0~daily342'
/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build doc/stdlib/html/index.html
make[3]: Entering directory '/<<BUILDDIR>>/coq-8.master~git~202104280013+22250-0~daily342'
flock .dune.lock dune build --display quiet --profile=release @all-src
Error: no rule to make target doc/stdlib/html/index.html (or missing .PHONY)
Is this a bug? How should I fix this?
Full log at https://launchpadlibrarian.net/535843303/buildlog_ubuntu-focal-amd64.coq_8.master~git~202104280013+22250-0~daily342-f38ecc3323~ubuntu20.04.1_BUILDING.txt.gz
The top-level invocation is make DOC_TARGETS=doc/stdlib/html/index.html doc/stdlib/html/index.html
This way of building the doc predates my changes to the packaging script, so I'm not sure why things are done this way, but I'd like the equivalent invocation for https://github.com/JasonGross/coq-packaging/blob/bb9e33fd7a3c69d560b8576fd8582c7c94175fde/debian/rules#L60
@Jason Gross As for any make target which is a compilation output, you can keep using it as long as you prepend it with _build/default/install/
I think.
Théo Zimmermann said:
Jason Gross As for any make target which is a compilation output, you can keep using it as long as you prepend it with
_build/default/install/
I think.
no
vo files are in lib/coq for instance
and also telling dune to build install/.../foo.vo won't put foo's dependencies in the install tree
The Windows64 job seems to be failing everywhere now with:
34 Error: Don't know how to build _build/install/default/bin/coqchk
which sounds vaguely related to the Dune PR even though this very job had passed in the PR's CI.
I've also seen a case of:
Error: The following <package>.install are missing:
- _build/default/nix-build-dune-2.8.2.drv-0/dune-2.8.2/dune.install
that seems vaguely related too, in a Nix job.
Ah, that's a missing $(EXE) stuff in the makefile, one sec
Do you understand how it could have appeared after the merge? Cygwin update?
No idea, I am at a loss here on when it is valid to drop the .exe suffix on windows.
I am at a loss here on when it is valid to drop the .exe suffix on windows.
My understanding is that it's valid to drop the .exe suffix only when calling the program. Separately, I think there's an issue (at least in older versions of OCaml) where ocamlopt will barf on Windows if you tell it it's supposed to be compiling an executable binary to a file name that does not end in .exe, though I can't find a reference
and also telling dune to build install/.../foo.vo won't put foo's dependencies in the install tree
Is this only true for the .vo files, or do I need to change something else as well for the particular case of doc/stdlib/html/index.html
?
it's true for everything
So how do I get doc/stdlib/html/index.html
and all of its dependencies built for install?
(Or is there some other documentation target I should be using instead?)
make doc-html
exists IIRC and probably does exactly what you want
We determined during the call that stdlib-doc-html
is what you would need and unfortunately this target doesn't exist (it would be the intersection of doc-html
with stdlib-doc
). We should provide it.
@Matthieu Sozeau Actually it seems that the Docker image is not broken (probably because it uses its own opam file and already had dune in scope). So if you switched to Docker-Coq-Action, you would be able to test your project with the latest coq.dev without waiting for the opam package fix.
I'll try that, it'll simplify things in the future as well :)
Indeed, everything is fine with the Coq-Docker-Action. However now my own dune build
in equations fails:
https://github.com/mattam82/Coq-Equations/runs/2459397594?check_suite_focus=true
+ (script @ line 23) $ opam exec -- ./configure.sh --enable-dune
+ (script @ line 24) $ opam exec -- make -j 2 ci-dune
opam install -j 2 -y coq-hott.8.13 --ignore-constraints-on=coq
The following actions will be performed:
- install coq-hott 8.13
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-hott.8.13] downloaded from https://github.com/HoTT/HoTT/archive/refs/tags/CoqPlatform.8.13.1.tar.gz
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed coq-hott.8.13
Done.
dune build
File "theories/dune", line 6, characters 12-34:
6 | (libraries coq.plugins.extraction equations.plugin)
^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.extraction" not found.
Hint: try: dune external-lib-deps --missing @@default
make: *** [Makefile:69: ci-dune] Error 1
I suppose I should ask for the dependency differently now?
@Matthieu Sozeau , in principle no.
The library should be installed in the opam switch that docker-action is using
Well, then I don't know what's happening
so that seems like a bug on the action, maybe it relies on coq.dev?
It uses its own thing I guess
Actually I had a check on my todo list about the docker action opam, I'd be surprised if we didn't break it, let me see.
But in principle it should work ok, weird
adding ocamlfind list
and opam list
to the script should allow us to debug more
I added an ocamlfind list
to the script, running here: https://github.com/mattam82/Coq-Equations/runs/2459686353?check_suite_focus=true
@Matthieu Sozeau quite likely the docker-action-opam somehow didn't track the fact that lib/coq/META
is now lib/coq-core/META
, I ignore why is that failing but 99% is the source of the issue.
The ocamlfind list has coq-core.plugins.extraction
, so maybe I should just update the dune dependency?
Or do you expect these to be installed with prefix coq
instead of coq-core
?
Oh so silly
Sorry, indeed you need to tweak that in your dune file; sorry for not realizing today my brain is applying too many quotients
We didn't provide a coq.*
package compat setup as only a couple of packages [gappa and interval] needed the coq -> coq-core change in the CI
as in general the OCaml API of Coq is not stable we deemed it was not worth it
Ok, so I just need to rename to coq-core?
Yes
Works like a charm: https://github.com/mattam82/Coq-Equations/runs/2460000854?check_suite_focus=true
@Pierre-Marie Pédrot , I submitted https://github.com/coq/coq/pull/14205 that should help for now, tho it is a bit of a hack but we will implement a better solution.
I think tho it would help devs to merge soon https://github.com/coq/coq/pull/14176 and https://github.com/coq/coq/pull/14059 so help would be much appreciated.
Another note related to zero build latency, is that dune setups rules in a lazy way, so for example doing dune exec -- dev/shim/coqc-prelude
rebuilds quite fast for the zero rebuild, but indeed the larger your DAG tree the more time will take both for rule setup and for up-to-date checking
So it usually pays off to have more precise rules; that said, I find zero build times OK in my laptop, some timings:
in watch mode
what are you timing exactly there?
From inotify modification time to end of build time
Ok, after some trouble I think the PRs in queue should provide a reasonable experience, things are a bit simpler now, the idea is that we always build and installed layout , either in _build/install
_build_vo/default
or after install, in whatever the prefix was set.
This makes many things simpler; we still have a bit too much glue code for ci-* and test-suite targets, which we should be able to simplify if the rules in the coq.boot for finding the right directories are a bit smart.
A workaround for those not having a flock binary accessible has been added to master; please let us know of any problems.
Seems to work (https://github.com/mit-plv/fiat-crypto/pull/966/checks?check_run_id=2557367712), thanks!
Great, thanks for the confirmation!
It was a while I didn't write C code XDD, the more I try to get away from make and C the closer I seem to get XD
Last updated: May 31 2023 at 15:01 UTC