Stream: Dune devs & users

Topic: Dune complains about a missing file


view this post on Zulip Clément Pit-Claudel (May 20 2020 at 02:20):

@Emilio Jesús Gallego Arias Any idea what the following means? I'm seeing it from time to time:

$ dune build @all
File "examples/rv/dune", line 1, characters 0-0:
Error: File unavailable:
/home/clement/documents/mit/plv/koika/_build/default/coq/ProgramTactics.vo

Usually re-running fixes the issue

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2020 at 09:28):

@Clément Pit-Claudel that's bizarre, are you using the cache?

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2020 at 09:28):

@Clément Pit-Claudel @Clément Pit-Claudel that's bizarre, are you using the dune cache?

view this post on Zulip Clément Pit-Claudel (May 20 2020 at 13:59):

I don't think so? I'm just using dune build xyz

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2020 at 14:02):

You can check in your .config/dune/config file

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2020 at 14:02):

Are you by any chance running two dune's in parallel ? This is currently racy, and not supported [plan to support this is underway]

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:42):

Emilio Jesús Gallego Arias said:

Are you by any chance running two dune's in parallel ? This is currently racy, and not supported [plan to support this is underway]

It might have been that. I have a lot of Makefile cruft around calls to dune to work around things that dune doesn't support, at the moment.

view this post on Zulip Théo Zimmermann (May 22 2020 at 13:43):

A lot? What features?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:45):

Pattern rules, mostly.

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:47):

My set up is that I have a compiler written in Coq for a deep-embedded language. We use Gallina as a meta-programming language (e.g. we use a Definition to define a subprogram that can be resued in multiple places). To compile a new program you need to go from .v to .ml using extraction, and then pass that to the compiler that's been extracted to OCaml, to produce a .obj.

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:49):

So I use Make's pattern rules and templating features to generate rules that say "to get a .obj, run Coq on this file (it will produce a .ml), then compile this .ml into a .cmxs, then run our compiler on this cmxs"

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:49):

Sometimes you can workaround that by using the OCaml support inside dune files to generate some rules, example https://dune.readthedocs.io/en/stable/advanced-topics.html#ocaml-syntax

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:50):

With Dune I have to write a script that generates Dune files, and then re-run it every time I have a new example or program

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:50):

Oh, interesting @Emilio Jesús Gallego Arias ! The warning there is a bit scary though

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:50):

I'm in the process of getting rid of the makefiles, though, because with your latest changes 90% of the cruft is unnecessary

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:50):

I don't think I'll go away in the short, lots of users

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:51):

I had stuff for cross-theory dependencies, which is unneeded now

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:51):

if it goes away will be in favor of a proper API to write your own rules

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:51):

Support for cross-theory is still a bit sketchy in the sense that composition only works intra-scope

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:51):

And stuff for dependencies between OCaml and Coq through extraction, which is gone too now

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:51):

I hope I can fix that in the next release

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:52):

Yeah not a lot missing other than improving composition support, and likely having better rules [quick, we can call coqdep less often, etc...]

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:52):

I do have one problem though: I have a rule like this:

(rule
 (mode (promote (until-clean)))
 (deps
  (:ml example.ml)
  (:mli example.mli))
 (targets
   example.cpp
   example.dot
   example.hpp
   example.kpkg
   example.verilator.cpp
   cuttlesim.hpp
   Makefile
   verilator.hpp)
 (action
  (chdir %{{workspace_root}}
   (run cuttlec %{{ml}} -T all -o .))))

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:53):

aha

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:53):

In that rule the call to run produces plenty of outputs; it takes an output folder -o. Obviously . is wrong, but I couldn't figure out how to determine the path of the folder containing the current dune file.

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:54):

Like, how do I save the pwd before I move to workspace_root?

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:55):

umm why you need the chdir ?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:55):

For error messages. Otherwise they just mention the file name instead of the path

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:55):

ah, there is a bug open about that already

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:56):

yeah the ML API does understand paths properly, so you can do this; in the dune side tho you may need to use a hack

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:56):

That's what the docs recommend in https://dune.readthedocs.io/en/stable/concepts.html#user-actions

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:56):

there is this new subdir support tho that could help

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:56):

Aha! What is subdir? Or what hacks can I use? ^^

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:57):

Not sure if it can help, https://dune.readthedocs.io/en/latest/dune-files.html?highlight=subdir#subdir

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 13:58):

OK, looking at it right now. But I'm not sure I see it yet. It seems it will be equivalent to moving stuff to a dune file in a subdir, but I actually control those dune files, so I can put them wherever they need to be ^^

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:59):

What I did in my generator is actually to adjust the path

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:59):

similarly to what dune does internally for rules

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:59):

so all Path.t that you have in scope are adjusted when inside a chdir

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:59):

so rules where

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 13:59):

(chdir %{root} (run bin -o foo/bar))

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:00):

yeah that's a bit annoying

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:01):

Ah but then you'd put everything in a dune file next to dune-project?

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:01):

no, in that case my generator placed dune files inside the subdirs

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:02):

but was aware of the structure

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:02):

I see https://github.com/ocaml/dune/issues/2856 , maybe we should forward there?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:03):

Completely forgot about this issue (and it looks like I dropped the ball on that one, woops). Thanks.

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:07):

So this is what we generated before in Coq to avoid this issue:

(rule
 (targets Tactics.vo Tactics.glob Tactics.vos .Tactics.aux)
 (deps (:pp-file ../../theories/Init/Tactics.v)
       ../../theories/Init/Notations.vo ../../theories/Init/Logic.vo
       ../../theories/Init/Specif.vo)
 (action (chdir %{project_root} (run coqc -q -coqlib %{project_root} -noinit -R theories Coq -w +default theories/Init/Tactics.v))))

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:08):

