mxvec_norm error when building

[ianhhlee]

Build failure when Dune builds mxtopology.v line 1942, characters 23-35:

Error: In environment R : numDomainType m, n : nat x : `M(m.+1, n.+1) The term "(ord0, ord0)" has type "('I?n'.+1 * 'I_?n'0.+1)%type" while it is expected to have type "Total_sort ?T"

[strub]

Hi. What is your build environment? (Version of Coq + libraries)

[ianhhlee]

Followed the Readme.md

[LucianoXu]

I came up with the same error today. There seems a type error in mxtopology.v.

[zhou31416]

Hi, the problem is caused by the version of mathcomp-analysis. Please try the early version coq-mathcomp-analysis.0.5.2 to see if it works. The mathcomp-analysis is an ongoing project and have critical changes in each update.

[ianhhlee]

Using mathcomp-analysis 0.5.2 failed:

[ERROR] The compilation of coq-mathcomp-analysis.0.5.2 failed at "make -j1".

=== ERROR while compiling coq-mathcomp-analysis.0.5.2 ========================# context 2.1.3 | linux/x86_64 | coq-mathcomp-fingroup.1.14.0 | https://coq.inria.fr/opam/released#2022-09-29 14:50 path ~/_opam/.opam-switch/build/coq-mathcomp-analysis.0.5.2 command ~/.opam/opam-init/hooks/sandbox.sh build make -j1 exit-code 2 env-file ~/.opam/log/coq-mathcomp-analysis-2291-8cb6e0.env output-file ~/.opam/log/coq-mathcomp-analysis-2291-8cb6e0.out

output

[...] File "./theories/lebesgue_measure.v", line 133, characters 0-76: Warning: Casts are ignored in patterns [cast-in-pattern,automation] File "./theories/lebesgue_measure.v", line 133, characters 0-76: Warning: Casts are ignored in patterns [cast-in-pattern,automation] COQC theories/lebesgue_integral.v File "./theories/lebesgue_integral.v", line 201, characters 0-51: Error: apply-w-params

make[2]: [Makefile.coq:764: theories/lebesgue_integral.vo] Error 1 make[1]: [Makefile.coq:387: all] Error 2 make[1]: Leaving directory '/home/leehh/_opam/.opam-switch/build/coq-mathcomp-analysis.0.5.2' make: *** [Makefile.common:63: this-build] Error 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> ┌─ The following actions failed λ build coq-mathcomp-analysis 0.5.2

[LucianoXu]

A reinstallation may be helpful. You can try deleting the opam switch and the CoqQ repository. After that, clone the repository and create the switch again using the new command.

[ianhhlee]

Yes, that seems to have worked. At least for the local switch.