Stream: Coq devs & plugin devs

Topic: Dune Migration


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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/

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Mar 27 2021 at 14:02):

Seems like a lot of work for little gain IMHO.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 27 2021 at 14:03):

which is ready to install

view this post on Zulip Théo Zimmermann (Mar 27 2021 at 14:03):

OK

view this post on Zulip Théo Zimmermann (Mar 27 2021 at 14:04):

IMHO this can always be refined later based on experience and feedback.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 27 2021 at 14:04):

Let's hear from @Guillaume Melquiond

view this post on Zulip 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...

view this post on Zulip 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 make you get a build like before, without opaque

how does that work wrt the plan of switching to Makefile.dune by default?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 27 2021 at 14:16):

make -f Makefile.dune help-install tries to provide an overview

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 30 2021 at 07:45):

I'll have a look.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:05):

Hey @Emilio Jesús Gallego Arias, I'm back.

view this post on Zulip 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):

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:06):

  1. users (or rather packagers) who want to build a Coq release or even a development version but for installing and using.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:07):

  1. developers who need to build Coq everyday (with incremental build support)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:13):

I don't mind if I have to explicitly call ./configure first.

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:26):

I see

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:26):

So if it works fine, why you have to go back?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:27):

Not the Dune ones in this case.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:27):

Ok, so fixing the dune case would actually solve your problem?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:28):

I see.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:29):

Well, I guess it's already worth doing.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:29):

so indeed I will add the dune profile as configure variable

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:29):

but you still have the problem then

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:31):

Why not?

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:32):

So currently, what works properly is the promoting of fullGrammar and orderedGrammar.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:32):

We can use a little script + subdir to achieve that

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:33):

https://github.com/ocaml/dune/blob/main/plugin/jbuild_plugin.mli

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:34):

Would live in a dune file but using the jbuild_plugin module

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:35):

this, + (subdir ..) should suffice for a lot of cases

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:35):

Yes

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:35):

not the cleanest thing, but is is the way many other systems work

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:36):

so, looking at the makefile.doc

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:36):

indeed

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:36):

what are the targets that are not declared?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:37):

already that code in makefile seems pretty broken IIUC

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:37):

in the sense of the dependency graph to be sound

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:37):

What do you mean?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:39):

I mean that calling doc_gram seems to produce a lot of files

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:39):

however these files are not declared in the make rules

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :(

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:41):

2000 lines of ocaml code and not a single comment....

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:43):

This is irrelevant to the current discussion, isn't it?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:44):

It's not like it was an actual part of Coq.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:46):

:(

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:47):

I can't even make sense of the makefile rules

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:48):

Why don't you ask me? I know what it does.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:49):

And my requests are in no way blocking BTW.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:52):

How many calls to the tool happen?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:52):

Two ?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:54):

right

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):

First call already works in dune, right?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):

so second call is just to update the files?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:54):

so we need to add a rule for patching mlg files?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:55):

not the best, however it is easy

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:55):

mlg files are never modified by the tool

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:55):

did you mean rst files?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:55):

sorry, rst

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 13:55):

yes I mean that sorry

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:55):

OK

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:55):

so in the make setup, the tool was intended to be called only once

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:55):

even if it has multiple phases

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:56):

it has different options to stop at one given phase

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:56):

So the first phase is to generate fullGrammar from the mlg files.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:57):

It works fine in Dune.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:57):

This phase takes the fullGrammar and the common.edit_mlg files as input.

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 13:59):

The last phase copies the relevant chunks into the rst files.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 14:01):

I see thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 14:03):

but indeed that's the classical tradeoff on whether to put file logic

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 14:03):

in the build system or in the app

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 01 2021 at 19:43):

Yep, this is perfect. (Though, I still need to test it by myself.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 14:34):

Oh, thanks a lot!

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Notification Bot (Apr 23 2021 at 09:41):

This topic was moved by Théo Zimmermann to #coqbot devs & users > CI minimization feedback

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 13:35):

Ah, that's a missing $(EXE) stuff in the makefile, one sec

view this post on Zulip Théo Zimmermann (Apr 28 2021 at 13:39):

Do you understand how it could have appeared after the merge? Cygwin update?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 14:00):

it's true for everything

view this post on Zulip 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?

view this post on Zulip Jason Gross (Apr 28 2021 at 14:50):

(Or is there some other documentation target I should be using instead?)

view this post on Zulip Théo Zimmermann (Apr 28 2021 at 15:15):

make doc-html exists IIRC and probably does exactly what you want

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 16:16):

I'll try that, it'll simplify things in the future as well :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 16:21):

I suppose I should ask for the dependency differently now?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 16:37):

@Matthieu Sozeau , in principle no.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 16:38):

Well, then I don't know what's happening

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 16:38):

It uses its own thing I guess

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 16:40):

But in principle it should work ok, weird

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 16:56):

Or do you expect these to be installed with prefix coq instead of coq-core ?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 17:15):

Oh so silly

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 17:30):

Ok, so I just need to rename to coq-core?

view this post on Zulip Théo Zimmermann (Apr 28 2021 at 17:39):

Yes

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 17:47):

Works like a charm: https://github.com/mattam82/Coq-Equations/runs/2460000854?check_suite_focus=true

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 19:08):

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 20:37):

in watch mode

what are you timing exactly there?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 23:32):

From inotify modification time to end of build time

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2021 at 21:27):

Great, thanks for the confirmation!

view this post on Zulip 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: Oct 21 2021 at 20:02 UTC