Stream: Dune devs & users

Topic: Dune on Windows

Michael Soegtrop (Nov 17 2023 at 14:07):

@Emilio Jesús Gallego Arias : I have substantial problems with dune on Windows. The status is:

• With dune 3.10 several projects fail to build on Windows, apparently cause of path issues - we discussed a while back that Windows APIs actually do support / and \ as path separator, and dune did also support this in 3.7, but as far as I know no longer in 3.10

• With dune 3.7 some other projects don't build any more, which apparently need a more recent dune - coq-elpi is an example which has some findlib issues with elpi packages with dune 3.7

How can we get this fixed?

Ali Caglayan (Nov 17 2023 at 23:43):

I'm interested in fixing these, would you be able to give some further details?

Ali Caglayan (Nov 17 2023 at 23:45):

It would help if you could give some concrete examples of these problems and I will try to replicate them on Windows.

Ali Caglayan (Nov 17 2023 at 23:47):

It would also be helpful to know if this is cygwin or native windows via dkml or something.

Ali Caglayan (Nov 18 2023 at 23:37):

Hi @Michael Soegtrop as I've said on GitHub, this appears to be due to coqdep reporting C:/foo/bar as C/:/foo/bar going back to 8.18-8.16 at least. The only reason this is now a problem is because we started passing -boot in order to get the complete dependencies, including the implicit ones from the stdlib. I'm a little unsure why this issue hasn't been a problem for other projects in the platform.

As mentioned, the best course of action in my opinion would be to patch coqdep in the Coq platform yourselves in order for it to mention the correct path. Once that is done, Dune should recognize C:/ as being absolute, as it already does for the OCaml logic.

Ali Caglayan (Nov 18 2023 at 23:38):

Let me know if this sounds good to you and if you have any more questions about Dune.

Michael Soegtrop (Nov 19 2023 at 08:06):

@Ali Caglayan : I anyway need to patch coqdep, so adding another is no issue. Can you supply me a patch or point me to the respective code?

Ali Caglayan (Nov 19 2023 at 10:20):

I'm not fully certain how the coqdep implementation works, but all the relevant code is in tools/coqdep/lib. From an initial reading, there appear to be some hacks relied on which might be a cause. cc @ejgallego in case he can give a more informed view.

Ali Caglayan (Nov 19 2023 at 14:45):

I had a look and https://github.com/coq/coq/blob/master/tools/coqdep/lib/makefile.ml looks very suspect to me. It seems : is being escaped for makefile which is definitely not something we want in a path.

Ali Caglayan (Nov 19 2023 at 17:04):

So coqdep always escapes the output for makefile, which isn't great when using Windows paths outside of makefiels.

Ali Caglayan (Nov 19 2023 at 17:05):

One solution we could do is to add an option to coqdep that prevents escaping in the output and then modify Dune so that it passes that option to coqdep.

Ali Caglayan (Nov 19 2023 at 17:05):

Another solution would be to add some preprocessing to the output of coqdep inside Dune directly.

Ali Caglayan (Nov 19 2023 at 17:06):

The latter seems simpler however the former seems more "correct".

Ali Caglayan (Nov 19 2023 at 17:07):

@Michael Soegtrop Let me know which you prefer and I will try to write the patches.

Michael Soegtrop (Nov 20 2023 at 11:11):

Still pondering over it ...

Michael Soegtrop (Nov 20 2023 at 11:15):

What I don't quite understand is how the escaping \ are converted to /. I guess this is the real bug in coqdep. Depending on how things are called (how much shell expansion is in the way) a \ escaping of : might not hurt.

I hope that there is a proper hack free way of doing this - I try to figure it out.

Michael Soegtrop (Nov 20 2023 at 11:41):

@Ali Caglayan : after pondering over this a bit more, my colusions are:

• coqdep outputs path like C\:\cygwin64_coq\ not C/:/cygwin64_coq/ - you posted this differently in github and in the discussion here
• looking at the coqdep escaping code you linked, this output is correctly make escaped and the only way it can be (besides using / for \ as separator). But according to make rules the \ in front of the : has to be there, and using \ with a non special symbol after it is OK.

What is not so clear to me is what the connection between dune and coqdep is. Does dune read in the coqdep generated make dependency files? If so, I would say the conclusion is that dune does not parse these files properly (according to the escaping rules of make).

Ali Caglayan (Nov 20 2023 at 12:57):

Sorry about being imprecise earlier. I mean to write C\:\foo\bar.

Ali Caglayan (Nov 20 2023 at 13:07):

Dune calls coqdep in order to determine the dependencies between .v files. However the output of coqdep was previously (wrongly) assumed to be an unescaped makefile rule.

Ali Caglayan (Nov 20 2023 at 13:09):

So my two solutions above address this issue in two different ways:

1. Add -no-escape option to coqdep and always use that with Dune
2. Improve Dune's parsing of escaped makefile rules.

