So will there be a new release of Corn for 8.12 etc.? Looks like the last release was in 2017.
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.
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?
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.)
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.
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.
@Bas Spitters per-file licensing is to me a "last resort". It makes it a nightmare legally to depend on a project.
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
That said, I applaud efforts to make Corn MIT (or something more permissive), but maybe one can make separate packages with GPL/MIT parts?
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.
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?
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
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.
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.)
Russell's files all start with the MIT license, check for instance
yes, you can claim that your code is MIT, but that doesn't make it MIT if it uses GPL'd code anywhere
Half of Russell's files still calls GPL code. The other half does not, and builds in isolation.
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.
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.
only lawyers can tell in the end
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 ?
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.
@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?
@Bas Spitters Yes, let's do this
@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.
@Bas Spitters > It’s unlikely that a lawyer will get involved
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.
For instance, all of @Karl Palmskog‘s questions become relevant.
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.
not in court, but a company doing legal due diligence with help of its legal team
We're in the process of contacting all the contributors (that we are still able to find).
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.
@Karl Palmskog maybe you have insight for projects on getting their ducks in a row?
(I guess we’re firmly OT now)
@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.
my 2 cents (in general) are: if you want to allow/encourage industrial usage, it can be useful to get that right in advance.
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
@Paolo Giarrusso, @Hugo Herbelin gives a good historical perspective on things:
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: Nov 29 2023 at 05:01 UTC