Zulip Chat Archive

Stream: general

Topic: GNU Public License files

Seul Baek (May 06 2019 at 22:24):

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 (May 06 2019 at 22:28):

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

Seul Baek (May 06 2019 at 22:35):

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

Seul Baek (May 06 2019 at 22:36):

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 (May 06 2019 at 22:49):

LeanCoP no longer completely unrelated to Lean :-)

Seul Baek (May 06 2019 at 23:19):

Yeah that was part of the motivation :)

Mario Carneiro (May 06 2019 at 23:27):

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

Mario Carneiro (May 06 2019 at 23:27):

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

Mario Carneiro (May 06 2019 at 23:28):

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

Mario Carneiro (May 06 2019 at 23:38):

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 (May 06 2019 at 23:49):

OK that sounds reasonable, thank you

Seul Baek (May 07 2019 at 00:02):

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

Last updated: Aug 03 2023 at 10:10 UTC