Skip to content

Commit

Permalink
[deps] Bump cmdliner dep to 1.1.0, remove deprecation warnings in OCa…
Browse files Browse the repository at this point in the history
…ml 4.14.0
  • Loading branch information
ejgallego committed Jun 23, 2022
1 parent 0a21863 commit 20f868b
Show file tree
Hide file tree
Showing 9 changed files with 48 additions and 50 deletions.
1 change: 1 addition & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
## Version 0.15.2:

- [deps] Support Jane Street libraries v0.15.0 (@ejgallego)
- [deps] Require cmdliner >= 1.1.0 (@ejgallego)

## Version 0.15.1:

Expand Down
2 changes: 1 addition & 1 deletion coq-serapi.opam
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ authors: [
depends: [
"ocaml" { >= "4.07.0" }
"coq" { !pinned & >= "8.15" & < "8.16" }
"cmdliner" { >= "1.0.0" }
"cmdliner" { >= "1.1.0" }
"ocamlfind" { >= "1.8.0" }
"sexplib" { >= "v0.13.0" }
"dune" { >= "2.0.1" }
Expand Down
2 changes: 1 addition & 1 deletion dune
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(env
(dev (flags :standard -rectypes -w -3))
(dev (flags :standard -rectypes))
(release (flags :standard -rectypes)))

(install
Expand Down
4 changes: 4 additions & 0 deletions serapi/ser_stream.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
(* Compat_code *)

let of_string = Stream.of_string [@warning "-3"]
let of_channel = Stream.of_channel [@warning "-3"]
8 changes: 4 additions & 4 deletions serapi/serapi_protocol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -601,7 +601,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
| TypeOf id -> snd (QueryUtil.info_of_id env id)
| Search -> [CoqString "Not Implemented"]
(* XXX: should set printing options in all queries *)
| Vernac q -> let pa = Pcoq.Parsable.make (Stream.of_string q) in
| Vernac q -> let pa = Pcoq.Parsable.make (Ser_stream.of_string q) in
Stm.query ~doc ~at:opt.sid ~route:opt.route pa; []
(* XXX: Should set the proper sid state *)
| Env -> [CoqEnv env]
Expand Down Expand Up @@ -705,14 +705,14 @@ module ControlUtil = struct

let parse_sentence ~doc ~(opt : parse_opt) sent =
let ontop = Extra.value opt.ontop ~default:(Stm.get_current_state ~doc) in
let pa = Pcoq.Parsable.make (Stream.of_string sent) in
let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in
let entry = Pvernac.main_entry in
Stm.parse_sentence ~doc ontop ~entry pa

exception End_of_input

let add_sentences ~doc opts sent =
let pa = Pcoq.Parsable.make (Stream.of_string sent) in
let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in
let i = ref 1 in
let acc = ref [] in
let stt = ref (Extra.value opts.ontop ~default:(Stm.get_current_state ~doc)) in
Expand Down Expand Up @@ -937,7 +937,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
| Tokenize input ->
let st = CLexer.Lexer.State.get () in
begin try
let istr = Stream.of_string input in
let istr = Ser_stream.of_string input in
let lex = CLexer.Lexer.tok_func istr in
CLexer.Lexer.State.set st;
let objs = Extra.stream_tok 0 [] lex in
Expand Down
20 changes: 9 additions & 11 deletions sertop/sercomp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ let input_doc ~input ~in_file ~in_chan ~process ~doc ~sid =
match input with
| I_vernac ->
begin
let in_strm = Stream.of_channel in_chan in
let in_strm = Serapi.Ser_stream.of_channel in_chan in
let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file} )) in_strm in
try while true do
let doc, sid = !stt in
Expand Down Expand Up @@ -227,18 +227,16 @@ let main () =

let sercomp_cmd =
let open Sertop.Sertop_arg in
Term.(const driver
$ comp_input $ comp_mode $ debug $ disallow_sprop $ indices_matter $ printer $ async $ async_workers $ error_recovery $ quick $ prelude
$ ml_include_path $ load_path $ rload_path $ input_file $ omit_loc $ omit_att $ omit_env $ exn_on_opaque
),
Term.info "sercomp" ~version:sercomp_version ~doc:sercomp_doc ~man:sercomp_man
let term =
Term.(const driver
$ comp_input $ comp_mode $ debug $ disallow_sprop $ indices_matter $ printer $ async $ async_workers $ error_recovery $ quick $ prelude
$ ml_include_path $ load_path $ rload_path $ input_file $ omit_loc $ omit_att $ omit_env $ exn_on_opaque
) in
let info = Cmd.info "sercomp" ~version:sercomp_version ~doc:sercomp_doc ~man:sercomp_man in
Cmd.v info term
in

try match Term.eval ~catch:false sercomp_cmd with
| `Error _ -> exit 1
| `Version
| `Help
| `Ok () -> exit 0
try exit (Cmd.eval ~catch:false sercomp_cmd)
with exn ->
let (e, info) = Exninfo.capture exn in
fatal_exn e info
Expand Down
20 changes: 9 additions & 11 deletions sertop/sername.ml
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ let create_document ~require_lib ~in_file ~stm_flags ~quick ~ml_load_path ~vo_lo
*)
let doc,sid = Stm.new_doc ndoc in
let sent = Printf.sprintf "Require %s." l in
let in_strm = Stream.of_string sent in
let in_strm = Serapi.Ser_stream.of_string sent in
let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file})) in_strm in
match Stm.parse_sentence ~doc ~entry:Pvernac.main_entry sid in_pa with
| Some ast ->
Expand Down Expand Up @@ -214,18 +214,16 @@ let main () =

