[dune engine] [bug] Error file unavaiable when an absolute path points to a symlink.

[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

This is where the error is raised:

dune/src/dune_engine/load_rules.ml

Line 291 in faa9254

| No_such_file -> report_user_error []

This seems like 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 for the error to be produced.

Likely test case to reproduce:

• setup a rule using Action_builder.dyn_paths that depends on something that is a symlink and uses an absolute path.

note: I have cleaned up this issue as the discussion was quite confusing due to some users hitting this bug + a Coq bug. The Coq bug is unrealted, this seems like a pure dune issue.

[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. coq/coq#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: #6167. It will be included in Dune 3.5 which is set to release soon.

[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 coq/coq#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 coq/coq#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 coq/coq#16571 but that should be not too hard to fix when we get a minute.