search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

#1018: Note licence exceptions #1021

Closed felixwellen closed 1 year ago

jpoiret commented 1 year ago

(IANAL) Thinking about it a bit more, I don't think you can license the whole project MIT if it includes GPL'd code that is then used by the MIT code, since it is infective.

Also, [1] might be a good resource, it's an FSFE initiative with clear standards.

[1] https://reuse.software/

felixwellen commented 1 year ago

What do you mean with 'infective'? Are you saying if I use something under the GPL in my source code, then my source code also needs to adopt the GPL principles? Also, note, that with this change, the project wouldn't be licensed under the MIT license anymore. Instead, it would have a license, which says some files are MIT, some something else. I wouldn't call that 'licensed under MIT'.

jpoiret commented 1 year ago

What do you mean with 'infective'? Are you saying if I use something under the GPL in my source code, then my source code also needs to adopt the GPL principles? Also, note, that with this change, the project wouldn't be licensed under the MIT license anymore. Instead, it would have a license, which says some files are MIT, some something else. I wouldn't call that 'licensed under MIT'.

(IANAL) While you can license some files under a license and some others using another one, you still have to respect the contents of both licenses, but here, the GPL explicitely covers modified versions of the original program, including things that are "based" on it.

To “modify” a work means to copy from or adapt all or part of the work in a fashion requiring copyright permission, other than the making of an exact copy. The resulting work is called a “modified version” of the earlier work or a work “based on” the earlier work.

A “covered work” means either the unmodified Program or a work based on the Program.

Then, the provision of section 5 applies, by which

c) You must license the entire work, as a whole, under this License to anyone who comes into possession of a copy. This License will therefore apply, along with any applicable section 7 additional terms, to the whole of the work, and all its parts, regardless of how they are packaged. This License gives no permission to license the work in any other way, but it does not invalidate such permission if you have separately received it.

You could say this is the whole point of the GPL, ie. to force things that use GPL'd programs to themselves be free software. The MIT license doesn't force this, it is not "infective".

felixwellen commented 1 year ago

Discussed with Josselin and understood that there really is a problem and we cannot do things like suggested in this PR :-(

felixwellen commented 1 year ago

To repeat the issue in my own words: Even if we would just depend on the 1lab sources and import something from there, without having it here, that would be not compatible with our use of the MIT license. This is because using source code under a GPL (which is not the LGPL) means that our work is derived from the work licensed under the GPL, and therefore has to be licensed under the GPL as well.

felixwellen commented 1 year ago

Adapted the text to using BSD-licensed files, which we can actually do.

felixwellen commented 1 year ago

As discussed in #988, this should be good now -> merging.