let sername_cmd =
let open Sertop.Sertop_arg in
Term.(const driver
$ debug $ printer $ disallow_sprop $ async $ async_workers $ error_recovery $ quick $ prelude
$ ml_include_path $ load_path $ rload_path $ require_lib $ str_pp $ de_bruijn $ body $ input_file $ omit_loc $ omit_att $ omit_env $ exn_on_opaque
),
Term.info "sername" ~version:sername_version ~doc:sername_doc ~man:sername_man
let term =
Term.(const driver
$ debug $ printer $ disallow_sprop $ async $ async_workers $ error_recovery $ quick $ prelude
$ ml_include_path $ load_path $ rload_path $ require_lib $ str_pp $ de_bruijn $ body $ input_file $ omit_loc $ omit_att $ omit_env $ exn_on_opaque
) in
let info = Cmd.info "sername" ~version:sername_version ~doc:sername_doc ~man:sername_man in
Cmd.v info term
in

try match Term.eval ~catch:false sername_cmd with
| `Error _ -> exit 1
| `Version
| `Help
| `Ok () -> exit 0
try exit (Cmd.eval ~catch:false sername_cmd)
with exn ->
let (e, info) = Exninfo.capture exn in
fatal_exn e info
Expand Down
24 changes: 12 additions & 12 deletions sertop/sertok.ml
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ exception End_of_input
let input_doc ~pp ~in_file ~in_chan ~doc ~sid =
let open Format in
let stt = ref (doc, sid) in
let in_strm = Stream.of_channel in_chan in
let in_strm = Serapi.Ser_stream.of_channel in_chan in
let source = Loc.InFile { dirpath = None; file = in_file } in
let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial source) in_strm in
let in_bytes = load_file in_file in
Expand All @@ -116,7 +116,7 @@ let input_doc ~pp ~in_file ~in_chan ~doc ~sid =
Bytes.sub_string in_bytes begin_char (end_char - begin_char)
in
let l_post_st = CLexer.Lexer.State.get () in
let sstr = Stream.of_string istr in
let sstr = Serapi.Ser_stream.of_string istr in
try
CLexer.Lexer.State.set l_pre_st;
let lex = CLexer.Lexer.tok_func sstr in
Expand Down Expand Up @@ -207,18 +207,18 @@ let main () =

let sertok_cmd =
let open Sertop.Sertop_arg in
Term.(const driver
$ debug $ disallow_sprop $ printer $ async $ async_workers $ error_recovery $ quick $ prelude
$ ml_include_path $ load_path $ rload_path $ input_file $ omit_loc $ omit_att $ omit_env $ exn_on_opaque
),
Term.info "sertok" ~version:sertok_version ~doc:sertok_doc ~man:sertok_man
let term =
Term.(const driver
$ debug $ disallow_sprop $ printer $ async $ async_workers $ error_recovery $ quick $ prelude
$ ml_include_path $ load_path $ rload_path $ input_file $ omit_loc $ omit_att $ omit_env $ exn_on_opaque
) in
let info = Cmd.info "sertok" ~version:sertok_version ~doc:sertok_doc ~man:sertok_man in
Cmd.v info term
in

try match Term.eval ~catch:false sertok_cmd with
| `Error _ -> exit 1
| `Version
| `Help
| `Ok () -> exit 0
try
let ecode = Cmd.eval ~catch:false sertok_cmd in
exit ecode
with exn ->
let (e, info) = Exninfo.capture exn in
fatal_exn e info
Expand Down
17 changes: 7 additions & 10 deletions sertop/sertop_bin.ml
Original file line number Diff line number Diff line change
Expand Up @@ -78,16 +78,13 @@ let sertop_cmd =
`P "See the documentation on the project's webpage for more information"
]
in
Term.(const sertop
$ printer $ print0 $ debug $ disallow_sprop $ indices_matter $ length $ prelude $ ml_include_path $ no_init $topfile $ no_prelude $ load_path $ rload_path $ implicit_stdlib
$ async $ deep_edits $ async_workers $ error_recovery $ omit_loc $ omit_att $ omit_env $ exn_on_opaque ),
Term.info "sertop" ~version:sertop_version ~doc ~man
let term =
Term.(const sertop
$ printer $ print0 $ debug $ disallow_sprop $ indices_matter $ length $ prelude $ ml_include_path $ no_init $topfile $ no_prelude $ load_path $ rload_path $ implicit_stdlib
$ async $ deep_edits $ async_workers $ error_recovery $ omit_loc $ omit_att $ omit_env $ exn_on_opaque ) in
let info = Cmd.info "sertop" ~version:sertop_version ~doc ~man in
Cmd.v info term

let main () =
match Term.eval sertop_cmd with
| `Error _ -> exit 1
| `Version
| `Help
| `Ok () -> exit 0
let main () = exit (Cmd.eval sertop_cmd)

let _ = main ()

0 comments on commit 20f868b

Please sign in to comment.