Zulip Chat Archive

Stream: general

Topic: GNU Public License files


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 06 2019 at 22:28):

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

view this post on Zulip Seul Baek (May 06 2019 at 22:35):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 06 2019 at 22:49):

LeanCoP no longer completely unrelated to Lean :-)

view this post on Zulip Seul Baek (May 06 2019 at 23:19):

Yeah that was part of the motivation :)

view this post on Zulip Mario Carneiro (May 06 2019 at 23:27):

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

view this post on Zulip Mario Carneiro (May 06 2019 at 23:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Seul Baek (May 06 2019 at 23:49):

OK that sounds reasonable, thank you

view this post on Zulip 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: May 17 2021 at 21:12 UTC