dune does not recognise paths starting with C:/ as absolute on Windows

[MSoegtropIMC]

Expected Behavior

dune produces correct paths in Windows cygwin MinGW cross environments

Actual Behavior

Path normalization in dune produces invalid paths. The likely cause is that paths starting with C:/ are not recognized as absolute paths. Please note that Windows file APIs do accept / as path separator (since pretty much ever) without any pre processing (say by MinGW C library). So dune should support this as well.

Example paths produced in a Coq Platform 2023.11 / 8.18 build are:

src/C/bin/cygwin64_coq_platform/home/Michael/.opam/CP.2023.11.0~8.18~2023.11/lib/coq/theories/extraction/ExtrOcamlString.vo
src/C/bin/cygwin64_coq_platform/home/Michael/.opam/CP.2023.11.0~8.18~2023.11/lib/coq/theories/ZArith/ZArith.vo
theories/C/bin/cygwin64_coq_platform/home/Michael/.opam/CP.2023.11.0~8.18~2023.11/lib/coq-core/plugins/ltac/ltac_plugin.cmxs

these paths result in error messages like:

# 10 |  (modules :standard)
# 11 |  (flags -noinit -indices-matter -color on))
# Error: No rule found for
# theories/C/bin/cygwin64_coq_platform/home/Michael/.opam/CP.2023.11.0~8.18~2023.11/lib/coq-core/plugins/ltac/ltac_plugin.cmxs

A few notes:

• I am using a cygwin MinGW cross build environment. The produced dune is a MinGW exe, not a cygwin exe.
• paths usually use a mix of / and \ as path separators in such an environment

Reproduction

• follow these instructions to setup a Coq Platform build environment on Windows - select extent "basic".
• open a shell of the newly created cygwin (which has opam)
• opam install dune 3.10.0 and any of these packages:
  • coq-simple-io.1.8.0
  • coq-mathcomp-word.2.1
  • coq-hott.8.18

Specifications

$ dune --version
3.10.0

$ ocamlc --version
4.14.1

