Stream: Coq Platform devs & users

Topic: Licensing of libhyps


view this post on Zulip Notification Bot (Sep 08 2022 at 19:06):

This topic was moved here from #Coq devs & plugin devs > Licensing of libhyps by Karl Palmskog.

view this post on Zulip Karl Palmskog (Sep 09 2022 at 11:58):

PR is merged :tada:, now we are just hoping for a new tag/release

view this post on Zulip Karl Palmskog (Sep 09 2022 at 15:42):

when it comes to licensing, it could be useful with a bot that triggers when someone uses the string "LGPL 2.1". There would be a huge red textbox asking: "Do you mean LGPL-2.1-only or LGPL-2.1-or-later?"

view this post on Zulip Karl Palmskog (Sep 09 2022 at 15:43):

context: https://github.com/mattam82/Coq-Equations/issues/496

view this post on Zulip Julien Puydt (Sep 09 2022 at 15:45):

Well, when it comes to licensing, you have a poor soul who will tell you about issues when he'll want to package for Debian... :oh_no:

view this post on Zulip Karl Palmskog (Sep 09 2022 at 15:47):

OK, then I don't think you want to know how things were with licensing before we had the Platform

view this post on Zulip Karl Palmskog (Sep 09 2022 at 15:48):

I've essentially been pressuring people to add SPDX identifiers, any SPDX identifiers, for years now in opam archive PRs.

view this post on Zulip Karl Palmskog (Sep 09 2022 at 15:50):

license: "GPL" is basically a nightmare, not just because of license versioning, but because incompatibility between GPL and the common Coq project licenses CECILL-B and CECILL-C. Docker containers can become license violations as a result.

view this post on Zulip Karl Palmskog (Sep 09 2022 at 16:10):

"typical" Coq project, 38 stars and lots of work behind it, with no license at all, or even license indications as far as I could see: https://github.com/andrejbauer/dedekind-reals

view this post on Zulip Karl Palmskog (Sep 09 2022 at 16:18):

to be honest I think the "I'm packaging this for Debian" angle is going to be much faster and more effective to get people to sort their licenses than when some rando opens a general "Fix your license" GitHub issue

view this post on Zulip Karl Palmskog (Sep 20 2022 at 10:22):

for the record, the license fix has been merged in the libhyps repo: https://github.com/Matafou/LibHyps/pull/10

but we'd also like a release of this code for packaging: https://github.com/Matafou/LibHyps/issues/11

view this post on Zulip Julien Puydt (Sep 20 2022 at 12:32):

Ping me when there's a new upstream release with a good license -- I'll then package for Debian


Last updated: Jan 30 2023 at 11:03 UTC