search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

Switch license to MPL #11

Closed liyishuai closed 3 years ago

liyishuai commented 3 years ago

I've noticed that this repo uses LGPL which is no longer recommended by the community. Should we switch license before having more contributors?

JasonGross commented 3 years ago

Why the MPL rather than MIT or BSD?

liyishuai commented 3 years ago

The current LGPL is weak-copyleft, so I proposed MPL which is still weak-copyleft but easier to clarify.

herbelin commented 3 years ago

I'm ok with licensing the plugin as MPL or MIT (or BSD).

SkySkimmer commented 3 years ago

Shouldn't plugins be lgpl so that they can exchange code with coq?

herbelin commented 3 years ago

Shouldn't plugins be lgpl so that they can exchange code with coq?

What about double licensing then?

Zimmi48 commented 3 years ago

Shouldn't plugins be lgpl so that they can exchange code with coq?

That's a fair question.

What about double licensing then?

This would work for the external plugin to Coq path, but not for the other way (I don't know if it's really important though).

liyishuai commented 3 years ago

Do we need double licensing for MPL code in LGPL project?

Zimmi48 commented 3 years ago

Do we need double licensing for MPL code in LGPL project?

No, actually, you're right. Since MPL 2.0 is explictly designed to be (L)GPL-compatible, we don't.

liyishuai commented 3 years ago

I can foresee migrating code from here to Coq repo, but not backwards. Propose merging on Monday if no other concerns arise.