search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

OPAM release? #17

Closed arthuraa closed 2 years ago

arthuraa commented 4 years ago

Any plans to release this on OPAM? :)

jwiegley commented 3 years ago

That's a great idea @arthuraa. I've never used OPAM before, would you be able to help?

arthuraa commented 3 years ago

@jwiegley Yes, I could help. I could create an OPAM file for the project and submit a pull request to the archive. I'll do it as soon as I get some spare time.

palmskog commented 3 years ago

@jwiegley @arthuraa before you submit any pull requests to the Coq opam archive, please resolve the license ambiguity for this project. The current README and the opam package file says "MIT", but the actual LICENSE file uses the BSD-3-Clause license text.

See for example here for the MIT license wording: https://spdx.org/licenses/MIT.html

jwiegley commented 2 years ago

@palmskog I've updated the opam package file to use "BSD" rather than "MIT".

palmskog commented 2 years ago

@jwiegley unfortunately "BSD" is ambiguous. If you submit this to the archive, please use "BSD-3-Clause" instead (based on the current text in LICENSE). The nitpicking is unfortunate but we hope to add automation to check licensing in the near future.

jwiegley commented 2 years ago

Sure thing. Pushed.

palmskog commented 2 years ago

Thanks. If you want to put this project in the Coq opam archive, you now have two options (not mutually exclusive):

Both of these are done by submitting a pull request to the archive. I can help if you want, but it might suffice to see an example: https://github.com/coq/opam-coq-archive/pull/1982/files

jwiegley commented 2 years ago

@palmskog Working on this now, will be pushed once #35 is merged and my opam check succeeds locally.

jwiegley commented 2 years ago

https://github.com/coq/opam-coq-archive/pull/2243