[coqdep] Don't "canonize" files.

[ejgallego]

"Canonization" is a fragile (and expensive) process, instead, we
require that files passed to coqdep match the layout given in the -R
/ -Q options.

[ejgallego]

For reference, the canonization tries to solve a hard to solve problem: make can't understand directory traversal properly, so for make foo/.. and . are different directories. The right way to solve this is for coqdep to do nothing with the paths, and just require users to input to coq_makefile consistent paths.

Note that make does recognize ./foo and foo as identical, and a few other ones.

See mit-plv/coqutil#67 for more info.

[gares]

foo/.. and . are not necessarily the same path if foo is a symlink. you have to look beyondthe syntax to know if it is the case.

[ejgallego]

Yes, indeed that's not the best example, but this is why canonization is a complex process. (And that's a big problem for submakefiles, dune has to deal with a lot of stuff so composition properly works due to adjusting paths)

It is better just to have the invariant that coq_makefile and coqdep don't do that, and just have to share the same path prefix, so we don't even try to understand if foo/.. and . are the same dir or not (without canonization, they are just not)

[Alizter]

Can you rebase and fix the CI?

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[SkySkimmer]

@coqbot run full ci

[ejgallego]

@SkySkimmer last time this PR was run indeed some users did rely on passing incorrect paths to Coq makefile but coqdep fixing them.

Maybe we should go ahead and do some overlays, I dunno.