Split boolp, classical_sets,... in a new mathcomp-classical package

[proux01]

Fixes #550

Classical currently contains boolp and classical_sets, we may also consider adding functions and signed there.

[affeldt-aist]

we may also consider adding functions and signed there.

I would maybe refrain to do so for now because we didn't have (yet?) explicit requests for them and functions.v requires more dependencies and this has consequences on compilation time.

[CohenCyril]

Actually, I would rather draw the line now, and dispatch to the new package anything that does not strictly pertain to topology/calculus/analysis, rather than adjust later and cause further changes in the dependencies of client packages.

[proux01]

@CohenCyril done. We thus have in classical:

• boolp.v
• classical_sets.v
• cardinality.v
• ereal.v
• forms.v
• fsbigop.v
• functions.v
• mathcomp_extra.v
• nngnum.v
• nsatz_realtype.v
• posnum.v
• prodnormedzmodule.v
• reals.v
• Rstruct.v
• signed.v
• all_classical.v

and in main package:

• landau.v
• Rstruct.v
• topology.v
• normedtype.v
• realfun.v
• sequences.v
• exp.v
• trigo.v
• esum.v
• set_interval.v
• lebesgue_measure.v
• derive.v
• measure.v
• numfun.v
• lebesgue_integral.v
• summability.v
• altreals/xfinmap.v
• altreals/discrete.v
• altreals/realseq.v
• altreals/realsum.v
• altreals/distr.v

@affeldt-aist points are valid though:

• compilation time of classical here is around 2min40s whereas boolp and classical alone only take 10s (however, that compilation time is comparable to mathcomp-algebra which is a dependency anyway, so that's probably acceptable)
• this adds HB as a dependency (which will be a dependency of MC 2.0 but whose OPAM package takes some time to compile (maybe because it runs tests by default))

[affeldt-aist]

what about the near tactic?

[proux01]

It is in topology.v and seem very related to topology IINM.

[affeldt-aist]

i think that at some point it was scheduled to replace bigenough

[CohenCyril]

i think that at some point it was scheduled to replace bigenough

it is, actually near is neither analysis nor classical 😄

[proux01]

@affeldt-aist has a good point that mathcomp-classical may, in the current state of the PR, be larger than what @strub initially requested.

What about cutting it in three instead?

• mathcomp-classical: with boolp and classical_sets, only requiring mathcomp-ssreflect
• mathcomp-reals: everything else not strictly pertaining to topology/calculus/analysis, requiring mathcomp-algebra and HB
• mathcomp-analysis: topology/calculus/analysis

[CohenCyril]

What about cutting it in three instead?

• mathcomp-classical: with boolp and classical_sets, only requiring mathcomp-ssreflect
• mathcomp-reals: everything else not strictly pertaining to topology/calculus/analysis, requiring mathcomp-algebra and HB
• mathcomp-analysis: topology/calculus/analysis

I disagree with this. I have no objection to merge reals and analysis, but I believe that:

• boolp.v
• classical_sets.v
• cardinality.v
• fsbigop.v
• functions.v (not in mathcomp just because of HB + a light separation between the constructive and classical part should be done)
  belong to classical.

On the other hand forms.v (PR in progress for a while) and mathcomp_extra.v (easy stuff) have to be merged in mathcomp.
Also nngnum.v, posnum.v and signed.v do belong to mathcomp too.

EDIT:
Finally, the near tactics do not belong to analysis nor do they belong to classical... and should thus be extracted from the repo...

@affeldt-aist has a good point that mathcomp-classical may, in the current state of the PR, be larger than what @strub initially requested.

The only reason not to make it bigger is to avoid delay. I advocate to be finer than lazy (in a CS way not a judgmental way)

[CohenCyril]

We should discuss this at the next mc analysis meeting

[proux01]

So, here is a classical package with only

• boolp.v
• classical_sets.v
• cardinality.v
• fsbigop.v
• functions.v
• the part of set_interval.v that doesn't depend on reals or ereal

The classical package depends on HB (because of functions) but I think it's fine as MC 2.0 will depend on it anyway.

Reals and ereal should probably go in another separate package but I think this belongs to a further PR.
BTW, ereal should maybe be split between its classic and non classic part.

[CohenCyril]

Sorry for the delay. This looks nice. We also need to take care of the nix packages when we do this.

[proux01]

Rebased (hope will manage to merge this "soon", because those rebases are rather painful)

[affeldt-aist]

Rebased (hope will manage to merge this "soon", because those rebases are rather painful)

Agreed. We can maybe merge the easy PRs in the pipeline that touch the relevant files and then make this PR the top priority, so that it can be merged by the next meeting.

[proux01]

CI green, this requires:

• for Nix: Split coqPackages.mathcomp-analysis NixOS/nixpkgs#184961 on nixpkgs, then Test split_mathcomp_analysis coq-community/coq-nix-toolbox#117 on coq-nix-toolbox (we could then update coq-nix-toolbox here and remove the overlays)
• for OPAM: a PR on extra-dev

[CohenCyril]

Hi @proux01 the overlays should be unnecessary (since you merged the nixpkgs pr), however this made me noticed that a mathcomp-analysis-single package would be convenient for dev and CI purposes (as in /~https://github.com/NixOS/nixpkgs/blob/2a48d5921115733b840e651b843a3c7c515db582/pkgs/development/coq-modules/mathcomp/default.nix#L54).
I'm sorry this is undocumented. The purpose of this package is to be able to build everything in a single make

[proux01]

Hi @proux01 the overlays should be unnecessary (since you merged the nixpkgs pr)

@CohenCyril right, removed. Ci is as green as expected (there is still this master failure with this strange dependency to real-closed that we should fix, but that's orthogonal to the current PR).

however this made me noticed that a mathcomp-analysis-single package would be convenient for dev and CI purposes (as in /~https://github.com/NixOS/nixpkgs/blob/2a48d5921115733b840e651b843a3c7c515db582/pkgs/development/coq-modules/mathcomp/default.nix#L54). I'm sorry this is undocumented. The purpose of this package is to be able to build everything in a single make

Done there: NixOS/nixpkgs#193162 (and successfully tested on the coq-nix-toolbox there: coq-community/coq-nix-toolbox#122)

I'll do the OPAM packages in extra-dev once this is merged

[proux01]

@CohenCyril Nix CI green (the Docker CI failure seems unrelated and is likely due to this: math-comp/math-comp#924)
So I think the current PR can be merged (I'll then update the extra-dev OPAM packages).

[proux01]

@CohenCyril CI "green" (the Docker failures are exepected due to the exhaustion of gitlab credits), including the mathcomp-analysis-single package.

[CohenCyril]

Fantastique !

[gares]

Classy ;-)

[proux01]

OPAM package done, we should be all set.