[cmdline] use / in -print-mod-uid as dir separator on windows

[gares]

@MSoegtropIMC I've opted for the most conservative solution, I've flipped \ for / only in this option

Fix #13827

[MSoegtropIMC]

To be extra safe, you might want to check for files starting with \. This is fairly rare in Windows, one typically either uses relative paths or has a drive letter as well. C:/a/b works, a/b works, but /a/b can lead to interesting (very hard to debug) effects. I would consider throwing an error (or a warning) that one should either use relative paths or absolute paths with a drive letter.

[ejgallego]

Umm, the below code is already using Filename.concat which should do the right thing on Win32, so this seems wrong. Looking at the original bug, the problem seems to be in the Makefiles that mess with quoting, so it seems to me that the problem should be handled there.

In fact, this whole operation get_native_name seems to be ultra-costly, as it loads the whole summary, etc... the name of the native file can be easily computed without calling Coq [this is what we do in Dune] and indeed it seems like a better approach to me.

[gares]

In fact, this whole operation get_native_name seems to be ultra-costly, as it loads the whole summary, etc... the name of the native file can be easily computed without calling Coq [this is what we do in Dune] and indeed it seems like a better approach to me.

Are you saying that you coded, in dune, the whole -R and -Q resolution strategy?

[ejgallego]

No, dune already knows about these flags natively, so the operation of producing the name for native is quite easy:

https://github.com/ocaml/dune/blob/86522e99241cea205cc3202e419e6a6e003cc3e8/src/dune_rules/coq_module.ml#L43-L47

Indeed having a bit more information about library resolution would be very interesting as it would solve the current problem of having to generate all source files before calling coqdep, but that's offtopic here.

As far as I can see the bug is a bug in the Makefiles, that are quoting incorrectly somewhere, so IMO it should be solved there, not in Coq which is doing the right thing. [If filename.concat is buggy upstream that's a different story, but then we should provide our own, not hack ad-hoc here]

[gares]

Well, Filename would spit / if it did detect cygwin, but it does not. The "problem" is that we require a unix environment to run coq_makefile, but coq itself is compiled to also work without cygwin (so filename spits \ which is the default on windows). Given that this option is only used by coq_makefile I think it is safe (as ci shows) to flip the \ to /.

[gares]

To be extra safe, you might want to check for files starting with .

Out of inspiration I replaced (.)\ with \1/, hope it covers all your weird cases

[ejgallego]

It seems that the problem here is that the makefiles are incorrect w.r.t. quoting, so instead of this hack we should fix the makefiles instead to preserve the \.

[ejgallego]

Well, Filename would spit / if it did detect cygwin, but it does not.

The problem is not that thing work when / is used and don't when \ is, but that coq_makefile is eating the \ symbol altogether, this points to broken quoting, which should be solved in the makefiles themselves [likely other stuff is broken such as spaces]

[silene]

This pull request is a one-liner. Either we apply it or we close it. Keeping it as a draft forever is just a waste of time.

[SkySkimmer]

In https://github.com/coq/coq/wiki/Coq-Call-2021-11-10 we said we would go with this solution

[ppedrot]

@SkySkimmer don't you want to assign and merge this one? It has been lingering quite a bit.

[ppedrot]

Since we collectively agreed on merging this I don't see any point in keeping this around. Let's fire and forget.

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: You can't merge the PR because some changes are requested.

collective agreement

[ppedrot]

@coqbot merge now