I cannot find the issue where this problem was discussed

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:08):

maybe we just chatted in person about it [with the Dune devs]

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:09):

but indeed that's a real problem, however when the "plugin" API becomes available things should work well as they will re-use the ML handling of this which is preetty good [thou not perfect yet]

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:11):

Ah! I see what you mean. You're hardcoding the path because we know what it's going to be anyway, so no need to have dune compute it. That makes sense

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:11):

well, actually I cannot see how your rule does work

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:12):

I mean, that rule you posted doesn't work, right?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:12):

The -o . is broken, yup

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:12):

The suggestion you make in the issue is good tho; as indeed chdir already has the capability to relocate paths

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:12):

It works if you remove the chdir

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:12):

yeah, you should relocate the path too, so you need to track the path in the generator

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:12):

Otherwise you'd need to remap the . to mean "what used to be . before the chdir happened"

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:12):

as we did for the coq files

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:13):

but indeed you could have chdir do that for you

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:13):

indeed, does it work if you do -o %{path:.} ?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:13):

Okie dokie. You could stretch it further and even stop using %{project_root} in fact, since we know where that is as well, but I agree that it's cleaner with project_root

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:14):

indeed you want to run the command from the directory the dune-project file is for error rep reasons

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:14):

Emilio Jesús Gallego Arias said:

indeed, does it work if you do -o %{path:.} ?

No, I don't think so (I just tried it)

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:15):

maybe %{dep:.} ?

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:15):

for files for sure you can make the rewriting from ./foo to ./bar/foo happen already

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:16):

let me double-triple check

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:17):

I screwed up my initial testing

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:17):

Error: %{path:..} was renamed to '%{dep:..}' in the 2.5 version of the dune language

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:17):

Let me try with dep

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:18):

I think the issue is that dep registers and extra dependency. path-no-dep is what I need I think, but it doesn't exist anymore

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:18):

Does registering the dir as a dep create issues?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:20):

It gives me a weird error Error: No rule found for tests/_objects/bigint.lv

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:20):

For this concrete file:

(rule
 (mode (promote (until-clean)))
 (deps (:lv ../../bigint.lv))
 (targets
   bigint.cpp
   bigint.dot
   bigint.hpp
   bigint.verilator.cpp
   cuttlesim.hpp
   Makefile
   verilator.hpp)
 (action
  (chdir %{workspace_root}
   (run cuttlec %{lv} -T all -o %{dep:.}))))

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:22):

is the rule for bigint.lv in place?

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:22):

It's a source file

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:23):

And it works fine if I remove the dep:.

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:23):

Just tried the trick of putting an absolute path in there, it works perfectly

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:23):

I think it's a good workaround for now

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:23):

(rule
 (mode (promote (until-clean)))
 (deps (:lv ../../bigint.lv))
 (targets
   bigint.cpp
   bigint.dot
   bigint.hpp
   bigint.verilator.cpp
   cuttlesim.hpp
   Makefile
   verilator.hpp)
 (action
  (chdir %{workspace_root}
   (run cuttlec %{lv} -T all -o tests/_objects/bigint.lv/))))

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:24):

Umm, see https://github.com/ocaml/dune/pull/944 , the reason given was that nobody used the path-no-dep

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:24):

indeed dirs are rarely used, so IMHO it could be added back as the support is there

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2020 at 14:25):

I see the error, it is interpreting the directory as a file

view this post on Zulip Clément Pit-Claudel (May 22 2020 at 14:29):

Emilio Jesús Gallego Arias said:

I see the error, it is interpreting the directory as a file

Yes, my example isn't great, with the directory being named the same as a file. Basically I have tests/{a,b,c,d}, and I build tests/_objects/a/a{.cpp,.hpp,…}, tests/_objects/b/b{.cpp,.hpp,…}, etc.

view this post on Zulip Rudi Grinberg (May 25 2020 at 19:07):

Do we need a dune stream perhaps? :)

view this post on Zulip Karl Palmskog (May 25 2020 at 19:08):

I second a dune stream, since I have projects that use dune for both Coq and OCaml, which would not obviously fit in "Coq users"

view this post on Zulip Karl Palmskog (May 25 2020 at 19:09):

ping @Théo Zimmermann (who I believe would need to agree for the new stream to happen)

view this post on Zulip Théo Zimmermann (May 25 2020 at 19:19):

I agree and I suggest calling it "Dune users & devs"

view this post on Zulip Théo Zimmermann (May 25 2020 at 19:20):

You don't need me to create it, do you?

view this post on Zulip Karl Palmskog (May 25 2020 at 19:21):

ah, I thought creation was limited, let me check

view this post on Zulip Théo Zimmermann (May 25 2020 at 19:22):

It is restricted to "full members" which you become after a few days

view this post on Zulip Karl Palmskog (May 25 2020 at 19:23):

created it now, but I don't think I can change the current topic to this stream instead? Or was this a Zulip limitation?

view this post on Zulip Karl Palmskog (May 25 2020 at 19:28):

perhaps I should have called it "Dune devs & users" for consistency, but regular users apparently can't edit stream names, hmm...

view this post on Zulip Théo Zimmermann (May 25 2020 at 19:29):

OK, I'll take care of these two things when I'm in front of a computer

view this post on Zulip Notification Bot (May 25 2020 at 20:27):

This topic was moved here from #Coq users > Dune complains about a missing file by Théo Zimmermann


Last updated: Jun 03 2023 at 18:01 UTC