Karl Palmskog (Sep 07 2022 at 18:58): Karl Palmskog (Sep 07 2022 at 18:58):@Julien Puydt coq-libhyps has been relicensed as MIT, can you point to where the license problems are?
Karl Palmskog (Sep 07 2022 at 18:59):official package has MIT at least: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-libhyps/coq-libhyps.2.0.5/opam
Julien Puydt (Sep 07 2022 at 19:00):I reported the issue here : the various source files don't claim the same thing, so I don't even try to propose it for Debian.
Karl Palmskog (Sep 07 2022 at 19:16):did a PR to fix it, now I'll wait a bit before possibly pinging author more extensively.
Notification Bot (Sep 08 2022 at 19:06):This topic was moved here from #Coq devs & plugin devs > Licensing of libhyps by Karl Palmskog.
Karl Palmskog (Sep 09 2022 at 11:58):PR is merged :tada:, now we are just hoping for a new tag/release
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?"
Karl Palmskog (Sep 09 2022 at 15:43):context: https://github.com/mattam82/Coq-Equations/issues/496
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:
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
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.
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.
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
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
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
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
Karl Palmskog (Sep 23 2022 at 13:58):@Julien Puydt an extra ping about the new LibHyps release:
Notification Bot (Sep 23 2022 at 13:59):Karl Palmskog has marked this topic as resolved.
Julien Puydt (Sep 23 2022 at 14:13):Thanks, I'll work on updating my would-be package and propose it for inclusion.
Last updated: Jun 05 2023 at 10:01 UTC