Ali Caglayan (May 24 2022 at 13:06): Ali Caglayan (May 24 2022 at 13:06):Update on dune consolidation PR.
Emilio Jesús Gallego Arias (May 24 2022 at 13:19):Consolidation PR can go after 1.
Emilio Jesús Gallego Arias (May 24 2022 at 13:19):Tho it still uses the legacy plugin loading method, unless we depend on files on _install
Emilio Jesús Gallego Arias (May 24 2022 at 13:20):as we discussed, we can:
runtime-library Ali Caglayan (May 24 2022 at 13:27):FTR 3. is a big nono and I am not happy doing that
Gaëtan Gilbert (May 24 2022 at 13:28):why?
Emilio Jesús Gallego Arias (May 24 2022 at 13:28):Ok, so let's cross 3
Emilio Jesús Gallego Arias (May 24 2022 at 13:28):then I'd suggest we try 2, seems quite easy to, and may be very useful to a lot of dune users
Emilio Jesús Gallego Arias (May 24 2022 at 13:29):basically to all dune users doing OCaml plugins, which I'm not sure how many are out there other than François
Ali Caglayan (May 24 2022 at 13:29):You shouldn't have to install the thing you are building to build it
Emilio Jesús Gallego Arias (May 24 2022 at 13:29):To run it you mean
Emilio Jesús Gallego Arias (May 24 2022 at 13:29)::)
Emilio Jesús Gallego Arias (May 24 2022 at 13:29):hehe
Emilio Jesús Gallego Arias (May 24 2022 at 13:30):actually Ali has proposed that we use packages as a boundaries, but @Ali Caglayan , isn't (package coq-core) in deps an instance of point 3. ?
Gaëtan Gilbert (May 24 2022 at 13:30):_build/install isn't actually installed, it's still under _build
Emilio Jesús Gallego Arias (May 24 2022 at 13:30):indeed, point 3 is very subtle
Ali Caglayan (May 24 2022 at 13:32):In order to have the META file in _install the entire package needs to be built. If I am building a .v file which requires plugin_a, then I need to build plugin_b because it is also in the original package.
Emilio Jesús Gallego Arias (May 24 2022 at 13:32):@Ali Caglayan that's not exactly like that
Emilio Jesús Gallego Arias (May 24 2022 at 13:32):META doesn't depend on anything, try building it yourself
Emilio Jesús Gallego Arias (May 24 2022 at 13:32):so in that sense is just an index
Emilio Jesús Gallego Arias (May 24 2022 at 13:32):but unlike foo.install
Emilio Jesús Gallego Arias (May 24 2022 at 13:32):it doesn't depend on the contents it indexes
Ali Caglayan (May 24 2022 at 13:33):If plugin_b doesn't build should the index still be built?
Emilio Jesús Gallego Arias (May 24 2022 at 13:33):Good question, as of today META is built
Emilio Jesús Gallego Arias (May 24 2022 at 13:33):just try from a clean tree dune build _build/default/META.coq-core
Ali Caglayan (May 24 2022 at 13:34):OK, then the issue is in findlib because it cannot read META.coq-core
Emilio Jesús Gallego Arias (May 24 2022 at 13:34):Or in dune because it places the meta file in the wrong place, so more in dune in fact, with this I agree with Enrico, but going back to point 3
Emilio Jesús Gallego Arias (May 24 2022 at 13:34):can you give me your opinion on this?
Emilio Jesús Gallego Arias (May 24 2022 at 13:34):Emilio Jesús Gallego Arias said:
actually Ali has proposed that we use packages as a boundaries, but Ali Caglayan , isn't
(package coq-core)in deps an instance of point 3. ?
Emilio Jesús Gallego Arias (May 24 2022 at 13:35):Because if we can do point 3 that's a good way for now
Ali Caglayan (May 24 2022 at 13:35):Right but then you cannot complain that we are building useless stuff when we depend on a package
Ali Caglayan (May 24 2022 at 13:35):If it's in core then its core stuff
Emilio Jesús Gallego Arias (May 24 2022 at 13:35):I can complain about that
Emilio Jesús Gallego Arias (May 24 2022 at 13:35):if I only need a subset of core, why build the full thing
Ali Caglayan (May 24 2022 at 13:35):If it is not meant to be built it should not be built (be in core)
Emilio Jesús Gallego Arias (May 24 2022 at 13:36):but it is not about my complaint
Emilio Jesús Gallego Arias (May 24 2022 at 13:36):it is about yours
Emilio Jesús Gallego Arias (May 24 2022 at 13:36):you said that depending on files in _install is a no go
Emilio Jesús Gallego Arias (May 24 2022 at 13:36):however, that's what package does
Emilio Jesús Gallego Arias (May 24 2022 at 13:36):Ali Caglayan said:
If it is not meant to be built it should not be built (be in core)
define "meant to be built"
Ali Caglayan (May 24 2022 at 13:36):Right internally in dune
Ali Caglayan (May 24 2022 at 13:36):However if tomorrow dune decided that _install was to be renamed
Emilio Jesús Gallego Arias (May 24 2022 at 13:36):Ali Caglayan said:
Right internally in dune
how is internal/external relevant
Ali Caglayan (May 24 2022 at 13:36):Then all our fragile scripts wont work
Emilio Jesús Gallego Arias (May 24 2022 at 13:37):actually I can do that externally too by doing dune build foo.install
Ali Caglayan (May 24 2022 at 13:37):Obviously I doubt that will happen
Ali Caglayan (May 24 2022 at 13:37):The _build/default directory is more concrete
Ali Caglayan (May 24 2022 at 13:37):and dune understands it
Emilio Jesús Gallego Arias (May 24 2022 at 13:37):Ali Caglayan said:
Obviously I doubt that will happen
we could use a variable for that, in dune
Emilio Jesús Gallego Arias (May 24 2022 at 13:37):as %{project_root}
Ali Caglayan (May 24 2022 at 13:37):Right, but in dune rules you should not be going out of project_root
Ali Caglayan (May 24 2022 at 13:37):Which is what relying on install does
Emilio Jesús Gallego Arias (May 24 2022 at 13:38):also (dep (package foo)) goes out of this
Emilio Jesús Gallego Arias (May 24 2022 at 13:38):doesn't it?
Ali Caglayan (May 24 2022 at 13:38):Yes but that is handled internally in dune
Emilio Jesús Gallego Arias (May 24 2022 at 13:38):oh no
Emilio Jesús Gallego Arias (May 24 2022 at 13:38):(deleted)
Emilio Jesús Gallego Arias (May 24 2022 at 13:38):(deleted)
Emilio Jesús Gallego Arias (May 24 2022 at 13:38):(deleted)
Emilio Jesús Gallego Arias (May 24 2022 at 13:39):as it doesn't generate _isntall
Emilio Jesús Gallego Arias (May 24 2022 at 13:39):umm, that seems weird
Ali Caglayan (May 24 2022 at 13:39):We should therefore never rely on the _build/install directory. Being relied on is not the job of that directory. It exists solely to be copied by dune install
Emilio Jesús Gallego Arias (May 24 2022 at 13:40):I'm not sure why
Emilio Jesús Gallego Arias (May 24 2022 at 13:40):actually I was correct
Emilio Jesús Gallego Arias (May 24 2022 at 13:41):_build/default/coq-core.install depends on stuff in _build/isntall
Emilio Jesús Gallego Arias (May 24 2022 at 13:41):so why we can't?
Emilio Jesús Gallego Arias (May 24 2022 at 13:41):I don't get it
Ali Caglayan (May 24 2022 at 13:41):The target coq-core.install will place everything in the _build/install directory you are correct
Ali Caglayan (May 24 2022 at 13:42):But if dune tomorrow decides, _build/install is to be renamed to _build/FOOBAR everything will break for us
Ali Caglayan (May 24 2022 at 13:42):But none of the (package coq-core) deps and the like will
Ali Caglayan (May 24 2022 at 13:42):There are explicit variables for depending on library things like %{lib:asdf}
Ali Caglayan (May 24 2022 at 13:43):The whole point is that these are not fixed.
Ali Caglayan (May 24 2022 at 13:43):Dune does not guarantee the install directory exists nor do they recommend it
Ali Caglayan (May 24 2022 at 13:44):We shouldn't have to "install" things in order to rely on them in a build
Ali Caglayan (May 24 2022 at 13:45):As we said before the data we need (for findlib) is already in META.coq-core
Ali Caglayan (May 24 2022 at 13:45):so we need to patch it to understand that file
Ali Caglayan (May 24 2022 at 13:53):Emilio Jesús Gallego Arias said:
actually Ali has proposed that we use packages as a boundaries, but Ali Caglayan , isn't
(package coq-core)in deps an instance of point 3. ?
So to be clear about this point. We can depend on (package coq-core), the fact that it pull deps from _build/install is not our problem anymore. I'm saying, explicitly expecting files in the _build/install directory to exist is wrong. We should go through the proper dune constructs like (package coq-core). Ofc there are issues relying on building the entire package to build a single .v file, but that can be alleviated by allowing Coq via findlib to understand the META.plugin_foo files that get generated via the build.
Emilio Jesús Gallego Arias (May 24 2022 at 13:54):Yes, so the best option is then to do a combo of 2 and 3
Emilio Jesús Gallego Arias (May 24 2022 at 13:54):where we add a variable for the install dir
Gaëtan Gilbert (May 24 2022 at 13:56):Ali Caglayan said:
But if dune tomorrow decides, _build/install is to be renamed to _build/FOOBAR everything will break for us
is there a plan to do that? why worry about this instead of anything else?
Ali Caglayan (May 24 2022 at 13:57):Even relying on %{lib:coq-core:META} will not work AFAIK
Ali Caglayan (May 24 2022 at 13:58):The files generated in _build/install are not known in advance by dune
Ali Caglayan (May 24 2022 at 13:58):So when you have a rule to depend on the meta file in the coq-core install dir, dune doesn't know what needs to be done
Ali Caglayan (May 24 2022 at 14:00):Because we shouldn't be relying on the install dir
Ali Caglayan (May 24 2022 at 14:00):Anyway, I have expressed my desire for 1, I don't think 2 is worth it and 3 is extremely fragile and just more useless work for us in the future
Ali Caglayan (May 24 2022 at 14:01):Emilio Jesús Gallego Arias said:
as we discussed, we can:
- patch findlib to support META.coq-core without a directory file
- patch dune to support
runtime-library- depend on _install files
Ali Caglayan (May 24 2022 at 14:03):Regarding 1 by the way: We should ship our own patched version of findlib since getting packages to update to the latest with the patch will be a pain.
Enrico Tassi (May 24 2022 at 14:58):Please don't fork findlib, fix dune instead.
Rudi Grinberg (May 24 2022 at 14:59):Enrico Tassi said:
Please don't fork findlib, fix dune instead.
is there a dune bug ticket for this?
Enrico Tassi (May 24 2022 at 15:17):I opened one, please move the discussion there
Gaëtan Gilbert (May 24 2022 at 15:39):(https://github.com/ocaml/dune/issues/5767)
Emilio Jesús Gallego Arias (May 24 2022 at 16:05):Ali Caglayan said:
Even relying on
%{lib:coq-core:META}will not work AFAIK
why not? @Ali Caglayan I'm having trouble understanding why you are againt some versions of 3, but not others.
Concretely, if the rules for $pkg.install do depend on stuff in install, why we can't do the same?
Forking findlib indeed seems not a good idea to me.
Ali Caglayan (May 24 2022 at 16:21):You said to me before, you don't want to depend on (package coq-core) because it saves a few seconds.
Ali Caglayan (May 24 2022 at 16:21):That is the only way to guarantee the META file in _build/install gets generated
Ali Caglayan (May 24 2022 at 16:23):The reason I think I findlib patch is more sensible is because we already have META.coq-core being generated. Findlib doesn't understand this META file, because according to it, it is sitting in the wrong location.
Ali Caglayan (May 24 2022 at 16:23):We don't need to build the entire package if we depend on META.coq-core.
Ali Caglayan (May 24 2022 at 16:24):On the side: Putting a "plugin" in a "core" package seems completely bonkers to me. It should be in its own package.
Ali Caglayan (May 24 2022 at 16:24):That way you can have finer dependencies.
Emilio Jesús Gallego Arias (May 24 2022 at 16:42):Yes, I think that depending on package is not good; but my point is let's forget about that for a moment.
Why would be depending on (package) good, which actually depends on _install stuff, instead of using our own rules?
What is the problem with %{lib:coq-core:META} %{lib:coq-core.plugins.ltac:ltac_plugin.cmxs} by the way?
Emilio Jesús Gallego Arias (May 24 2022 at 16:43):That seems to me like a fine dep?
Ali Caglayan (May 24 2022 at 16:45):Compare that with a possible (package coq-core.plugins.ltac).
Ali Caglayan (May 24 2022 at 16:46):Dune can only have targets in the install directory through the (package ) stanza
Ali Caglayan (May 24 2022 at 16:46):If you try %{lib:coq-core:META} you will get a not found error
Ali Caglayan (May 24 2022 at 16:49):Anyway, if I can't get my point across then maybe I am doing something wrong. I will spend my time thinking about other things.
Ali Caglayan (May 24 2022 at 16:52):https://www.youtube.com/watch?v=HMqZ2PPOLik
Emilio Jesús Gallego Arias (May 24 2022 at 16:53):Ali Caglayan said:
If you try
%{lib:coq-core:META}you will get a not found error
yes, because that's not a lib, there is an issue for having %{pkg:foo:file}
Emilio Jesús Gallego Arias (May 24 2022 at 16:54):Ali Caglayan said:
Dune can only have targets in the install directory through the (package ) stanza
This is where I'm confused, your sentence doesn't make sense to me.
Targets in the install directory are added only with (install ...) stanzas
Emilio Jesús Gallego Arias (May 24 2022 at 16:54):for the engine are regular rules
Emilio Jesús Gallego Arias (May 24 2022 at 16:54):anyways we don't want to have targets on install, but depend on stuff in _install
Emilio Jesús Gallego Arias (May 24 2022 at 16:54):so I must be doing something wrong, because I have asked a very concrete question a few times and so far I didn't got an answer
Emilio Jesús Gallego Arias (May 24 2022 at 16:55):let me rephrase
Emilio Jesús Gallego Arias (May 24 2022 at 16:55):there is a lot of stuff already in dune that depends on files on _build/install , so modulo the renaming risk (which can be solved easily) what is the problem for Coq doing so?
Emilio Jesús Gallego Arias (May 25 2022 at 16:15):I did test all the stuff that we discussed in the call and I have to say it works and I'm satisfied with current state of the code, modulo a few more tweaks
Emilio Jesús Gallego Arias (May 25 2022 at 16:16):Dune needs to be updated to support the new method, but works fine with the compat layer (modulo the users having to use the new Declare ML Syntax)
Emilio Jesús Gallego Arias (May 25 2022 at 16:16):Dune's test-suite works fine with 8.16 once that is done
Last updated: Sep 30 2023 at 16:01 UTC