Clément Pit-Claudel (May 20 2020 at 02:20): 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
Emilio Jesús Gallego Arias (May 20 2020 at 09:28):@Clément Pit-Claudel that's bizarre, are you using the cache?
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?
Clément Pit-Claudel (May 20 2020 at 13:59):I don't think so? I'm just using dune build xyz
Emilio Jesús Gallego Arias (May 20 2020 at 14:02):You can check in your .config/dune/config file
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]
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.
Théo Zimmermann (May 22 2020 at 13:43):A lot? What features?
Clément Pit-Claudel (May 22 2020 at 13:45):Pattern rules, mostly.
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.
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"
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
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
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
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
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
Clément Pit-Claudel (May 22 2020 at 13:51):I had stuff for cross-theory dependencies, which is unneeded now
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
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
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
Emilio Jesús Gallego Arias (May 22 2020 at 13:51):I hope I can fix that in the next release
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...]
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 .))))
aha
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.
Clément Pit-Claudel (May 22 2020 at 13:54):Like, how do I save the pwd before I move to workspace_root?
Emilio Jesús Gallego Arias (May 22 2020 at 13:55):umm why you need the chdir ?
Clément Pit-Claudel (May 22 2020 at 13:55):For error messages. Otherwise they just mention the file name instead of the path
Emilio Jesús Gallego Arias (May 22 2020 at 13:55):ah, there is a bug open about that already
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
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
Emilio Jesús Gallego Arias (May 22 2020 at 13:56):there is this new subdir support tho that could help
Clément Pit-Claudel (May 22 2020 at 13:56):Aha! What is subdir? Or what hacks can I use? ^^
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
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 ^^
Emilio Jesús Gallego Arias (May 22 2020 at 13:59):What I did in my generator is actually to adjust the path
Emilio Jesús Gallego Arias (May 22 2020 at 13:59):similarly to what dune does internally for rules
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
Emilio Jesús Gallego Arias (May 22 2020 at 13:59):so rules where
Emilio Jesús Gallego Arias (May 22 2020 at 13:59):(chdir %{root} (run bin -o foo/bar))
Emilio Jesús Gallego Arias (May 22 2020 at 14:00):yeah that's a bit annoying
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?
Emilio Jesús Gallego Arias (May 22 2020 at 14:01):no, in that case my generator placed dune files inside the subdirs
Emilio Jesús Gallego Arias (May 22 2020 at 14:02):but was aware of the structure
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?
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.
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))))
I cannot find the issue where this problem was discussed
Emilio Jesús Gallego Arias (May 22 2020 at 14:08):maybe we just chatted in person about it [with the Dune devs]
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]
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
Emilio Jesús Gallego Arias (May 22 2020 at 14:11):well, actually I cannot see how your rule does work
Emilio Jesús Gallego Arias (May 22 2020 at 14:12):I mean, that rule you posted doesn't work, right?
Clément Pit-Claudel (May 22 2020 at 14:12):The -o . is broken, yup
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
Clément Pit-Claudel (May 22 2020 at 14:12):It works if you remove the chdir
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
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"
Emilio Jesús Gallego Arias (May 22 2020 at 14:12):as we did for the coq files
Emilio Jesús Gallego Arias (May 22 2020 at 14:13):but indeed you could have chdir do that for you
Emilio Jesús Gallego Arias (May 22 2020 at 14:13):indeed, does it work if you do -o %{path:.} ?
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
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
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)
Emilio Jesús Gallego Arias (May 22 2020 at 14:15):maybe %{dep:.} ?
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
Clément Pit-Claudel (May 22 2020 at 14:16):let me double-triple check
Clément Pit-Claudel (May 22 2020 at 14:17):I screwed up my initial testing
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
Clément Pit-Claudel (May 22 2020 at 14:17):Let me try with dep
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
Emilio Jesús Gallego Arias (May 22 2020 at 14:18):Does registering the dir as a dep create issues?
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
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:.}))))
is the rule for bigint.lv in place?
Clément Pit-Claudel (May 22 2020 at 14:22):It's a source file
Clément Pit-Claudel (May 22 2020 at 14:23):And it works fine if I remove the dep:.
Clément Pit-Claudel (May 22 2020 at 14:23):Just tried the trick of putting an absolute path in there, it works perfectly
Clément Pit-Claudel (May 22 2020 at 14:23):I think it's a good workaround for now
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/))))
Umm, see https://github.com/ocaml/dune/pull/944 , the reason given was that nobody used the path-no-dep
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
Emilio Jesús Gallego Arias (May 22 2020 at 14:25):I see the error, it is interpreting the directory as a file
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.
Rudi Grinberg (May 25 2020 at 19:07):Do we need a dune stream perhaps? :)
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"
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)
Théo Zimmermann (May 25 2020 at 19:19):I agree and I suggest calling it "Dune users & devs"
Théo Zimmermann (May 25 2020 at 19:20):You don't need me to create it, do you?
Karl Palmskog (May 25 2020 at 19:21):ah, I thought creation was limited, let me check
Théo Zimmermann (May 25 2020 at 19:22):It is restricted to "full members" which you become after a few days
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?
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...
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
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: Nov 29 2023 at 06:01 UTC