Integration of corn real numbers into Coq's standard library

[VincentSe]

This pull request introduced a constructive real numbers interface in Coq's standard library
rocq-prover/rocq#10632

It is compatible with corn's CReals interface, which opens a way to move corn's files about real numbers into Coq's standard library.

There is a problem of copyright though : corn is under the General Public License, whereas Coq is under the Lesser General Public License. Therefore we would need to change the copyright and license of all corn files that we copy inside Coq's stdlib, making them under LPGL. Also, the names of the authors would need to be removed from the source code files, to go into Coq's global CREDITS file.

There are 19 corn developper listed for the reals : Henk Barendregt, Luís Cruz-Filipe, Herman Geuvers, Mariusz Giero, Rik van Ginneken, Dimitri Hendriks, Sébastien Hinderer, Bart Kirkels, Pierre Letouzey, Iris Loeb, Lionel Mamane, Milad Niqui, Russell O’Connor, Randy Pollack, Nickolay V. Shmyrev, Bas Spitters, Dan Synek, Freek Wiedijk, Jan Zwanenburg.

Their copyright is declared to end in 2006, but still we need them to agree to such an integration.

Does anyone know how to reach them, and how to change corn's license for those files ?

[Zimmi48]

Dates in copyright headers do not mean that their copyright has come to an end but indicate the date of the works. So indeed, if Corn was to be relicensed, it would need an agreement from the all the copyright holders.

But I don't think that the license is the only blocker here: one important question is whether this proposal is something that the Coq development team will agree with. I can only encourage you to come to a working group to have this idea discussed (chances are that the next one will be held in Nantes though). I am personally very interested in this perspective.

Another point is that we are likely going to split the standard library into several packages in the future, so the fact that a part of it is under a different license may not necessarily turn out to be problematic.

[VincentSe]

@Zimmi48 I have never been invited to such a working group. When is the next one and how can I enter it ? Also, how do we add this question of the integration of Corn's reals to its agenda ?

[Zimmi48]

The working groups are public, anyone can come. This is the page to look for regarding its organization: https://github.com/coq/coq/wiki/Next-Coq-Working-Group
As you can see, the next one will be toward the end of September.

[Zimmi48]

The agenda is set by editing the wiki page.

[VincentSe]

@Zimmi48 Hello, the next proposed date for the working group is next Thursday and no choice has been made yet ? I need to book a hotel and a train...

[Zimmi48]

I'm sorry, I was so busy I forgot to inform you that the date has been set, and@mattam82 apparently forgot to update the wiki page 😕
The dates are October 1st and 2nd in Nantes. Enjoy if you are going! (Unfortunately, I won't be able to make it, even by visio 😞)

[VincentSe]

@Zimmi48 Nice... Yes I'll be there. Anything else I need to know to get there? Location? Digicode?

[Zimmi48]

This will probably be written in time on the wiki page. For now, there has been no such information.

[Zimmi48]

BTW if you want a slot to be devoted to a discussion on standard library's reals, you should add this point to the wiki page

[VincentSe]

Duplicate of #99