Huỳnh Trần Khanh (Sep 26 2022 at 15:22): Huỳnh Trần Khanh (Sep 26 2022 at 15:22):I plan to make a new library for my personal use... and maybe for other people too. In JavaScript I would do this: initialize new npm package with npm init, write some code, install some dependencies and publish everything on a package repository somewhere. And everyone who installs my package with npm install has the necessary dependencies too. How could I achieve the same in Coq?
Huỳnh Trần Khanh (Sep 26 2022 at 15:24):Also: my code is licensed under CC0, I use coq-equations which is licensed under LGPL, and I plan to use coq-stdpp which is licensed under a BSD 3 clause license. Is this legal? Does this violate copyright?
Karl Palmskog (Sep 26 2022 at 15:26):both LGPL-2.1 and BSD-3 allow you to use essentially any license for derivative works (in case of LGPL, you mustn't change anything in the upstream library). So in particular, as long as you don't bundle/include the Equations or Stdpp code in your repo, CC0 is fine, to my knowledge.
Karl Palmskog (Sep 26 2022 at 15:29):as for Coq project repository boilerplate and structure, two examples here, one using our templates:
meta.yml) Karl Palmskog (Sep 26 2022 at 15:30):if you want to publish a package, please make a pull request to this repo with an opam file in the released repo
here (please base the package on an archive with a stable URL, e.g., one generated by GitHub from a tag): https://github.com/coq/opam-coq-archive/#usage
Some additional documentation here: https://coq.inria.fr/opam-packaging.html
Notification Bot (Sep 26 2022 at 16:34):Huỳnh Trần Khanh has marked this topic as resolved.
Notification Bot (Sep 27 2022 at 15:42):This topic was moved to #Miscellaneous > CC0 for software by Théo Zimmermann.
Last updated: Oct 03 2023 at 04:02 UTC