agda / cubical

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

Note licence exceptions #1018

Closed felixwellen closed 1 year ago

felixwellen commented 1 year ago

We already have or will soon have files which are essentially copied from the 1lab. Since the 1lab uses the AGPL 3 licence and we use an MIT licence, we should note the exceptions in our licence file. Maybe like this: "There are a couple of files, which are licenced under more restrictive licences. Those files are marked with the corresponding SPDX identifier." I do not know if this is how it should be done, if you know, please speak up. See the discussion here: #988.

felixwellen commented 1 year ago

I have not found and not heard of anything against this way of dealing with it, so I'll implement it.

felixwellen commented 1 year ago

The solution was that the authors of the corresponding parts of the 1lab agreed to relicense under some BSD license. The license exception is noted now.