@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
@Clément Pit-Claudel that's bizarre, are you using the cache?
@Clément Pit-Claudel @Clément Pit-Claudel that's bizarre, are you using the dune cache?
I don't think so? I'm just using dune build xyz
You can check in your .config/dune/config
file
Are you by any chance running two dune's in parallel ? This is currently racy, and not supported [plan to support this is underway]
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.
A lot? What features?
Pattern rules, mostly.
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
.
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"
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
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
Oh, interesting @Emilio Jesús Gallego Arias ! The warning there is a bit scary though
I'm in the process of getting rid of the makefiles, though, because with your latest changes 90% of the cruft is unnecessary
I don't think I'll go away in the short, lots of users
I had stuff for cross-theory dependencies, which is unneeded now
if it goes away will be in favor of a proper API to write your own rules
Support for cross-theory is still a bit sketchy in the sense that composition only works intra-scope
And stuff for dependencies between OCaml and Coq through extraction, which is gone too now
I hope I can fix that in the next release
Yeah not a lot missing other than improving composition support, and likely having better rules [quick, we can call coqdep less often, etc...]
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 .))))
aha
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.
Like, how do I save the pwd before I move to workspace_root?
umm why you need the chdir ?
For error messages. Otherwise they just mention the file name instead of the path
ah, there is a bug open about that already
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
That's what the docs recommend in https://dune.readthedocs.io/en/stable/concepts.html#user-actions
there is this new subdir
support tho that could help
Aha! What is subdir? Or what hacks can I use? ^^
Not sure if it can help, https://dune.readthedocs.io/en/latest/dune-files.html?highlight=subdir#subdir
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 ^^
What I did in my generator is actually to adjust the path
similarly to what dune does internally for rules
so all Path.t
that you have in scope are adjusted when inside a chdir
so rules where
(chdir %{root} (run bin -o foo/bar))
yeah that's a bit annoying
Ah but then you'd put everything in a dune file next to dune-project?
no, in that case my generator placed dune files inside the subdirs
but was aware of the structure
I see https://github.com/ocaml/dune/issues/2856 , maybe we should forward there?
Completely forgot about this issue (and it looks like I dropped the ball on that one, woops). Thanks.
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))))
I cannot find the issue where this problem was discussed
maybe we just chatted in person about it [with the Dune devs]
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]
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
well, actually I cannot see how your rule does work
I mean, that rule you posted doesn't work, right?
The -o .
is broken, yup
The suggestion you make in the issue is good tho; as indeed chdir already has the capability to relocate paths
It works if you remove the chdir
yeah, you should relocate the path too, so you need to track the path in the generator
Otherwise you'd need to remap the .
to mean "what used to be .
before the chdir happened"
as we did for the coq files
but indeed you could have chdir do that for you
indeed, does it work if you do -o %{path:.}
?
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
indeed you want to run the command from the directory the dune-project
file is for error rep reasons
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)
maybe %{dep:.}
?
for files for sure you can make the rewriting from ./foo
to ./bar/foo
happen already
let me double-triple check
I screwed up my initial testing
Error: %{path:..} was renamed to '%{dep:..}' in the 2.5 version of the dune language
Let me try with dep
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
Does registering the dir as a dep create issues?
It gives me a weird error Error: No rule found for tests/_objects/bigint.lv
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:.}))))
is the rule for bigint.lv in place?
It's a source file
And it works fine if I remove the dep:.
Just tried the trick of putting an absolute path in there, it works perfectly
I think it's a good workaround for now
(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/))))
Umm, see https://github.com/ocaml/dune/pull/944 , the reason given was that nobody used the path-no-dep
indeed dirs are rarely used, so IMHO it could be added back as the support is there
I see the error, it is interpreting the directory as a file
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.
Do we need a dune stream perhaps? :)
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"
ping @Théo Zimmermann (who I believe would need to agree for the new stream to happen)
I agree and I suggest calling it "Dune users & devs"
You don't need me to create it, do you?
ah, I thought creation was limited, let me check
It is restricted to "full members" which you become after a few days
created it now, but I don't think I can change the current topic to this stream instead? Or was this a Zulip limitation?
perhaps I should have called it "Dune devs & users" for consistency, but regular users apparently can't edit stream names, hmm...
OK, I'll take care of these two things when I'm in front of a computer
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