Error: file not available when depending on an external dep

[ejgallego]

Dune seems to error when dune build $file is called with $file being an absolute path towards a symlink.

Example with a trivial project that builds library foo:

$ dune clean
$ dune build /home/egallego/tmp/dune-bugs/ext/_build/install/default/lib/bar/META
Error: File unavailable:
/home/egallego/tmp/dune-bugs/ext/_build/install/default/lib/bar/META
$ dune build _build/install/default/lib/bar/META
$ # Success, now the first command also works

In Coq we've been getting the error here

https://github.com/ocaml/dune/blob/faa9254023cf64bf92c8e4c0ecfb0f0368bd993b/src/dune_engine/load_rules.ml#L291

quite often, see for example:

https://github.com/ejgallego/coq-universe/runs/6745395168?check_suite_focus=true#step:7:33

This started to happen because recently, coqdep is emitting a dep to a file in the _install layout.

Independently of the coqdep behavior, that we think is wrong, this is a bug in Dune. If the dep on the external file is not allowed, Dune should error at Action_build.dyn_deps.

Note that the missing file is a symlink.

Likely test case to reproduce:

• setup a rule using Action_builder.dyn_paths that depends on something on _build/install

[ejgallego]

cc: @Alizter

[ejgallego]

Note the file coqdep produces is an absolute path (that could be the point is confusing dune)

Ali mentioned that the problem could be related to the cache, that was my impression too, but I'm not sure.

[Alizter]

Windows builds and cache enabled seems to trigger it.

[ejgallego]

It can be triggered reliably c.f. https://github.com/coq/coq/issues/15608

[ejgallego]

We found more info on this, updating the issue.

[rlepigre]

I'm experiencing a similar problem, also in the context of a Coq project with plugins. Has anyone understood the problem yet? Is there a workaround?

[Alizter]

@rlepigre The issue for plugins should be fixed: https://github.com/ocaml/dune/pull/6167. It will be included in Dune 3.5 which is set to release soon.

[ejgallego]

I'm experiencing a similar problem, also in the context of a Coq project with plugins. Has anyone understood the problem yet? Is there a workaround?

What is your Declare ML Module ?

[ejgallego]

@rlepigre The issue for plugins should be fixed: #6167. It will be included in Dune 3.5 which is set to release soon.

I'm not sure that will fix that particular problem, in this case this is due to coqdep emitting the META dep.

[rlepigre]

What is your Declare ML Module ?

I have several plugins, and hence several Declare ML Module. They are all placed in the same opam package. So for each plugin my dune file looks something like this:

(library
 (name my_plugin)
 (public_name my_plugins.my_plugin))

And the corresponding declaration in a Coq file is:

Declare ML Module "my_plugin:my_plugins.my_plugin".

[ejgallego]

That's on 8.16 , right? What's the name of the META file that coqdep generates?

I'm afraid that we may want to patch coqdep so in legacy mode the meta file dep is not emitted. See declare_ml_to_file in tools/coqdep/lib/common.ml

[rlepigre]

Yes, on Coq 8.16.0. I'm not sure what the name of the generated META file is. How do I figure that out? I expected I could just look in the file.v.d file corresponding to the file.v file that has the Declare ML Module, but I see no META file.

[ejgallego]

I mean, what is the name of the file that dune crashes on?

But indeed I think we should write a patch for Coq 8.16.1 , see https://github.com/coq/coq/pull/16658

[ejgallego]

@rlepigre let me know if that PR fixes the problem for you.

[rlepigre]

Oh sorry. The error I get is something like:

Error: File unavailable:
/absolute/path/to/_build/install/default/lib/my_plugins/META

I'll try out the MR later and let you know. Thanks!

[ejgallego]

I see thanks, my PR should fix that for now, hopefully. The Dune bug should also be fixed of course.

[rlepigre]

@ejgallego I confirmed that your patch to Coq (or rather, my back-ported version of it) fixes my problem. Thanks! For reference, see https://github.com/coq/coq/pull/16664.

[ejgallego]

Glad to hear @rlepigre ; actually there is not a lot that we need to support the new findlib loading mode in Dune, main road block is https://github.com/coq/coq/issues/16571 but that should be not too hard to fix when we get a minute.