cygwin 64 bit on Windows 10, MinGW cross (that is using https://github.com/ocaml-opam/opam-repository-mingw)

[nojb]

The likely cause is that paths starting with C:/ are not recognized as absolute paths.

Do you have a theory as to why there are no colons : in the (incorrect) paths produced in your setup?

[MSoegtropIMC]

@nojb : no. But since the opam packages don't pass paths to dune, I expect that this are issues with normalising CWD.

Can someone point me to the path normalisation code in dune, so that I can review it? I might also search for it, but it is hard to tell if I get all of it.

[Alizter]

The path normalization code is in otherlibs/stdune/src/path.ml. I'm currently trying to setup Coq platform as per your instructions (thank you very much for detailed instructions by the way), and I will see what the issue is soon enough.

By the way, we very rarely normalize paths which is why I am a bit surprised this has happened. My original suspicion was if something changed in coqdep and it was feeding dune nonsense paths. But I have yet to find evidence for that.

Edit: FTR, what I wrote above is incorrect. There is no path normalization code in Dune because we don't do it. The most we have with path manipulation is reaching one directory from another which isn't used in this case. Generally, we are very careful with our path operations to make sure they are correct on all platforms and efficient.

[Alizter]

Here is what coqdep in Coq 8.18 is outputting:

  $ coqdep a.v -noinit -boot -R 'C:\cygwin64_coq\home\ali\.opam\CP.2023.03.0~8.17~2023.08\lib/coq/theories' Coq
  a.vo a.glob a.v.beautified a.required_vo: a.v C\:\cygwin64_coq\home\ali\.opam\CP.2023.03.0~8.17~2023.08\lib/coq/theories/Init/Prelude.vo
  a.vio: a.v C\:\cygwin64_coq\home\ali\.opam\CP.2023.03.0~8.17~2023.08\lib/coq/theories/Init/Prelude.vio

Newer versions of Dune started calling coqdep with -boot by default and passing the -R for Coq. The dependency on the stdlib is now being made explicit whereas previously it would have been implicit/undeclared leading to funky behaviour.

However now that we ask for an external dependency, coqdep appears to be outputting C\:\cygwin64_coq\ which is complete garbage and confuses Dune into thinking this is a relative path.

This also appears to be an issue on 8.17 and 8.16.

It therefore appears that coqdep never worked correctly when referencing external dependencies on cygwin which is somewhat surprising. I'm not particularly happy disabling -boot for cygwin users as this would lead to incorrect setups. Since this is only a Coq platform thing, would it be possible to patch the bug in coqdep yourselves so that it reports the correct path?

[MSoegtropIMC]

@Alizter : many thanks for the root cause analysis! So it is apparently and issue in coqdep and not in dune.

Since it is apparently not an issue in dune, I am closing this.

[MSoegtropIMC]

@nojb: I reopen this since an analysis showed that the produced path syntax C\:\cygwin64_coq\... appears to be the correct escaping in make files (and the dependency files generated by coqdep are in makefile syntax). The colon character is a special character in make and must be escaped. This is the reason for the strange looking C:\:\... The escaping code in coqdep is here and contains some explanations. Please note that according to this, the backskash itself need not be escaped in most cases.

So the root cause of the issue appears to be that dune does not properly unescape makefile syntax in dependency files.

[Alizter]

I am currently preparing a patch that you can use for Coq Platform. The relevant code is:

dune/src/dune_rules/coq/coq_rules.ml

Lines 438 to 456 in 7debf4e

	let parse_line ~dir line =
	match String.lsplit2 line ~on:':' with
	| None -> coqdep_invalid "split" line
	| Some (basename, deps) ->
	(* This should always have a file, but let's handle the error
	properly *)
	let target =
	match String.extract_blank_separated_words basename with
	| [] -> coqdep_invalid "target" line
	| vo :: _ -> vo
	in
	(* let depname, ext = Filename.split_extension ff in *)
	let target = Path.relative (Path.build dir) target in
	let deps = String.extract_blank_separated_words deps in
	(* Add prelude deps for when stdlib is in scope and we are not actually
	compiling the prelude *)
	let deps = List.map ~f:(Path.relative (Path.build dir)) deps in
	target, deps
	;;

I am already not so happy that we have to do any parsing of coqdep output as this is very fragile, but now we have to also take into account the escaping.

It would be great if coqdep had a machine readable output like canonical S-expressions so that we didn't have to do this. Alternatively, if we vendored some of the coqdep library and simply called it in OCaml, however this is fragile for other reasons.

In any case, adding the extra parsing steps here and in the platform seems the best and most practical way forward.

[MSoegtropIMC]

Indeed it would be an option to have an alternate output format for coqdep. What I wouldn't appreciate though is if we would introduce simplified variants of make file syntax in order to simplify the communication between coqdep and dune. We should always use standard formats - S expressions would be a good choice IMHO. I don't care which format we use, but let's stick to whatever standard we use.

[ejgallego]

Indeed the way coqdep constructs paths could be improved; it's been in my TODO for a while, but not happening any time soon due to lack of time.

@Alizter thank you very much, your patch is IMO the right thing to do. coqdep, as called by dune, outputs paths in Makefile format as correctly noted by @MSoegtropIMC ; thus, dune should unescape the strings assuming they come in Makefile format.

[nojb]

thus, dune should unescape the strings assuming they come in Makefile format.

Where can one find a specification of the format? I couldn't see anything related in the manual of GNU Make.

[MSoegtropIMC]

Indeed, as far as I can tell, the manual only says that # and a line trailing backslash can be escaped with a backslash. It is fairly obvious that a colon must be escaped if it appears in a target path - if make requires to escape it if it appears in a dependency I haven't tried.

The comment explaining escaping in coqdep was written by @ejgallego. Emilio: do you have a reference or evidence?

[ejgallego]

@MSoegtropIMC I'm unsure if that's what you are asking for, but the escape code for coqdep is here

https://github.com/coq/coq/blob/0c40866dc1b2f0c54c0f9bba4d965d961e6655cb/tools/coqdep/lib/makefile.ml#L18

Dune should be in sync with that code and unescape the paths properly.

[MSoegtropIMC]

@ejgallego : the question was if you have some references for the quoting rules in coqdep. There are some comments in the coqdep sources - from GIT history I guess by you - so I guess you have read about this somewhere. I couldn't fund much about this in the gnu make reference manual. Afaikt it only explains the escaping of \ and #.

[ejgallego]

The quoting rules were mostly added in Coq's commits:

• coq/coq@9a22ebe
• coq/coq@c6b7976

and to the best of my knowlegde, they remain unchanged.