I prefer 1 over 2, but practically 2 is easier.

Ali Caglayan (Nov 20 2023 at 13:12):

I'll prepare a PR for Dune that correctly parses escaped output from coqdep (2) that you can later use as a patch.

Michael Soegtrop (Nov 20 2023 at 13:45):

@Ali Caglayan : IMHO solution 2 is the correct solution. Makefiles should have a well defined syntax and I don't think it is a good idea to introduce new variants of this syntax. We should stick to the syntax as it is defined. This means the issue is with dune and should be fixed there.

Michael Soegtrop (Nov 20 2023 at 13:45):

I btw. reopened the github issue.

Ali Caglayan (Nov 20 2023 at 13:46):

Yes, I saw. I also added some more information there. I am currently looking into a patch that will parse this output correctly on Windows.

Ali Caglayan (Nov 20 2023 at 13:47):

The reason I prefer 1 by the way, is because escaping then unescaping paths seems like a waste of time if the tool could be configured to just output wtihout the escaping.

Michael Soegtrop (Nov 20 2023 at 13:48):

Perfect, thanks! I am looking forward to it. If you want to test it in Coq Platform CI, please base your branch on https://github.com/MSoegtropIMC/platform/tree/split-mathcomp.

Ali Caglayan (Nov 20 2023 at 13:53):

There is one thing I am still confused about, and that is the occurance of \\\\ in the Windows paths. When reading the coqdep code, it seemed to me that these were also escaped but you mentioned that this was not the case?

Ali Caglayan (Nov 20 2023 at 13:53):

I guess it doesn't really matter in the end since it is harmless. I will just fish for \: and replace it with :.

Michael Soegtrop (Nov 20 2023 at 14:12):

I expect that this is sufficient. Coq itself has very stringent requirements on file and path names (even _ is not allowed afair), so there is no reason to expect strange paths with special characters in them - maybe ' might be an issue ...

Gaëtan Gilbert (Nov 20 2023 at 14:16):

that's only true for paths relative to some -Q / -R, the absolute path prefix can be anything
ie -Q "foo bar/_/random control characters/" MyTheory can happen (probably not well supported though, especially I expect spaces get mangled by going through the makefile)

Ali Caglayan (Nov 20 2023 at 14:29):

There are tests in the test-suite (misc?) that try some unicode paths from a user in Greece. I believe these are escaped.

Emilio Jesús Gallego Arias (Nov 21 2023 at 14:24):

Hi folks, thanks for looking into this.

Emilio Jesús Gallego Arias (Nov 21 2023 at 14:26):

It seems to me that the right thing to do here is to have Dune understand coqdep escaping.

As of today "makefile" format is the official dune / coqdep interface. I agree with Ali that it is not optimal, but back in the day was the quicker way to make it work, and note that Dune does the same for ocamldep, so actually I just adapted the ocamldep parsing code.

Michael Soegtrop (Nov 21 2023 at 14:36):

@Emilio Jesús Gallego Arias : do you know if ocamldep works on Windows or what it outputs for Windows absolute paths?

Emilio Jesús Gallego Arias (Nov 21 2023 at 16:47):

ocamldep works on windows, I'm unsure what paths it outputs tho.

Emilio Jesús Gallego Arias (Nov 21 2023 at 16:47):

Dune doesn't use path resolution from ocamldep, but instead calls it with the -module option and performs path resolution itself

Emilio Jesús Gallego Arias (Nov 21 2023 at 16:48):

that's a thing that has been asked many times for the Coq side

Michael Soegtrop (Nov 22 2023 at 07:55):

Well coqdep did also work on Windows until we started to pass absolute paths via dune. As long as one stays in the realm of relative paths, nothing bad will happen. The question was: does ocamldep work when it has to handle absolute Windows paths.

Ali Caglayan (Nov 25 2023 at 15:40):

@Michael Soegtrop This isn't a problem for ocamldep because it is used with the -modules field, essentially becoming a simple lexer for modules. It is then upto Dune to resolve the module names to known libraries etc. Coqdep on the other hand is actually going and finding the exact .vo files you need to depend on.

We have discussed in the past having a -modules mode for coqdep https://github.com/ocaml/dune/issues/5100. I even implemented such a library on the Dune side to do essentially what ocamldep -modules did, but there were some disagreements about the design (where does the code go and how do we share) and ultimiately it fizzled out. Since then we improved support for installed theories in Dune and coqdep is working pretty well. (modulo these windows issues).

Ali Caglayan (Nov 25 2023 at 15:42):

And if it wasn't clear, ocamldep -modules output looks like this:

ocamldep -modules bench/micro/fiber_bench.ml
bench/micro/fiber_bench.ml: Exn_with_backtrace Fiber Fun Int List Printexc Stdune

Last updated: Oct 13 2024 at 01:02 UTC