Building with COQ 8.19 results in `Error: A left-recursive notation must have an explicit level.` in `fingroup/presentation.v` about math-comp HOT 4 CLOSED

1.17 is indeed known not to compile with Coq 8.19, you should use 1.19.0 (or 2.2.0)
BTW, the easiest way to compile a release of mathcomp is to use OPAM (or Nix) which takes care of this kind of dependencies.

from math-comp.

@proux01 thanks, this is for the Void Linux repository so I have to build it :) 2.2.0 gives a different error:

COQC ssreflect/eqtype.v
File "./ssreflect/eqtype.v", line 3, characters 0-34:
Error: Cannot find a physical path bound to logical path
structures with prefix HB.

from math-comp.

Yes, 2.2.0 has additional dependencies: https://github.com/coq/opam/blob/master/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.2.0/opam

from math-comp.

Thanks @proux01 1.19 seems to build! I guess more work will be required for 2.2.0 :)) Thank you so much.

from math-comp.