Update on dune consolidation PR.
Consolidation PR can go after 1.
Tho it still uses the legacy plugin loading method, unless we depend on files on _install
as we discussed, we can:
runtime-library
FTR 3. is a big nono and I am not happy doing that
why?
Ok, so let's cross 3
then I'd suggest we try 2, seems quite easy to, and may be very useful to a lot of dune users
basically to all dune users doing OCaml plugins, which I'm not sure how many are out there other than François
You shouldn't have to install the thing you are building to build it
To run it you mean
:)
hehe
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. ?
_build/install isn't actually installed, it's still under _build
indeed, point 3 is very subtle
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.
@Ali Caglayan that's not exactly like that
META doesn't depend on anything, try building it yourself
so in that sense is just an index
but unlike foo.install
it doesn't depend on the contents it indexes
If plugin_b doesn't build should the index still be built?
Good question, as of today META is built
just try from a clean tree dune build _build/default/META.coq-core
OK, then the issue is in findlib because it cannot read META.coq-core
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
can you give me your opinion on this?
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. ?
Because if we can do point 3 that's a good way for now
Right but then you cannot complain that we are building useless stuff when we depend on a package
If it's in core then its core stuff
I can complain about that
if I only need a subset of core, why build the full thing
If it is not meant to be built it should not be built (be in core)
but it is not about my complaint
it is about yours
you said that depending on files in _install is a no go
however, that's what package does
Ali Caglayan said:
If it is not meant to be built it should not be built (be in core)
define "meant to be built"
Right internally in dune
However if tomorrow dune decided that _install was to be renamed
Ali Caglayan said:
Right internally in dune
how is internal/external relevant
Then all our fragile scripts wont work
actually I can do that externally too by doing dune build foo.install
Obviously I doubt that will happen
The _build/default directory is more concrete
and dune understands it
Ali Caglayan said:
Obviously I doubt that will happen
we could use a variable for that, in dune
as %{project_root}
Right, but in dune rules you should not be going out of project_root
Which is what relying on install does
also (dep (package foo))
goes out of this
doesn't it?
Yes but that is handled internally in dune
oh no
(deleted)
(deleted)
(deleted)
as it doesn't generate _isntall
umm, that seems weird
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
I'm not sure why
actually I was correct
_build/default/coq-core.install
depends on stuff in _build/isntall
so why we can't?
I don't get it
The target coq-core.install will place everything in the _build/install directory you are correct
But if dune tomorrow decides, _build/install is to be renamed to _build/FOOBAR everything will break for us
But none of the (package coq-core) deps and the like will
There are explicit variables for depending on library things like %{lib:asdf}
The whole point is that these are not fixed.
Dune does not guarantee the install directory exists nor do they recommend it
We shouldn't have to "install" things in order to rely on them in a build
As we said before the data we need (for findlib) is already in META.coq-core
so we need to patch it to understand that file
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.
Yes, so the best option is then to do a combo of 2 and 3
where we add a variable for the install dir
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?
Even relying on %{lib:coq-core:META}
will not work AFAIK
The files generated in _build/install are not known in advance by dune
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
Because we shouldn't be relying on the install dir
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
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
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.
Please don't fork findlib, fix dune instead.
Enrico Tassi said:
Please don't fork findlib, fix dune instead.
is there a dune bug ticket for this?
I opened one, please move the discussion there
(https://github.com/ocaml/dune/issues/5767)
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.
You said to me before, you don't want to depend on (package coq-core)
because it saves a few seconds.
That is the only way to guarantee the META file in _build/install gets generated
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.
We don't need to build the entire package if we depend on META.coq-core
.
On the side: Putting a "plugin" in a "core" package seems completely bonkers to me. It should be in its own package.
That way you can have finer dependencies.
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?
That seems to me like a fine dep?
Compare that with a possible (package coq-core.plugins.ltac)
.
Dune can only have targets in the install directory through the (package ) stanza
If you try %{lib:coq-core:META}
you will get a not found error
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.
https://www.youtube.com/watch?v=HMqZ2PPOLik
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}
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
for the engine are regular rules
anyways we don't want to have targets on install, but depend on stuff in _install
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
let me rephrase
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?
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
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)
Dune's test-suite works fine with 8.16 once that is done
Last updated: Jun 09 2023 at 08:01 UTC