diff --git a/CHANGES.md b/CHANGES.md index 32ee780d..23d34b3d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,11 @@ +## Version 0.19.1 + + - [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 - [serapi] (!) support for Coq 8.19, thanks to all the developers diff --git a/LICENSE b/LICENSE index 8b88e2c9..54458aa3 100644 --- a/LICENSE +++ b/LICENSE @@ -3,22 +3,24 @@ Upstream-Name: coq-serapi Upstream-Contact: Emilio J. Gallego Arias 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 + +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. diff --git a/coq-serapi.opam b/coq-serapi.opam index a0cb06f8..e0d9d626 100644 --- a/coq-serapi.opam +++ b/coq-serapi.opam @@ -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" diff --git a/serapi/dune b/serapi/dune index 8a2044b4..a8e6698b 100644 --- a/serapi/dune +++ b/serapi/dune @@ -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)) diff --git a/serapi/ser_stream.ml b/serapi/ser_stream.ml index 56cae70b..16b091b5 100644 --- a/serapi/ser_stream.ml +++ b/serapi/ser_stream.ml @@ -1,4 +1,20 @@ -(* Compat_code *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* (* let pfs = Proof_global.get_all_proof_names pstate in *) diff --git a/serapi/serapi_doc.mli b/serapi/serapi_doc.mli index 267c9a88..68cf69fe 100644 --- a/serapi/serapi_doc.mli +++ b/serapi/serapi_doc.mli @@ -1,20 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2021 *) -(* unit diff --git a/serapi/serapi_goals.ml b/serapi/serapi_goals.ml index 1eac1ff6..2c362b35 100644 --- a/serapi/serapi_goals.ml +++ b/serapi/serapi_goals.ml @@ -1,19 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* coq_path:string -> string list * Loadpath.vo_path list (* Generate a module name given a file, to be removed in 8.10 *) diff --git a/serapi/serapi_pp.ml b/serapi/serapi_pp.ml index 1834db61..d9412edd 100644 --- a/serapi/serapi_pp.ml +++ b/serapi/serapi_pp.ml @@ -1,16 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let prefix_len = String.length prefix in - String.length s >= prefix_len && loop s ~prefix ~char_equal (prefix_len - 1) - - let is_prefix s ~prefix = is_prefix_gen s ~prefix ~char_equal:(fun x y -> x = y) - - let split_while xs ~f = - let rec loop acc = function - | hd :: tl when f hd -> loop (hd :: acc) tl - | t -> (List.rev acc, t) - in - loop [] xs - - (* End of Core_kernel code, (c) Jane Street *) - (******************************************************************************) + let is_prefix = Base.String.is_prefix + let split_while = Base.List.split_while + (* Custom tokenizer *) let rec stream_tok n_tok acc lstr = let e = Gramlib.LStream.next (Pcoq.get_keyword_state()) lstr in let loc = Gramlib.LStream.get_loc n_tok lstr in diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli index 036e93d4..e3484366 100644 --- a/serapi/serapi_protocol.mli +++ b/serapi/serapi_protocol.mli @@ -1,24 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Sexp.t -> 'a data - * val sexp_of_data : ('a -> Sexp.t) -> 'a data -> Sexp.t *) diff --git a/serlib/ser_proof_bullet.ml b/serlib/ser_proof_bullet.ml index 48afa5d2..09ac0803 100644 --- a/serlib/ser_proof_bullet.ml +++ b/serlib/ser_proof_bullet.ml @@ -1,18 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Exninfo.info -> 'a diff --git a/sertop/js_sexp_printer.ml b/sertop/js_sexp_printer.ml new file mode 100644 index 00000000..f4fbfed6 --- /dev/null +++ b/sertop/js_sexp_printer.ml @@ -0,0 +1,121 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* true + (* Avoid unquoted comma at the beggining of the string *) + | ',' -> ix = 0 || loop (ix - 1) + | '|' -> ix > 0 && let next = ix - 1 in str.[next] = '#' || loop next + | '#' -> ix > 0 && let next = ix - 1 in str.[next] = '|' || loop next + | '\000' .. '\032' -> true + | '\248' .. '\255' -> true + | _ -> ix > 0 && loop (ix - 1) + in + loop (len - 1) + +(* XXX: Be faithful to UTF-8 *) +let st_escaped (s : string) = + let sget = String.unsafe_get in + let open Bytes in + let n = ref 0 in + for i = 0 to String.length s - 1 do + n := !n + + (match sget s i with + | '\"' | '\\' | '\n' | '\t' | '\r' | '\b' -> 2 + | ' ' .. '~' -> 1 + (* UTF-8 are valid between \033 -- \247 *) + | '\000' .. '\032' -> 4 + | '\248' .. '\255' -> 4 + | _ -> 1) + done; + if !n = String.length s then Bytes.of_string s else begin + let s' = create !n in + n := 0; + for i = 0 to String.length s - 1 do + begin match sget s i with + | ('\"' | '\\') as c -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n c + | '\n' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'n' + | '\t' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 't' + | '\r' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'r' + | '\b' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'b' + | (' ' .. '~') as c -> unsafe_set s' !n c + (* Valid UTF-8 are valid between \033 -- \247 *) + | '\000' .. '\032' + | '\248' .. '\255' as c -> + let a = Char.code c in + unsafe_set s' !n '\\'; + incr n; + unsafe_set s' !n (Char.chr (48 + a / 100)); + incr n; + unsafe_set s' !n (Char.chr (48 + (a / 10) mod 10)); + incr n; + unsafe_set s' !n (Char.chr (48 + a mod 10)); + | c -> unsafe_set s' !n c + end; + incr n + done; + s' + end + +let esc_str (str : string) = + let open Bytes in + let estr = st_escaped str in + let elen = length estr in + let res = create (elen + 2) in + blit estr 0 res 1 elen; + set res 0 '"'; + set res (elen + 1) '"'; + to_string res + +let sertop_maybe_esc_str str = + if must_escape str then esc_str str else str + +let rec pp_sertop_internal may_need_space ppf = function + | Atom str -> + let str' = sertop_maybe_esc_str str in + let new_may_need_space = str' == str in + if may_need_space && new_may_need_space then pp_print_string ppf " "; + pp_print_string ppf str'; + new_may_need_space + | List (h :: t) -> + pp_print_string ppf "("; + let may_need_space = pp_sertop_internal false ppf h in + pp_sertop_rest may_need_space ppf t; + false + | List [] -> pp_print_string ppf "()"; false + +and pp_sertop_rest may_need_space ppf = function + | h :: t -> + let may_need_space = pp_sertop_internal may_need_space ppf h in + pp_sertop_rest may_need_space ppf t + | [] -> pp_print_string ppf ")" + +let pp_sertop ppf sexp = ignore (pp_sertop_internal false ppf sexp) diff --git a/sertop/js_sexp_printer.mli b/sertop/js_sexp_printer.mli new file mode 100644 index 00000000..8e8cc0f6 --- /dev/null +++ b/sertop/js_sexp_printer.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Sexplib.Sexp.t -> unit diff --git a/sertop/sercomp.ml b/sertop/sercomp.ml index 9397b9e6..befb8ac9 100644 --- a/sertop/sercomp.ml +++ b/sertop/sercomp.ml @@ -1,19 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* unit diff --git a/sertop/sername.ml b/sertop/sername.ml index 6b50b661..ee9c32f2 100644 --- a/sertop/sername.ml +++ b/sertop/sername.ml @@ -1,18 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Sertop_util.pp_sertop + | SP_Sertop -> Js_sexp_printer.pp_sertop | SP_Mach -> Sexp.pp | SP_Human -> Sexp.pp_hum @@ -93,7 +93,6 @@ module Impargs = Ser_impargs module Constr = Ser_constr module EConstr = Ser_eConstr module Constrexpr = Ser_constrexpr -module Proof = Ser_proof module Tok = Ser_tok module Ppextend = Ser_ppextend module Notation_gram = Ser_notation_gram diff --git a/sertop/sertop_ser.mli b/sertop/sertop_ser.mli index c86e2948..d06be1bd 100644 --- a/sertop/sertop_ser.mli +++ b/sertop/sertop_ser.mli @@ -1,19 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* true - (* Avoid unquoted comma at the beggining of the string *) - | ',' -> ix = 0 || loop (ix - 1) - | '|' -> ix > 0 && let next = ix - 1 in str.[next] = '#' || loop next - | '#' -> ix > 0 && let next = ix - 1 in str.[next] = '|' || loop next - | '\000' .. '\032' -> true - | '\248' .. '\255' -> true - | _ -> ix > 0 && loop (ix - 1) - in - loop (len - 1) - -(* XXX: Be faithful to UTF-8 *) -let st_escaped (s : string) = - let sget = String.unsafe_get in - let open Bytes in - let n = ref 0 in - for i = 0 to String.length s - 1 do - n := !n + - (match sget s i with - | '\"' | '\\' | '\n' | '\t' | '\r' | '\b' -> 2 - | ' ' .. '~' -> 1 - (* UTF-8 are valid between \033 -- \247 *) - | '\000' .. '\032' -> 4 - | '\248' .. '\255' -> 4 - | _ -> 1) - done; - if !n = String.length s then Bytes.of_string s else begin - let s' = create !n in - n := 0; - for i = 0 to String.length s - 1 do - begin match sget s i with - | ('\"' | '\\') as c -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n c - | '\n' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'n' - | '\t' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 't' - | '\r' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'r' - | '\b' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'b' - | (' ' .. '~') as c -> unsafe_set s' !n c - (* Valid UTF-8 are valid between \033 -- \247 *) - | '\000' .. '\032' - | '\248' .. '\255' as c -> - let a = Char.code c in - unsafe_set s' !n '\\'; - incr n; - unsafe_set s' !n (Char.chr (48 + a / 100)); - incr n; - unsafe_set s' !n (Char.chr (48 + (a / 10) mod 10)); - incr n; - unsafe_set s' !n (Char.chr (48 + a mod 10)); - | c -> unsafe_set s' !n c - end; - incr n - done; - s' - end - -let esc_str (str : string) = - let open Bytes in - let estr = st_escaped str in - let elen = length estr in - let res = create (elen + 2) in - blit estr 0 res 1 elen; - set res 0 '"'; - set res (elen + 1) '"'; - to_string res - -let sertop_maybe_esc_str str = - if must_escape str then esc_str str else str - -let rec pp_sertop_internal may_need_space ppf = function - | Atom str -> - let str' = sertop_maybe_esc_str str in - let new_may_need_space = str' == str in - if may_need_space && new_may_need_space then pp_print_string ppf " "; - pp_print_string ppf str'; - new_may_need_space - | List (h :: t) -> - pp_print_string ppf "("; - let may_need_space = pp_sertop_internal false ppf h in - pp_sertop_rest may_need_space ppf t; - false - | List [] -> pp_print_string ppf "()"; false - -and pp_sertop_rest may_need_space ppf = function - | h :: t -> - let may_need_space = pp_sertop_internal may_need_space ppf h in - pp_sertop_rest may_need_space ppf t - | [] -> pp_print_string ppf ")" - -let pp_sertop ppf sexp = ignore (pp_sertop_internal false ppf sexp) - -(* XXX: This is terrible and doesn't work yet *) let rec coq_pp_opt (d : Pp.t) = let open Pp in let rec flatten_glue l = match l with | [] -> [] diff --git a/sertop/sertop_util.mli b/sertop/sertop_util.mli index d0509add..8ee77c7e 100644 --- a/sertop/sertop_util.mli +++ b/sertop/sertop_util.mli @@ -1,24 +1,21 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Sexp.t -> unit - val coq_pp_opt : Pp.t -> Pp.t val feedback_pos_filter : string -> Feedback.feedback -> Feedback.feedback diff --git a/tests/genarg/dune b/tests/genarg/dune index 0ed6b41d..11ec5940 100644 --- a/tests/genarg/dune +++ b/tests/genarg/dune @@ -10,7 +10,7 @@ (run chmod +w test_roundtrip) ; We insert the digest of the binaries to force a rebuild of the ; test cases if the binary has been modified. - (bash "echo \"# $(md5sum ../../sertop/sercomp.exe)\" >> test_roundtrip")))) + (bash "for i in ../../sertop/sercomp.exe ../../serlib/plugins/*/*.cmxs; do echo \"# $(md5sum $i)\"; done >> test_roundtrip")))) (rule (alias runtest) @@ -57,6 +57,11 @@ (deps (:input exists.v)) (action (run ./test_roundtrip %{input}))) +(rule + (alias runtest) + (deps (:input extraction.v)) + (action (run ./test_roundtrip %{input}))) + (rule (alias runtest) (deps (:input firstorder.v)) diff --git a/tests/genarg/extraction.v b/tests/genarg/extraction.v new file mode 100644 index 00000000..ec92c845 --- /dev/null +++ b/tests/genarg/extraction.v @@ -0,0 +1,8 @@ +Require Coq.extraction.Extraction. + +Extraction Language Haskell. + +Extraction Implicit pred [1]. + +Axiom Y : Set -> Set -> Set. +Extract Constant Y "'a" "'b" => " 'a * 'b ".