This topic was moved here from #Coq devs & plugin devs > Licensing of libhyps by Karl Palmskog.
PR is merged :tada:, now we are just hoping for a new tag/release
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?"
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:
OK, then I don't think you want to know how things were with licensing before we had the Platform
I've essentially been pressuring people to add SPDX identifiers, any SPDX identifiers, for years now in opam archive PRs.
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.
"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
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
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
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