Build failure with mathcomp-2.0.0

JasonGross commented 1 year ago

File "./mathcomp_compat/CommonSSR.v", line 84, characters 21-36:
Error: The reference ordinal_finType was not found in the current
environment.

What version of mathcomp should I be using? / Is there a way to make this compatible with 2.0.0?

ak-2485 commented 1 year ago

Hello! We're working on porting LAProof to MathComp 2.0.0 and will open a "mathcomp2" branch soon. LAProof was originally developed using the Coq platform 8.16~2022.09; the package versions can be found here: https://github.com/coq/platform/blob/main/doc/PackageTable~8.16~2022.09.csv.

JasonGross commented 1 year ago

Urgh, even when I downgrade to mathcomp<2, the build still fails:

File "./accuracy_proofs/mv_mathcomp.v", line 617, characters 6-16:
Error:
In environment
m : nat
A : 'M_m.+1
u : 'cV_m.+1
umax : R
Hequmax : umax = normv u
Unable to unify
 "(\big[Order.max/?M4802]_(i | ?M4803 i) ?M4804 i <=
   \big[Order.max/?M4802]_(i | ?M4803 i) ?M4805 i)%O = true" with
 "(\big[maxr/0]_(i < m.+1) Rabs ((A *m u) i 0) <=
   \big[maxr/0]_(i0 < m.+1) ((\sum_(j < m.+1) Rabs (A i0 j)) * umax)) = true".

Command exited with non-zero status 1
accuracy_proofs/mv_mathcomp.vo (real: 5.58, user: 4.93, sys: 0.38, mem: 921572 ko)

JasonGross commented 1 year ago

I've managed to get everything to build with #10, though

VeriNum / LAProof

Build failure with mathcomp-2.0.0 #5