Build error with CI / opam-build (dev, ubuntu-latest) (pull_request)

[jdchristensen]

The build error is:

 Error: - Error: Required library Basics matches several files in path (found
  - /home/rocq/.opam/4.14.2+flambda/.opam-switch/build/coq-hott.dev/_build/default/theories/Basics.vo and
  - /home/rocq/.opam/4.14.2+flambda/lib/coq/theories/Program/Basics.vo).

This must be related to the changes to Coq about not accepting ambiguous path names. We could probably work around it by changing Basics to HoTT.Basics everywhere, but that's annoying. Can we instead remove Program or maybe all of coq/theories from the search path somehow?

@Alizter

[jdchristensen]

If I add

-arg -exclude-dir -arg Program

to the _CoqProject file, it removes Coq.Program from the LoadPath. But this isn't very satisfactory as it is too vague; it will exclude any directory called "Program", not just coq/theories/Program. Moreover, this is just one of many things in the LoadPath that we don't want (see below). How do we exclude all of them (or maybe all but a small subset)? Note that Remove LoadPath <string> was removed from a recent Rocq version...

Should we just bite the bullet and add From HoTT ... before all of our Require lines to avoid ambiguity? It's pretty annoying to have to do this across a large development.

Coq /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories
Coq.Arith /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Arith
Coq.Array /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Array
Coq.Bool /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Bool
Coq.Classes /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Classes
Coq.Compat /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Compat
Coq.FSets /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/FSets
Coq.Floats /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Floats
Coq.Init /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Init
Coq.Lists /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Lists
Coq.Logic /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Logic
Coq.MSets /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/MSets
Coq.NArith /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/NArith
Coq.Numbers /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers
Coq.Numbers.Cyclic /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Cyclic
Coq.Numbers.Cyclic.Abstract
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Cyclic/Abstract
Coq.Numbers.Cyclic.Int63
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Cyclic/Int63
Coq.Numbers.Integer /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Integer
Coq.Numbers.Integer.Abstract
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Integer/Abstract
Coq.Numbers.Integer.Binary
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Integer/Binary
Coq.Numbers.Integer.NatPairs
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Integer/NatPairs
Coq.Numbers.NatInt /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/NatInt
Coq.Numbers.Natural /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Natural
Coq.Numbers.Natural.Abstract
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Natural/Abstract
Coq.Numbers.Natural.Binary
  /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Numbers/Natural/Binary
Coq.PArith /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/PArith
Coq.Program /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Program
Coq.QArith /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/QArith
Coq.Reals /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Reals
Coq.Reals.Abstract /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Reals/Abstract
Coq.Reals.Cauchy /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Reals/Cauchy
Coq.Relations /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Relations
Coq.Setoids /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Setoids
Coq.Sets /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Sets
Coq.Sorting /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Sorting
Coq.Strings /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Strings
Coq.Structures /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Structures
Coq.Unicode /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Unicode
Coq.Vectors /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Vectors
Coq.Wellfounded /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/Wellfounded
Coq.ZArith /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/ZArith
Coq.btauto /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/btauto
Coq.derive /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/derive
Coq.extraction /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/extraction
Coq.funind /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/funind
Coq.micromega /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/micromega
Coq.nsatz /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/nsatz
Coq.omega /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/omega
Coq.rtauto /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/rtauto
Coq.setoid_ring /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/setoid_ring
Coq.ssr /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/ssr
Coq.ssrmatching /home/jdc/scratchy/.opam/8.20-4.14.1/lib/coq/theories/ssrmatching

[jdchristensen]

@Alizter Any ideas? The build errors are annoying, so I'd like to fix this.

[Alizter]

@jdchristensen I'll try to take a look this weekend.

[jdchristensen]

I tried adding

-arg -exclude-dir -arg Program

to _CoqProject, but this caused a problem because SetoidRewrite.v indirectly uses this part of the standard library.

Is there a way to only exclude Program from the search path in the core library? Or is there another quick solution?

If not, I guess we'll need to put From HoTT everywhere?

Any thoughts, @Alizter ?