Accept \ in Windows pathnames in coq_project args

[jfehrle]

Fix regression from #14558. See here.

FYI: @Columbus240

[Alizter]

What happens on macos?

[jfehrle]

I took out $ for now, that likely won't come up too much on Windows. Very hard to test this because the dune build doesn't have a coq_makefile-prelude and building a modified version for Windows is a project (I rarely do this anymore). If it's not a fix, it is at least a step in the right direction.

[silene]

Since the Makefile generated by coq_makefile assumes that filenames do not contain any backslash, it does not seem to be a good idea to allow them inside _CoqProject.

[herbelin]

Shouldn't it be recommended to have _CoqProject independent of the platform? (And in particular to have a common separator for directories independent of the platform?)

[jfehrle]

The _CoqProject contains no backslashes:

-R . Jim

./JEF_test.v

When I try to open JEF_test.v in CoqIDE, it tries to read the _CoqProject file. I see this message flashed at the bottom of the CoqIDE window for 5 seconds (easily missed), and the buffer isn't created. (The message should be a lot more visible, noted in #15774.)

I expect this is because let f = CUnix.correct_path f' orig_dir in converts the relative path to an absolute path, which would introduce backslashes on Windows.

As I said, I think this is a step forwards and may be a fix, but I'm not going to do any more work on this now.

[herbelin]

I expect this is because let f = CUnix.correct_path f' orig_dir in converts the relative path to an absolute path, which would introduce backslashes on Windows.

I see, then, it is maybe enough that the check_filename is done on the f parsed in the _CoqProject file rather than the system-dependent f obtained by calling CUnix.correct_path!

[jfehrle]

Indeed, that just occurred to me. I updated the PR to do just that.

[silene]

I expect this is because let f = CUnix.correct_path f' orig_dir in converts the relative path to an absolute path

This is not quite correct. Function correct_path just prepends orig_dig to f' if f' is not an absolute path. But orig_dir itself is not an absolute path. In normal uses of coq_makefile, orig_dir should just be . or foo, not an absolute path. But I guess this assumption does not apply to Coqide and that is how an absolute path ends up here.

[jfehrle]

@silene Yeah, the routine won't make the path absolute unless the argument is absolute, but I expect it always converts / to \ on Windows, also problematic.

[jfehrle]

@herbelin @silene Who can/should be the assignee? I'd like to get this in 8.15.1.

[herbelin]

Will merge soon.

[herbelin]

@coqbot: merge now

[Columbus240]

Fix regression from #14558. See here.

FYI: @Columbus240

Good catch! Thanks for mentioning me.
If I'm not badly mistaken, the commit in this PR doesn't contain any functional change, except the lines with Minilib.log and the Parsing_error. So does this PR, as it is now, really fix the problem?

[jfehrle]

@Columbus240 Notice that I renamed the original f' to f, so the check_filename f behaves differently. Right?

If I'm not badly mistaken

Questions from others, even if mistaken, can be quite helpful. So no need to apologize with "badly". I usually make several mistakes before breakfast each day.

[Columbus240]

Both before and after the change, the code does the following (if I interpret it correctly): Take the first element of the list, and apply CUnix.correct_path _ orig_dir to it. Before the change, the first element of the list was called f' and the result was stored in f, after the change the first element of the list is called f and the result is stored in abs_f.
So I don’t see the functional change, because the renaming was done consistently.

[Columbus240]

I find abs_f is a slightly more evocative name, making the meaning of this variable a little more clear. So I have nothing against renaming.

[SkySkimmer]

So I don’t see the functional change, because the renaming was done consistently.

not quite, see eg line 259 (before PR) https://github.com/coq/coq/pull/15775/files#diff-13482a4486eee3b60cca52baee0cf046a6d89d7d009e314364bce73ee4377effL259

[Columbus240]

Ooh, that makes sense. Thanks for the explanation.