Path conflict on theories/homotopy_theory/path.v with core ssreflect path.v

[MSoegtropIMC]

Recently the file

https://github.com/math-comp/analysis/commits/master/theories/homotopy_theory/path.v

was introduced. This produces a path conflict:

.../CP.2024.10.1~8.20~2025.01/lib/coq/user-contrib/mathcomp/analysis/homotopy_theory/path.vo and
.../CP.2024.10.1~8.20~2025.01/lib/coq/user-contrib/mathcomp/ssreflect/path.vo

e.g. in Finmap.v which contains

From mathcomp Require Import choice path finset finfun fintype bigop.

This has the effect that one can compile finmap only before mathcomp-analysis, but not after it. Maybe mathcomp-analysis depends on it, so that this cannot happen, but it is still bad and might break existing code.

I would suggest to rename this file.

[affeldt-aist]

Yes, we already identified the issue #1412 .
This PR to finmap math-comp/finmap#114 is partly addressing the issue
by removing the explicit Require Import to path.
But anyway the true solution in the current state is indeed to rename the file.
(Sorry for the inconvenience.)

[MSoegtropIMC]

The other option is to write in FinMap:

From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp.ssreflect Require Import choice path finset finfun fintype bigop.

[MSoegtropIMC]

And sorry for not searching the issues first.

[MSoegtropIMC]

IMHO it should be discussed in Zulip how mathcomp wants to handle this. Either one says From mathcomp Require is recommended - then duplicate files should be avoided, and this should be tested for.

Or one recommends to use a more specific require like From mathcomp.ssreflect Require - that is at least specify the top level module under mathcomp, so that file names need only be unique per module.

I would think long term the second solution is more feasible, but both are fine.

[CohenCyril]

Either one says From mathcomp Require is recommended - then duplicate files should be avoided, and this should be tested for.

This ☝️