Stream: Constructive reals & analysis

Topic: New release of Corn?


view this post on Zulip Karl Palmskog (Sep 05 2020 at 06:47):

So will there be a new release of Corn for 8.12 etc.? Looks like the last release was in 2017.

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 09:03):

Vincent already created a tag for inclusion in the Coq platform 8.12.0: https://github.com/coq-community/corn/releases/tag/8.12.0. It might change though before the Coq platform release.

I must admit I didn't have time as yet to look into it - too busy with technical issues in the Coq platform and my main job.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 09:53):

I would consider the Platform and Coq opam archive separate at this point, so maybe @Vincent Semeria can comment on whether I can put this tag as a package in the opam archive?

view this post on Zulip Karl Palmskog (Sep 05 2020 at 09:54):

Also, I think the current license of Corn is GPL-2.0-only, right? (As opposed to GPL-2.0-or-later or something else entirely.)

view this post on Zulip Vincent Semeria (Sep 05 2020 at 10:00):

Yes you can put this tag as a package in the opam archive, and the current license is GPL-2.0-only thanks. Please let me know when you have delivered it.

view this post on Zulip Bas Spitters (Sep 05 2020 at 10:05):

In fact, we are in the process of cleaning up the licenses. Large parts of corn are MIT, but given the large number of contributors. It takes a while to sort this out.
@Karl Palmskog You previously suggested a LICENSE file with per file/per directory licenses. I think we could apply it to corn too, while we are sorting out the relicense issue.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:06):

@Bas Spitters per-file licensing is to me a "last resort". It makes it a nightmare legally to depend on a project.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:07):

you would also have to look very carefully what constitutes a derived work, since almost anything that in some way uses GPL'd code is GPL

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:08):

That said, I applaud efforts to make Corn MIT (or something more permissive), but maybe one can make separate packages with GPL/MIT parts?

view this post on Zulip Bas Spitters (Sep 05 2020 at 10:10):

We are trying to resolve the issue.
Corn being GPL only is incorrect, I think. Russell O'Connor contributed a lot to the library and explicitly licensed his code to be MIT.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:12):

well, it would still unfortunately require legal-technical analysis to tell if the code could fall under MIT. For example, can that code be built in isolation from other parts?

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:15):

Bas already saw this, but I expounded on the complexities of having GPL anywhere in a project in a recent coq-community issue: https://github.com/coq-community/manifesto/issues/114

view this post on Zulip Vincent Semeria (Sep 05 2020 at 10:16):

I worked several weeks to cut many GPL calls from Russell's MIT code. Russell's basic definitions of constructive real numbers do build in isolation now.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:18):

here is where the GPL kicks in again. Have you been in touch with Russell to re-license the code? Because when he first contributed it and used GPL'd code, it automatically became all GPL (at least to my understanding, Théo may be able to elaborate as well.)

view this post on Zulip Vincent Semeria (Sep 05 2020 at 10:19):

Russell's files all start with the MIT license, check for instance
https://github.com/coq-community/corn/blob/master/reals/fast/CRAlternatingSum.v

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:19):

yes, you can claim that your code is MIT, but that doesn't make it MIT if it uses GPL'd code anywhere

view this post on Zulip Vincent Semeria (Sep 05 2020 at 10:21):

Half of Russell's files still calls GPL code. The other half does not, and builds in isolation.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:22):

ahhh, I think I'm going to go nuts about GPL, I will just stay out of this, sorry, I'm just going to add the package with GPL-2.0-only in the license field.

view this post on Zulip Bas Spitters (Sep 05 2020 at 10:24):

What happens with a GPL license if it is not enforced? The team knew about the contribution of MIT code and noone objected for over a decade. In fact, I believe most people thought it was fine, as far as I am aware.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:25):

only lawyers can tell in the end

view this post on Zulip Bas Spitters (Sep 05 2020 at 10:39):

I know, but it's unlikely that a lawyer will get involved in this.
The GPL only would be wrong, I think. What are the other options? "Disputed"/mixed/under consideration ?

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:42):

as you pointed to above, it's perfectly possible to define licensing on a per-file/per-directory basis, even CompCert does this. I don't think there's anything fundamental about in-file differences in licensing either, it's just that it's so hard to define the different parts of a file unambiguously. In the opam package or similar, one would write something like: "part GPL / part [Other]". But if you have multiple packages/collections and one-license-per-package, this is easier to deal with for everyone.

view this post on Zulip Bas Spitters (Sep 05 2020 at 10:45):

@Vincent Semeria @Michael Soegtrop I propose that for this release we list the directories that are under MIT license, and announce that we are in the process of relicensing and encourage people objecting to contact the coq-community. We can then hope to have things properly resolved in the next release. Does that make sense?

view this post on Zulip Vincent Semeria (Sep 05 2020 at 10:47):

@Bas Spitters Yes, let's do this

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 10:49):

@Bas Spitters yes, a more elaborate license file mentioning this would be a good idea. For Coq platform things are more relaxed than for the Coq library - the Coq platform anyway also contains GPL3 and all sorts of things. The actual licenses of installed stuff will be listed at the begin of the installation process.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 10:55):

@Bas Spitters > It’s unlikely that a lawyer will get involved

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 10:56):

Please allow me some polite push-back (maybe not relevant to _this_ project): All that is alright, until a company is interested in using that code commercially, and _then_ things can get dicey.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 10:57):

For instance, all of @Karl Palmskog‘s questions become relevant.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 10:58):

right, this was basically what I meant about lawyers, these things are sadly operationally defined. I've been part of some similar copyright investigations, and they are very focused on details on whom did what when.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 10:59):

Ah!

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:00):

not in court, but a company doing legal due diligence with help of its legal team

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:00):

makes sense

view this post on Zulip Bas Spitters (Sep 05 2020 at 11:01):

We're in the process of contacting all the contributors (that we are still able to find).

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:01):

indeed, while I’d have thought these questions are only defined by lawsuits, they’re also discussed when e.g. a company lawyer determines whether software can be safely used.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:02):

@Karl Palmskog maybe you have insight for projects on getting their ducks in a row?

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:02):

(I guess we’re firmly OT now)

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:04):

@Paolo Giarrusso not many insights that apply here. It's usually all about building a careful history of contributions and what license they were under, then carefully excising and replacing code that there are doubts about. I think this is what Vincent is already doing.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:05):

my 2 cents (in general) are: if you want to allow/encourage industrial usage, it can be useful to get that right in advance.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:07):

what makes Coq projects easier than other open source software projects legally is that they usually have only a handful of contributors, Corn may be one of the exceptions. If more projects than CompCert go seriously commercial, we will probably soon see these annoying contributor legal forms being required for all PRs

view this post on Zulip Bas Spitters (Sep 05 2020 at 11:09):

@Paolo Giarrusso, @Hugo Herbelin gives a good historical perspective on things:
https://github.com/coq-community/corn/pull/99#issuecomment-677920967

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 11:44):

Well at least for anything recent hosted on a public GIT server, it is at least clear who did what. Problematic are projects that already started in the pre GIT era, like CoRN.


Last updated: Feb 06 2023 at 05:03 UTC