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 to a single uniform header
- Move JS file to its own file, note that on license.
  • Loading branch information
@ejgallego
ejgallego committed Feb 21, 2024
1 parent b1dd23b commit c8d4473
Show file tree
Hide file tree
Showing 243 changed files with 2,428 additions and 1,852 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
View file
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
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 <e@x80.org>
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 <opensource-contacts@janestreet.com>

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
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ maintainer: "e@x80.org"
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
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
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
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
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
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
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
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
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
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
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

0 comments on commit c8d4473

Please sign in to comment.