search

math-comp / math-comp

Mathematical Components
https://math-comp.github.io
573 stars 112 forks source link

Old comments mentioning unsupported versions of Coq #606

Open pi8027 opened 3 years ago

pi8027 commented 3 years ago

Should we review, simplify, and/or remove them? https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/ssreflect/ssrAC.v#L70-L72 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/ssreflect/finfun.v#L18-L21 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L1856-L1858 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L3551-L3552 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/vector.v#L1384-L1386 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/field/fieldext.v#L1584-L1592

CohenCyril commented 3 years ago

Should we review, simplify, and/or remove them?

The short answer is yes we should review and simplify, remove what can be removed and open issues if things are still blocked.

pi8027 commented 3 years ago

Will do.

pi8027 commented 3 years ago

After #743, there are 4 remarks remaining:

finfun

https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/ssreflect/finfun.v#L18-L21 We cannot address this right now (#701).

ssralg

https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L1856-L1858 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L3551-L3552 I didn't manage to understand what are the issues here.

fieldext

https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/field/fieldext.v#L1584-L1592 There is still a minor performance issue here (Qed takes two seconds). I suggest investigating it in detail in MathComp 2.0.

pi8027 commented 3 years ago

I unassign me since I don't see any immediate fix for the remaining ones. I think we need a volunteer to look at ssralg.

ejgallego commented 3 years ago

Would be nice to ensure all the problems noted in the comment got an entry in Coq's test-suite