Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[doc] [license] Improve licensing situation. #361

Merged
merged 1 commit into from
Feb 21, 2024
Merged

[doc] [license] Improve licensing situation. #361

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@
- [serlib] Support `btauto` Coq plugin (@ejgallego, #362)
- [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n,
#375, fixes #371)
- [general] Make licensing clearer (@ejgallego, @palmskog,
@SnarkBoojum, #361, closes #266)

## Version 0.19.0

Expand Down
18 changes: 10 additions & 8 deletions LICENSE
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,22 +3,24 @@ 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: sertop/js_sexp_printer.ml*
License: MIT
Copyright: Copyright (c) 2005--2023 Jane Street Group, LLC <[email protected]>

Files: serlib/* serapi/* sertop/ser* sertop/comp*
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
View file
Open in desktop
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
2 changes: 1 addition & 1 deletion serapi/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@
(name serapi)
(public_name coq-serapi.serapi_v8_14)
(synopsis "Serialization Protocol for Coq")
(libraries coq-core.stm coq-core.plugins.ltac sexplib))
(libraries coq-core.stm coq-core.plugins.ltac sexplib base))
18 changes: 17 additions & 1 deletion serapi/ser_stream.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,20 @@
(* Compat_code *)
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

let of_string = Gramlib.Stream.of_string
let of_channel = Gramlib.Stream.of_channel
14 changes: 7 additions & 7 deletions serapi/serapi_assumptions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Very Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

type ax_ctx = (Names.Label.t * Constr.rel_context * Constr.t) list
Expand Down
14 changes: 7 additions & 7 deletions serapi/serapi_assumptions.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Very Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

type ax_ctx = (Names.Label.t * Constr.rel_context * Constr.t) list
Expand Down
16 changes: 7 additions & 9 deletions serapi/serapi_doc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,23 +1,21 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2021 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Copyright 2020-2021 Inria *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

(* Duplicate with sertop, fix in different refactoring *)
let check_pending_proofs ~pstate =
Option.iter (fun _pstate ->
(* let pfs = Proof_global.get_all_proof_names pstate in *)
Expand Down
15 changes: 7 additions & 8 deletions serapi/serapi_doc.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,19 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2021 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Copyright 2020-2021 Inria *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

val check_pending_proofs : pstate:Vernacstate.LemmaStack.t option -> unit
Expand Down
14 changes: 7 additions & 7 deletions serapi/serapi_goals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Very Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

type 'a hyp = (Names.Id.t list * 'a option * 'a)
Expand Down
14 changes: 7 additions & 7 deletions serapi/serapi_goals.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Very Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

(* We ship our own type due to Context lack of support for anything
Expand Down
18 changes: 7 additions & 11 deletions serapi/serapi_paths.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,25 +1,21 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Very Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

(******************************************************************************)
(* Coq Prelude Loading Defaults (to be improved) *)
(******************************************************************************)

let coq_loadpath_default ~implicit ~coq_path =
let open Loadpath in
let mk_path prefix = coq_path ^ "/" ^ prefix in
Expand Down
15 changes: 7 additions & 8 deletions serapi/serapi_paths.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,22 +1,21 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
(* Written by: Emilio J. Gallego Arias *)
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
(************************************************************************)
(* Status: Very Experimental *)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
(* Written by: Emilio J. Gallego Arias and others *)
(************************************************************************)

(* Default load path for Coq's stdlib *)
val coq_loadpath_default : implicit:bool -> coq_path:string -> string list * Loadpath.vo_path list

(* Generate a module name given a file, to be removed in 8.10 *)
Expand Down
Loading
Loading