coq-mathcomp-reals package

[proux01]

Motivation for this change

New packages:

• coq-mathcomp-reals
  • all_reals.v
  • constructive_ereal.v
  • itv.v
  • nsatz_realtype.v
  • prodnormedzmodule.v
  • real_interval.v
  • reals.v
  • signed.v
• coq-mathcomp-altreals
  • altreals/dedekind.v
  • altreals/discrete.v
  • altreals/distr.v
  • altreals/realseq.v
  • altreals/realsum.v
  • altreals/xfinmap.v
• coq-mathcomp-reals-stdlib
  • Rstruct.v
• coq-mathcomp-analysis-stdlib
  • Rstruct_topology.v

Following discussions during last meeting https://github.com/math-comp/analysis/wiki/2024-10-10-Meeting
This is probably best inspected by commit.
Depends on: #1347 and #1348
If we agree on the principle, I'll do the changelog and packages / CI work.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• Nix packages
• make CI work (uses Nix packages)
• Opam packages (retrieve script from mathcomp)

• [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Should we also consider a package for altreals? It looks dependency on topology are not needed, see PR 1353.

[proux01]

Should we also consider a package for altreals? It looks dependency on topology are not needed, see PR 1353

This PR puts them in reals (sorry, I forgot the files in the top post description) but we could indeed make it an independent package, that would only depend on reals. No strong opinion on my side, altreals really feels to me like a never finished attempt not very useful in its current state, so I don't really care where it goes. If one day it provides an actual instance of realType, I guess we would be happy to have it in reals?

[affeldt-aist]

This PR puts them in reals (sorry, I forgot the files in the top post description)

I see. I should have double-checked the diff.

but we could indeed make it an independent package, that would only depend on reals.

Since there are admitted facts in altreal, that could be a nice way to quarantine them.

No strong opinion on my side, altreals really feels to me like a never finished attempt not very useful in its current state, so I don't really care where it goes. If one day it provides an actual instance of realType, I guess we would be happy to have it in reals?

I am not sure there is such a plan.

I am wondering whether Rstruct.v and Rstruct_topology.v should go together.
Of course, that will make the whole package depends on topology.v which is
maybe what you tried to avoid, but on the other hand, Rstruct_topology.v is so small,
yet I am unsure about potential for its extension. (Sorry, no concrete proposal here.)

[proux01]

Since there are admitted facts in altreal, that could be a nice way to quarantine them.

Ok done

No strong opinion on my side, altreals really feels to me like a never finished attempt not very useful in its current state, so I don't really care where it goes. If one day it provides an actual instance of realType, I guess we would be happy to have it in reals?

I am not sure there is such a plan.

Ok

I am wondering whether Rstruct.v and Rstruct_topology.v should go together. Of course, that will make the whole package depends on topology.v which is maybe what you tried to avoid, but on the other hand, Rstruct_topology.v is so small, yet I am unsure about potential for its extension. (Sorry, no concrete proposal here.)

I'd like to avoid that. A user wanting only reals but also working with Stdlib would then have to compile the entire Analysis.

[proux01]

So this is ready. Let me know if / when we merge so that I can update the nix toolbox at about the same time to minimize disruptions in CIs.

[affeldt-aist]

The packages all make sense, dependencies have been reduced, there is even a packager to facilitate releases, and cherry on top the nix expertise. This is great. Thank you.

[affeldt-aist]

For the changelog, the list up of the file movements summarized in the first item of the conversation is almost enough a documentation for the user I think.

[proux01]

Changelog done