Stream: Coq users

Topic: ✔ New project


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 26 2022 at 15:29):

as for Coq project repository boilerplate and structure, two examples here, one using our templates:

view this post on Zulip 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

view this post on Zulip Notification Bot (Sep 26 2022 at 16:34):

Huỳnh Trần Khanh has marked this topic as resolved.

view this post on Zulip Notification Bot (Sep 27 2022 at 15:42):

This topic was moved to #Miscellaneous > CC0 for software by Théo Zimmermann.


Last updated: Jan 28 2023 at 07:30 UTC