Stream: Coq devs & plugin devs

Topic: Roadmap to "consolidation PR"


view this post on Zulip Ali Caglayan (May 24 2022 at 13:06):

Update on dune consolidation PR.

  1. There is a bug in plugin loading that needs to be fixed: https://github.com/coq/coq/pull/15991
  2. Fix some issues with META / findlib / dune
  3. Consolidation PR

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:19):

Consolidation PR can go after 1.

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:20):

as we discussed, we can:

  1. patch findlib to support META.coq-core without a directory file
  2. patch dune to support runtime-library
  3. depend on _install files

view this post on Zulip Ali Caglayan (May 24 2022 at 13:27):

FTR 3. is a big nono and I am not happy doing that

view this post on Zulip Gaëtan Gilbert (May 24 2022 at 13:28):

why?

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:28):

Ok, so let's cross 3

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

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

view this post on Zulip Ali Caglayan (May 24 2022 at 13:29):

You shouldn't have to install the thing you are building to build it

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:29):

To run it you mean

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:29):

:)

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:29):

hehe

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

view this post on Zulip Gaëtan Gilbert (May 24 2022 at 13:30):

_build/install isn't actually installed, it's still under _build

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:30):

indeed, point 3 is very subtle

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:32):

@Ali Caglayan that's not exactly like that

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:32):

META doesn't depend on anything, try building it yourself

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:32):

so in that sense is just an index

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:32):

but unlike foo.install

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:32):

it doesn't depend on the contents it indexes

view this post on Zulip Ali Caglayan (May 24 2022 at 13:33):

If plugin_b doesn't build should the index still be built?

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:33):

Good question, as of today META is built

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:33):

just try from a clean tree dune build _build/default/META.coq-core

view this post on Zulip Ali Caglayan (May 24 2022 at 13:34):

OK, then the issue is in findlib because it cannot read META.coq-core

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:34):

can you give me your opinion on this?

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

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

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

view this post on Zulip Ali Caglayan (May 24 2022 at 13:35):

If it's in core then its core stuff

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:35):

I can complain about that

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:35):

if I only need a subset of core, why build the full thing

view this post on Zulip Ali Caglayan (May 24 2022 at 13:35):

If it is not meant to be built it should not be built (be in core)

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:36):

but it is not about my complaint

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:36):

it is about yours

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:36):

you said that depending on files in _install is a no go

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:36):

however, that's what package does

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

view this post on Zulip Ali Caglayan (May 24 2022 at 13:36):

Right internally in dune

view this post on Zulip Ali Caglayan (May 24 2022 at 13:36):

However if tomorrow dune decided that _install was to be renamed

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:36):

Ali Caglayan said:

Right internally in dune

how is internal/external relevant

view this post on Zulip Ali Caglayan (May 24 2022 at 13:36):

Then all our fragile scripts wont work

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:37):

actually I can do that externally too by doing dune build foo.install

view this post on Zulip Ali Caglayan (May 24 2022 at 13:37):

Obviously I doubt that will happen

view this post on Zulip Ali Caglayan (May 24 2022 at 13:37):

The _build/default directory is more concrete

view this post on Zulip Ali Caglayan (May 24 2022 at 13:37):

and dune understands it

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:37):

as %{project_root}

view this post on Zulip Ali Caglayan (May 24 2022 at 13:37):

Right, but in dune rules you should not be going out of project_root

view this post on Zulip Ali Caglayan (May 24 2022 at 13:37):

Which is what relying on install does

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:38):

also (dep (package foo)) goes out of this

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:38):

doesn't it?

view this post on Zulip Ali Caglayan (May 24 2022 at 13:38):

Yes but that is handled internally in dune

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:38):

oh no

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:38):

(deleted)

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:38):

(deleted)

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:38):

(deleted)

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:39):

as it doesn't generate _isntall

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:39):

umm, that seems weird

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:40):

I'm not sure why

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:40):

actually I was correct

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:41):

_build/default/coq-core.install depends on stuff in _build/isntall

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:41):

so why we can't?

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:41):

I don't get it

view this post on Zulip Ali Caglayan (May 24 2022 at 13:41):

The target coq-core.install will place everything in the _build/install directory you are correct

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

view this post on Zulip Ali Caglayan (May 24 2022 at 13:42):

But none of the (package coq-core) deps and the like will

view this post on Zulip Ali Caglayan (May 24 2022 at 13:42):

There are explicit variables for depending on library things like %{lib:asdf}

view this post on Zulip Ali Caglayan (May 24 2022 at 13:43):

The whole point is that these are not fixed.

view this post on Zulip Ali Caglayan (May 24 2022 at 13:43):

Dune does not guarantee the install directory exists nor do they recommend it

view this post on Zulip Ali Caglayan (May 24 2022 at 13:44):

We shouldn't have to "install" things in order to rely on them in a build

view this post on Zulip Ali Caglayan (May 24 2022 at 13:45):

As we said before the data we need (for findlib) is already in META.coq-core

view this post on Zulip Ali Caglayan (May 24 2022 at 13:45):

so we need to patch it to understand that file

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 13:54):

where we add a variable for the install dir

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

view this post on Zulip Ali Caglayan (May 24 2022 at 13:57):

Even relying on %{lib:coq-core:META} will not work AFAIK

view this post on Zulip Ali Caglayan (May 24 2022 at 13:58):

The files generated in _build/install are not known in advance by dune

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

view this post on Zulip Ali Caglayan (May 24 2022 at 14:00):

Because we shouldn't be relying on the install dir

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

view this post on Zulip Ali Caglayan (May 24 2022 at 14:01):

Emilio Jesús Gallego Arias said:

as we discussed, we can:

  1. patch findlib to support META.coq-core without a directory file
  2. patch dune to support runtime-library
  3. depend on _install files

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

view this post on Zulip Enrico Tassi (May 24 2022 at 14:58):

Please don't fork findlib, fix dune instead.

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

view this post on Zulip Enrico Tassi (May 24 2022 at 15:17):

I opened one, please move the discussion there

view this post on Zulip Gaëtan Gilbert (May 24 2022 at 15:39):

(https://github.com/ocaml/dune/issues/5767)

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

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

view this post on Zulip Ali Caglayan (May 24 2022 at 16:21):

That is the only way to guarantee the META file in _build/install gets generated

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

view this post on Zulip Ali Caglayan (May 24 2022 at 16:23):

We don't need to build the entire package if we depend on META.coq-core.

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

view this post on Zulip Ali Caglayan (May 24 2022 at 16:24):

That way you can have finer dependencies.

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 16:43):

That seems to me like a fine dep?

view this post on Zulip Ali Caglayan (May 24 2022 at 16:45):

Compare that with a possible (package coq-core.plugins.ltac).

view this post on Zulip Ali Caglayan (May 24 2022 at 16:46):

Dune can only have targets in the install directory through the (package ) stanza

view this post on Zulip Ali Caglayan (May 24 2022 at 16:46):

If you try %{lib:coq-core:META} you will get a not found error

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

view this post on Zulip Ali Caglayan (May 24 2022 at 16:52):

https://www.youtube.com/watch?v=HMqZ2PPOLik

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 16:54):

for the engine are regular rules

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 24 2022 at 16:55):

let me rephrase

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

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

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

view this post on Zulip 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: Feb 05 2023 at 23:30 UTC