GNU Public License files

Stream: general

[Seul Baek]

I was going to make a PR that includes a small example of interacting with an external solver, but I noticed that this solver is under the GNU Public License. Are there any potential issues here with including the scripts of the solver? I'm not sure how GPL differs from Apache 2.0, so I wouldn't want to do this if this makes all of mathlib GPL.

[Kevin Buzzard]

I know nothing about licenses, but which solver out of interest?

[Seul Baek]

http://www.leancop.de/leancopD.html#leancop10 This one.

[Seul Baek]

It's probably too slow for anything practical, but it's meant to be a usage example for a general interface to external FOL solvers

[Kevin Buzzard]

LeanCoP no longer completely unrelated to Lean :-)

[Seul Baek]

Yeah that was part of the motivation :)

[Mario Carneiro]

Unfortunately, GPL v3 is incompatible with Apache 2 https://www.apache.org/licenses/GPL-compatibility.html

[Mario Carneiro]

This is why I hate licenses. Join me and support CC0 / PD

[Mario Carneiro]

If it's just an example or demonstration, I think you can license just that file as GPL

[Mario Carneiro]

Or you can contact Jens Otten and ask for him to allow the file (or at least your derivative work) to be Apache licensed. Given that there's only one line about licensing anywhere on the site, I expect he didn't think so much about licenses so the request will probably be granted

[Seul Baek]

OK that sounds reasonable, thank you

[Seul Baek]

Just an aside, but it seems that software license is one area that could really benefit from logical specifications to sort out its ambiguities...