Emilio Jesús Gallego Arias (Mar 06 2021 at 00:02): Emilio Jesús Gallego Arias (Mar 06 2021 at 00:02):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
Emilio Jesús Gallego Arias (Mar 06 2021 at 00:52):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.
Ali Caglayan (Mar 06 2021 at 14:44):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?
Emilio Jesús Gallego Arias (Mar 26 2021 at 17:30):@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/
Emilio Jesús Gallego Arias (Mar 26 2021 at 17:31):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?
Théo Zimmermann (Mar 26 2021 at 18:38):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.
Emilio Jesús Gallego Arias (Mar 27 2021 at 13:57):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.
Théo Zimmermann (Mar 27 2021 at 13:59):Is there any way to make the two "compatible" by, e.g., using a different profile?
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:00):That is likely to never work well, IMHO you wanna make a choice to work with one build system or the other
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:01):To make them compatible the make-based system would have to learn quite a bit about profiles, dependencies on envars, ocaml compiler, etc...
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:02):Seems like a lot of work for little gain IMHO.
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:03):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
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:03):So the idea of the PR is that if you type make you get a build like before, without opaque
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:03):which is ready to install
Théo Zimmermann (Mar 27 2021 at 14:03):OK
Théo Zimmermann (Mar 27 2021 at 14:04):IMHO this can always be refined later based on experience and feedback.
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:04):Let's hear from @Guillaume Melquiond
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:05):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...
Gaëtan Gilbert (Mar 27 2021 at 14:13):Emilio Jesús Gallego Arias said:
So the idea of the PR is that if you type
makeyou get a build like before, without opaque
how does that work wrt the plan of switching to Makefile.dune by default?
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:15):@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
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:16):make -f Makefile.dune help-install tries to provide an overview
Emilio Jesús Gallego Arias (Mar 27 2021 at 14:16):We can have configure generate the profile name if you think it is useful, I'm not so sure tho
Emilio Jesús Gallego Arias (Mar 29 2021 at 17:54):@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.
Théo Zimmermann (Mar 30 2021 at 07:45):I'll have a look.
Emilio Jesús Gallego Arias (Mar 31 2021 at 12:13):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.
Théo Zimmermann (Mar 31 2021 at 12:28):Hey @Emilio Jesús Gallego Arias, I'm replying to a student and I'll be there.
Théo Zimmermann (Mar 31 2021 at 13:05):Hey @Emilio Jesús Gallego Arias, I'm back.
Théo Zimmermann (Mar 31 2021 at 13:06):So, it seems clear that there are two main use cases for the build system(s):
Théo Zimmermann (Mar 31 2021 at 13:06): Théo Zimmermann (Mar 31 2021 at 13:07): Théo Zimmermann (Mar 31 2021 at 13:07):For the first group, it is good to keep supporting ./configure -prefix /foo && make && make install.
Théo Zimmermann (Mar 31 2021 at 13:07):For the second group, it is clear that Dune brings benefits and there should be only one recommended build method.
Théo Zimmermann (Mar 31 2021 at 13:08):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.
Théo Zimmermann (Mar 31 2021 at 13:10):So it seems reasonable to keep -profile devel (while maybe removing -local) but to make it automatically rely on the dev Dune profile.
Théo Zimmermann (Mar 31 2021 at 13:11):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).
Théo Zimmermann (Mar 31 2021 at 13:13):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.
Théo Zimmermann (Mar 31 2021 at 13:13):I don't mind if I have to explicitly call ./configure first.
Théo Zimmermann (Mar 31 2021 at 13:14):Especially given that these are developer-only targets, and that we would like to generalize their use soon.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:25):Thanks for the write up @Théo Zimmermann , what do you specifically mean by "keeping the benefits of the dev Dune profile"?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:25):By the way, it should be possible to much improve the doc_gram, only thing preventing me from doing so is time
Théo Zimmermann (Mar 31 2021 at 13:25):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.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:26):I see
Théo Zimmermann (Mar 31 2021 at 13:26):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.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:26):So if it works fine, why you have to go back?
Théo Zimmermann (Mar 31 2021 at 13:27):Oh, I think we are misunderstanding each other here. I meant the legacy makefile targets work fine.
Théo Zimmermann (Mar 31 2021 at 13:27):Not the Dune ones in this case.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:27):Ok, so fixing the dune case would actually solve your problem?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:28):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
Théo Zimmermann (Mar 31 2021 at 13:28):I see.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:29):so we would solve little, other than making the switch between the two systems a bit more seamless
Théo Zimmermann (Mar 31 2021 at 13:29):Well, I guess it's already worth doing.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:29):so indeed I will add the dune profile as configure variable
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:29):but you still have the problem then
Théo Zimmermann (Mar 31 2021 at 13:29):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.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:31):Why not?
Théo Zimmermann (Mar 31 2021 at 13:31):Because the targets that you need to promote are all over the place (all the rst files in multiple subdirectories of doc/sphinx).
Théo Zimmermann (Mar 31 2021 at 13:32):So currently, what works properly is the promoting of fullGrammar and orderedGrammar.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:32):We can use a little script + subdir to achieve that
Théo Zimmermann (Mar 31 2021 at 13:32):(You have to call the Dune target twice though, which is a bit annoying but not a real issue.)
Théo Zimmermann (Mar 31 2021 at 13:33):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?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:33):https://github.com/ocaml/dune/blob/main/plugin/jbuild_plugin.mli
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:34):Would live in a dune file but using the jbuild_plugin module
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:34):likely some mangling would be needed, I need to look at the tool more closely
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:34):Dune 3.0 will have a much better workflow for this as you can have rules generate dune files
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:35):this, + (subdir ..) should suffice for a lot of cases
Théo Zimmermann (Mar 31 2021 at 13:35):Yes
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:35):not the cleanest thing, but is is the way many other systems work
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:35):there is also discussion about having a true programming language in the configuration of dune
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:35):I don't like it too much, but your use case seems simple enough as to be OK
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:36):so, looking at the makefile.doc
Théo Zimmermann (Mar 31 2021 at 13:36):indeed
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:36):what are the targets that are not declared?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:37):already that code in makefile seems pretty broken IIUC
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:37):in the sense of the dependency graph to be sound
Théo Zimmermann (Mar 31 2021 at 13:37):What do you mean?
Théo Zimmermann (Mar 31 2021 at 13:38):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.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:39):I mean that calling doc_gram seems to produce a lot of files
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:39):however these files are not declared in the make rules
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:40):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.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:40):And I'd rather avoid the top-level makefile depending on configure-generated values
Théo Zimmermann (Mar 31 2021 at 13:40):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.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:40):After looking at doc_gram, I'm afraid that tool is gonna be very hard to maintain :(
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:41):2000 lines of ocaml code and not a single comment....
Théo Zimmermann (Mar 31 2021 at 13:43):This is irrelevant to the current discussion, isn't it?
Théo Zimmermann (Mar 31 2021 at 13:44):Even if we had to delete that tool at some point, it would already have helped make the documentation better.
Théo Zimmermann (Mar 31 2021 at 13:44):It's not like it was an actual part of Coq.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:46):Well, a whole lot of work is now blocked on trying to udnerstand the tool
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:46):I have been looking at it for 30 mins and still can't understand a single thing of what it does
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:46)::(
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:47):I can't even make sense of the makefile rules
Théo Zimmermann (Mar 31 2021 at 13:48):Why don't you ask me? I know what it does.
Théo Zimmermann (Mar 31 2021 at 13:49):And my requests are in no way blocking BTW.
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:52):How many calls to the tool happen?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:52):Two ?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:53):And my requests are in no way blocking BTW.
we should fix all use cases, otherwise we will never end the migration
Théo Zimmermann (Mar 31 2021 at 13:54):right
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):First call already works in dune, right?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):so second call is just to update the files?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):so we need to add a rule for patching mlg files?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):one quick way to do this is to add one rule per mlg file
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:55):not the best, however it is easy
Théo Zimmermann (Mar 31 2021 at 13:55):mlg files are never modified by the tool
Théo Zimmermann (Mar 31 2021 at 13:55):did you mean rst files?
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:55):sorry, rst
Emilio Jesús Gallego Arias (Mar 31 2021 at 13:55):yes I mean that sorry
Théo Zimmermann (Mar 31 2021 at 13:55):OK
Théo Zimmermann (Mar 31 2021 at 13:55):so in the make setup, the tool was intended to be called only once
Théo Zimmermann (Mar 31 2021 at 13:55):even if it has multiple phases
Théo Zimmermann (Mar 31 2021 at 13:56):it has different options to stop at one given phase
Théo Zimmermann (Mar 31 2021 at 13:56):but we could also change it to perform the different phases independently if that would help
Théo Zimmermann (Mar 31 2021 at 13:56):So the first phase is to generate fullGrammar from the mlg files.
Théo Zimmermann (Mar 31 2021 at 13:57):It works fine in Dune.
Théo Zimmermann (Mar 31 2021 at 13:57):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.
Théo Zimmermann (Mar 31 2021 at 13:57):This phase takes the fullGrammar and the common.edit_mlg files as input.
Théo Zimmermann (Mar 31 2021 at 13:59):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).
Théo Zimmermann (Mar 31 2021 at 13:59):The last phase copies the relevant chunks into the rst files.
Théo Zimmermann (Mar 31 2021 at 13:59):Currently, the dune rule does the full thing, but it only promotes the fullGrammar and orderedGrammar files.
Théo Zimmermann (Mar 31 2021 at 14:00):However, if you do a cp -R _build/default/doc/sphinx doc/sphinx, you get the edits to the rst files as well.
Emilio Jesús Gallego Arias (Mar 31 2021 at 14:01):I see thanks
Emilio Jesús Gallego Arias (Mar 31 2021 at 14:02):I guess we need to let dune know about the patching, how tricky is this going to be I don't know
Emilio Jesús Gallego Arias (Mar 31 2021 at 14:03):A bit of the problem seems indeed that the tool could be a bit more modular
Emilio Jesús Gallego Arias (Mar 31 2021 at 14:03):but indeed that's the classical tradeoff on whether to put file logic
Emilio Jesús Gallego Arias (Mar 31 2021 at 14:03):in the build system or in the app
Emilio Jesús Gallego Arias (Mar 31 2021 at 15:40):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?
Théo Zimmermann (Apr 01 2021 at 07:47):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.
Emilio Jesús Gallego Arias (Apr 01 2021 at 09:13):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.
Emilio Jesús Gallego Arias (Apr 01 2021 at 15:26):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
Théo Zimmermann (Apr 01 2021 at 19:43):Yep, this is perfect. (Though, I still need to test it by myself.)
Emilio Jesús Gallego Arias (Apr 05 2021 at 16:25):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.
Emilio Jesús Gallego Arias (Apr 08 2021 at 14:31):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.
Théo Zimmermann (Apr 08 2021 at 14:33):Agreed. I was just lacking time to do a proper review (I started one yesterday though).
Emilio Jesús Gallego Arias (Apr 08 2021 at 14:34):Oh, thanks a lot!
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:01):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.
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:11):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]
Notification Bot (Apr 23 2021 at 09:41):This topic was moved by Théo Zimmermann to #coqbot devs & users > CI minimization feedback
Emilio Jesús Gallego Arias (Apr 26 2021 at 21:05):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
Emilio Jesús Gallego Arias (Apr 28 2021 at 00:02):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]
Emilio Jesús Gallego Arias (Apr 28 2021 at 00:02):We could add some checks, but it feels sad that we have to do an anti-cleanup.
Jason Gross (Apr 28 2021 at 00:31):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
Jason Gross (Apr 28 2021 at 00:34):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
Théo Zimmermann (Apr 28 2021 at 12:44):@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.
Gaëtan Gilbert (Apr 28 2021 at 12:44):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
Gaëtan Gilbert (Apr 28 2021 at 12:45):and also telling dune to build install/.../foo.vo won't put foo's dependencies in the install tree
Théo Zimmermann (Apr 28 2021 at 13:30):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.
Théo Zimmermann (Apr 28 2021 at 13:31):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.
Emilio Jesús Gallego Arias (Apr 28 2021 at 13:35):Ah, that's a missing $(EXE) stuff in the makefile, one sec
Théo Zimmermann (Apr 28 2021 at 13:39):Do you understand how it could have appeared after the merge? Cygwin update?
Emilio Jesús Gallego Arias (Apr 28 2021 at 13:44):No idea, I am at a loss here on when it is valid to drop the .exe suffix on windows.
Jason Gross (Apr 28 2021 at 13:53):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
Jason Gross (Apr 28 2021 at 13:56):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?
Gaëtan Gilbert (Apr 28 2021 at 14:00):it's true for everything
Jason Gross (Apr 28 2021 at 14:50):So how do I get doc/stdlib/html/index.html and all of its dependencies built for install?
Jason Gross (Apr 28 2021 at 14:50):(Or is there some other documentation target I should be using instead?)
Théo Zimmermann (Apr 28 2021 at 15:15):make doc-html exists IIRC and probably does exactly what you want
Théo Zimmermann (Apr 28 2021 at 15:33):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.
Théo Zimmermann (Apr 28 2021 at 15:37):@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.
Matthieu Sozeau (Apr 28 2021 at 16:16):I'll try that, it'll simplify things in the future as well :)
Matthieu Sozeau (Apr 28 2021 at 16:20):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
Matthieu Sozeau (Apr 28 2021 at 16:21): + (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?
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:37):@Matthieu Sozeau , in principle no.
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:38):The library should be installed in the opam switch that docker-action is using
Matthieu Sozeau (Apr 28 2021 at 16:38):Well, then I don't know what's happening
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:38):so that seems like a bug on the action, maybe it relies on coq.dev?
Matthieu Sozeau (Apr 28 2021 at 16:38):It uses its own thing I guess
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:39):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.
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:40):But in principle it should work ok, weird
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:40):adding ocamlfind list and opam list to the script should allow us to debug more
Matthieu Sozeau (Apr 28 2021 at 16:53):I added an ocamlfind list to the script, running here: https://github.com/mattam82/Coq-Equations/runs/2459686353?check_suite_focus=true
Emilio Jesús Gallego Arias (Apr 28 2021 at 16:54):@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.
Matthieu Sozeau (Apr 28 2021 at 16:55):The ocamlfind list has coq-core.plugins.extraction, so maybe I should just update the dune dependency?
Matthieu Sozeau (Apr 28 2021 at 16:56):Or do you expect these to be installed with prefix coq instead of coq-core ?
Emilio Jesús Gallego Arias (Apr 28 2021 at 17:15):Oh so silly
Emilio Jesús Gallego Arias (Apr 28 2021 at 17:15):Sorry, indeed you need to tweak that in your dune file; sorry for not realizing today my brain is applying too many quotients
Emilio Jesús Gallego Arias (Apr 28 2021 at 17:16):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
Emilio Jesús Gallego Arias (Apr 28 2021 at 17:16):as in general the OCaml API of Coq is not stable we deemed it was not worth it
Matthieu Sozeau (Apr 28 2021 at 17:30):Ok, so I just need to rename to coq-core?
Théo Zimmermann (Apr 28 2021 at 17:39):Yes
Matthieu Sozeau (Apr 28 2021 at 17:47):Works like a charm: https://github.com/mattam82/Coq-Equations/runs/2460000854?check_suite_focus=true
Emilio Jesús Gallego Arias (Apr 28 2021 at 18:40):@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.
Emilio Jesús Gallego Arias (Apr 28 2021 at 18:57):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
Emilio Jesús Gallego Arias (Apr 28 2021 at 18:57):So it usually pays off to have more precise rules; that said, I find zero build times OK in my laptop, some timings:
Emilio Jesús Gallego Arias (Apr 28 2021 at 19:08): Gaëtan Gilbert (Apr 28 2021 at 20:37):in watch mode
what are you timing exactly there?
Emilio Jesús Gallego Arias (Apr 28 2021 at 23:32):From inotify modification time to end of build time
Emilio Jesús Gallego Arias (May 01 2021 at 14:37):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.
Emilio Jesús Gallego Arias (May 11 2021 at 14:43):A workaround for those not having a flock binary accessible has been added to master; please let us know of any problems.
Jason Gross (May 11 2021 at 20:55):Seems to work (https://github.com/mit-plv/fiat-crypto/pull/966/checks?check_run_id=2557367712), thanks!
Emilio Jesús Gallego Arias (May 11 2021 at 21:27):Great, thanks for the confirmation!
Emilio Jesús Gallego Arias (May 11 2021 at 21:28):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