Skip to content

Commit

Permalink
[doc] [license] Improve licensing situation.
Browse files Browse the repository at this point in the history
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog
for helping with this.

- Fix LICENSE and opam file discrepancies
- Update LICENSE from `debian/copyright` work by Julien
- Fix file headers
- Move JS files to its own util files (can be also removed in favor of
  `base` these days)
  • Loading branch information
ejgallego committed Sep 29, 2023
1 parent 1b603b3 commit 413f870
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 10 deletions.
4 changes: 3 additions & 1 deletion CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
## unreleased

- [general] Cleanup old / unused code (@ejgallego, #)
- [general] Cleanup old / unused code (@ejgallego, #362)
- [general] Make licensing clearer (@ejgallego @palmskog
@SnarkBoojum, #361, closes #266)

## Version 0.18.1:

Expand Down
14 changes: 6 additions & 8 deletions LICENSE
Original file line number Diff line number Diff line change
Expand Up @@ -3,22 +3,20 @@ Upstream-Name: coq-serapi
Upstream-Contact: Emilio J. Gallego Arias <[email protected]>
Source: https://github.com/ejgallego/coq-serapi
License: LGPL-2.1+
Copyright: 2016-2022, MINES ParisTech / Inria
Copyright: 2016-2023, MINES ParisTech / Inria / others
Authors: Emilio J. Gallego Arias, Karl Palmskog, Clément Pit-Claudel, Kaiyu Yang

Authors: Emilio J. Gallego Arias
Files: serlib/* serapi/* sertop/*
License: LGPL-2.1+
Copyright: 2016-2023, MINES ParisTech / Inria / others

Files: notes/*
License: LGPL-2.1+ / CC-BY-SA 3.0

Files: jscoq/*
License: GPL-3+

Files: tests/genarg/*
Authors: Karl Palmskog
Licence: Derived from many projects as test cases, falls into fair-use

Comment: the intent is to be compatible with Coq's license. Note that
the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor
that. In some cases, like when linking with jsCoq's code or other code
that is GPL-3 only, the resulting .js or binaries files will be GPL-3.
the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor that.

2 changes: 1 addition & 1 deletion coq-serapi.opam
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ maintainer: "[email protected]"
homepage: "https://github.com/ejgallego/coq-serapi"
bug-reports: "https://github.com/ejgallego/coq-serapi/issues"
dev-repo: "git+https://github.com/ejgallego/coq-serapi.git"
license: "GPL-3.0-or-later"
license: "LGPL-2.1-or-later"
doc: "https://ejgallego.github.io/coq-serapi/"

synopsis: "Serialization library and protocol for machine interaction with the Coq proof assistant"
Expand Down

0 comments on commit 413f870

Please sign in to comment.