From dd15e030be5e55d3770d27fbbc2fe0f5384f0166 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 19:42:08 +0200 Subject: Adding methods help and parse_extra to custom toplevels data. In particular, method init does not do parsing any more. This allows for instance to let coqidetop treats itself the "-filteropts" option. --- toplevel/workerLoop.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'toplevel/workerLoop.ml') diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index d362f9db22..6d147ac308 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -13,18 +13,21 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let arg_init init ~opts extra_args = - let extra_args = parse extra_args in +let worker_parse_extra ~opts extra_args = + opts, parse extra_args + +let worker_init init ~opts = Flags.quiet := true; init (); - CoqworkmgrApi.(init !async_proofs_worker_priority); - opts, extra_args + CoqworkmgrApi.(init !async_proofs_worker_priority) let start ~init ~loop = let open Coqtop in let custom = { + parse_extra = worker_parse_extra; + help = (fun _ -> output_string stderr "Same options as coqtop"); opts = Coqargs.default; - init = arg_init init; + init = worker_init init; run = (fun ~opts:_ ~state:_ -> loop ()); } in start_coq custom -- cgit v1.2.3 From e55ba2f04578738ec72c4ca64daf23b9ea51ec06 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 May 2019 00:36:49 +0200 Subject: An attempt to reorganize further coqtop initialization into semantic units. Incidentally moving parsing of "-batch" to the coqtop binary. --- toplevel/workerLoop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/workerLoop.ml') diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 6d147ac308..1fcc106348 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -14,7 +14,7 @@ let rec parse = function | [] -> [] let worker_parse_extra ~opts extra_args = - opts, parse extra_args + Coqtop.Interactive, parse extra_args let worker_init init ~opts = Flags.quiet := true; -- cgit v1.2.3 From 2bdfddc39d1fd6200042ddb95ded98b44e14b8e5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 11:24:51 +0200 Subject: Passing command-line option async_proofs_worker_priority functionally. We lose track of it at some time in "known_state" and assume that the reference cur_opt has not been modified in between the time it was set (in "new_doc") and "known_state". --- toplevel/workerLoop.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'toplevel/workerLoop.ml') diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 1fcc106348..c2bd8213b0 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -18,8 +18,7 @@ let worker_parse_extra ~opts extra_args = let worker_init init ~opts = Flags.quiet := true; - init (); - CoqworkmgrApi.(init !async_proofs_worker_priority) + init () let start ~init ~loop = let open Coqtop in -- cgit v1.2.3 From 01c965e1989cbc528d46b1751d8c2c708542da4e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 20:26:30 +0200 Subject: Some common points between coqc and other coq binaries. - Binding coqc execution to the generic support for Coq binaries (i.e. to start_coq). - Moving init_toploop to the init part of coq executables so that coqc can avoid to call it. By the way, it is unclear what workerloop should do with it. Also, it is unclear how much the -l option should be considered an coqidetop or coq*worker option. In any case, it should be disallowed in coqc, I guess? - Moving the custom init part at the end of the initialization phase. Seems ok, despites the few involved side effects. --- toplevel/workerLoop.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'toplevel/workerLoop.ml') diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index c2bd8213b0..0087e4833c 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -14,11 +14,12 @@ let rec parse = function | [] -> [] let worker_parse_extra ~opts extra_args = - Coqtop.Interactive, parse extra_args + (), parse extra_args -let worker_init init ~opts = +let worker_init init () ~opts = Flags.quiet := true; - init () + init (); + Coqtop.init_toploop opts let start ~init ~loop = let open Coqtop in @@ -27,6 +28,6 @@ let start ~init ~loop = help = (fun _ -> output_string stderr "Same options as coqtop"); opts = Coqargs.default; init = worker_init init; - run = (fun ~opts:_ ~state:_ -> loop ()); + run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); } in start_coq custom -- cgit v1.2.3 From fe487e8eaae3186803ec657c517d0ebebab3bafd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 22:42:48 +0200 Subject: An even more uniform treatment of the -help option across executables. Incidentally fix some missing newline in coqc help, and give proper help for coqidetop and the "coq*worker"s. --- toplevel/workerLoop.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'toplevel/workerLoop.ml') diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 0087e4833c..3af48bad99 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -21,11 +21,13 @@ let worker_init init () ~opts = init (); Coqtop.init_toploop opts -let start ~init ~loop = +let start ~init ~loop name = + let _ = Usage.add_to_usage name "" ("\n" ^ name ^ " specific options:\ +\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n") in let open Coqtop in let custom = { parse_extra = worker_parse_extra; - help = (fun _ -> output_string stderr "Same options as coqtop"); + help = Usage.print_usage name; opts = Coqargs.default; init = worker_init init; run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); -- cgit v1.2.3 From f2779d48d3b7735687444e22b16cdb7cb8f7ce60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 09:36:57 +0200 Subject: Usage: bypassing a useless detour via a reference. --- toplevel/workerLoop.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'toplevel/workerLoop.ml') diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 3af48bad99..5f80ac475c 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -21,13 +21,18 @@ let worker_init init () ~opts = init (); Coqtop.init_toploop opts +let worker_specific_usage name = Usage.{ + executable_name = name; + extra_args = ""; + extra_options = ("\n" ^ name ^ " specific options:\ +\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n"); +} + let start ~init ~loop name = - let _ = Usage.add_to_usage name "" ("\n" ^ name ^ " specific options:\ -\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n") in let open Coqtop in let custom = { parse_extra = worker_parse_extra; - help = Usage.print_usage name; + help = worker_specific_usage name; opts = Coqargs.default; init = worker_init init; run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); -- cgit v1.2.3