Port to MathComp 2

[pi8027]

No description provided.

[proux01]

Apparently, the github action is missing something like opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

[pi8027]

I locally tested my patch with MathComp 2.0. So I'm ok with fixing that part of CI after the release of Algebra Tactics.

However, I still have to make it compatible with MathComp dev (2.1).

[pi8027]

If I do:

Set Printing All.
Check 10%:~R.

I get:

@intmul _ (GRing.one _) (@GRing.natmul _ (GRing.one _) (S (S (S (S (S (S (S (S (S (S O)))))))))))

Is this intentional? It just looks ridiculous to me...

[proux01]

That's indeed a bug:

About intmul.
(* Arguments intmul [R] (x n)%ring_scope *)

It should be Arguments intmul [R] x%ring_scope n%int_scope

[proux01]

If you have only non negative constants, just use 10%:R which is way less buggy.

[pi8027]

If you have only non negative constants, just use 10%:R which is way less buggy.

Well, but replacing intmul with natmul in an existing large proof may invite another issue.

[pi8027]

Anyway I did a minimal fix.

[proux01]

10%Z%:~R is a bit ugly but should work

[proux01]

@pi8027 I have a fix there: math-comp/math-comp#1086 but it may require an overlay for Apery (I don't know since Apery is not in mathcomp's CI currently). So I suggest the following course of action:

1. merge this
2. then I can reintroduce Apery in mathcomp's CI
3. I can merge Fix the scope of arguments of intmul math-comp/math-comp#1086 (potentially after an overlay here)

Let me know if that's ok for you or if you would prefer to go the other way round (i.e., merge math-comp/math-comp#1086 then adapt the current PR)

[pi8027]

Regarding number notations, I think we should do a performance comparison (timed diff) of apery before/after the introduction of number notations. Commit e40179eb4e8452250741f4ead570ea9dc2ec77e3 should work with MathComp 1.12 to 1.17, and would be suited for this benchmarking.

[pi8027]

Also, the build of Apery took about 5 minutes in CI before this PR (before MC2): https://github.com/coq-community/apery/actions/runs/6509030922/job/17679609794
However, now it takes about 10 minutes here. It might just be a global issue of HB/MC2 but it is quite concerning to me. (I think Assia spent a lot of time optimizing the compilation of Apery.)

[proux01]

Regarding number notations, I think we should do a performance comparison (timed diff) of apery before/after the introduction of number notations. Commit e40179eb4e8452250741f4ead570ea9dc2ec77e3 should work with MathComp 1.12 to 1.17, and would be suited for this benchmarking.

Being just a notation, I'm not expecting any significant performance impact, but sure, feel free to benchmark (I recommend using make -j1 TIMED=1 to have reasonnably reproducible results).

Also, the build of Apery took about 5 minutes in CI before this PR (before MC2): https://github.com/coq-community/apery/actions/runs/6509030922/job/17679609794 However, now it takes about 10 minutes here. It might just be a global issue of HB/MC2 but it is quite concerning to me. (I think Assia spent a lot of time optimizing the compilation of Apery.)

A factor 2 is along the lines of what we currently observe on both mathcomp itself and analysis: math-comp/hierarchy-builder#391 You can use the TIMED and TIMING options of coq_makefile https://coq.inria.fr/doc/V8.18.0/refman/practical-tools/utilities.html#timing-targets-and-performance-testing to find out if some lines are particular bottlenecks.

[pi8027]

Being just a notation, I'm not expecting any significant performance impact.

I think that turning 1 *~ Posz n into 1 *~ (1 *+ n) can be a source of noticeable slow down.

Unfortunately, I have been delaying many things because of Algebra Tactics. I cannot spend more time on this kind of maintenance work right now.

[proux01]

@pi8027 should we merge? this seems ready as far as I can see.