Coq-Equations icon indicating copy to clipboard operation
Coq-Equations copied to clipboard

Published 20 hours ago • verified publisher icon mattam82

License: unclear

Open SnarkBoojum opened this issue 3 years ago • 1 comments

I packaged coq-equations for Debian, but it got rejected because of licensing issues: the file headers says LGPL 2.1, the opam says LGPL-2.1+.

There are files (theories//Relation.v) out of coq: they are LGPL-2.1.

Could you clarify? Thanks.

SnarkBoojum avatar Jul 09 '22 05:07 SnarkBoojum

It is LGPL-2.1, I don't know why the or-later popped up in the opam package.

mattam82 avatar Jul 27 '22 10:07 mattam82

The origin of the LGPL-2.1-or-later is a suggestion by me to try to clarify the ambiguous "LGPL 2.1": https://github.com/coq/opam-coq-archive/pull/999

However, it was just a suggestion, it was approved by @mattam82. So maybe we can clarify once and for all, and I'll update the opam archive: the SPDX identifier of the Equations license is LGPL-2.1-only?

palmskog avatar Sep 09 '22 15:09 palmskog