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)