aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/idetop.ml8
-rw-r--r--topbin/coqproofworker_bin.ml2
-rw-r--r--topbin/coqqueryworker_bin.ml2
-rw-r--r--topbin/coqtacticworker_bin.ml2
-rw-r--r--toplevel/coqargs.ml8
-rw-r--r--toplevel/coqargs.mli4
-rw-r--r--toplevel/coqc.ml17
-rw-r--r--toplevel/coqtop.ml11
-rw-r--r--toplevel/coqtop.mli2
-rw-r--r--toplevel/usage.ml48
-rw-r--r--toplevel/usage.mli8
-rw-r--r--toplevel/workerLoop.ml6
-rw-r--r--toplevel/workerLoop.mli4
13 files changed, 60 insertions, 62 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index f79ad5deab..eb76951b44 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -552,8 +552,10 @@ let rec parse = function
x :: parse rest
| [] -> []
-let () = Usage.add_to_usage "coqidetop"
-" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\
+let () = Usage.add_to_usage "coqidetop" "" "\n\
+coqidetop specific options:\n\
+\n --xml_formatinclude dir (idem)\
+\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\
\n --help-XML-protocol print documentation of the Coq XML protocol\n"
let islave_parse ~opts extra_args =
@@ -580,7 +582,7 @@ let () =
let open Coqtop in
let custom = {
parse_extra = islave_parse ;
- help = (fun _ -> output_string stderr "Same options as coqtop");
+ help = Usage.print_usage "coqidetop";
init = islave_init;
run = loop;
opts = islave_default_opts } in
diff --git a/topbin/coqproofworker_bin.ml b/topbin/coqproofworker_bin.ml
index baf76582ac..2715406b13 100644
--- a/topbin/coqproofworker_bin.ml
+++ b/topbin/coqproofworker_bin.ml
@@ -11,4 +11,4 @@
module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
let () =
- WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
+ WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqproofworker"
diff --git a/topbin/coqqueryworker_bin.ml b/topbin/coqqueryworker_bin.ml
index 0f7005e422..225158e064 100644
--- a/topbin/coqqueryworker_bin.ml
+++ b/topbin/coqqueryworker_bin.ml
@@ -10,4 +10,4 @@
module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
-let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
+let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqqueryworker"
diff --git a/topbin/coqtacticworker_bin.ml b/topbin/coqtacticworker_bin.ml
index 19a8cde88a..962028e0e7 100644
--- a/topbin/coqtacticworker_bin.ml
+++ b/topbin/coqtacticworker_bin.ml
@@ -10,4 +10,4 @@
module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
-let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
+let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqtacticworker"
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 5e3a82dcb9..b07639511c 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -81,7 +81,7 @@ type coqargs_pre = {
type coqargs_query =
| PrintTags | PrintWhere | PrintConfig
| PrintVersion | PrintMachineReadableVersion
- | PrintHelp of (unit -> unit)
+ | PrintHelp of (out_channel -> unit)
type coqargs_main =
| Queries of coqargs_query list
@@ -290,6 +290,7 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy
exception NoCoqLib
+(* Is this still useful for displaying help? *)
let usage help =
begin
try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
@@ -298,7 +299,7 @@ let usage help =
let lp = Coqinit.toplevel_init_load_path () in
(* Necessary for finding the toplevels below *)
List.iter Loadpath.add_coq_path lp;
- help ()
+ help
(* Main parsing routine *)
let parse_args ~help ~init arglist : t * string list =
@@ -554,7 +555,8 @@ let parse_args ~help ~init arglist : t * string list =
|"-type-in-type" -> set_type_in_type (); oval
|"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
|"-where" -> set_query oval PrintWhere
- |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp (fun () -> usage help))
+ |"-h"|"-H"|"-?"|"-help"|"--help" ->
+ set_query oval (PrintHelp (fun co -> usage (help co)))
|"-v"|"--version" -> set_query oval PrintVersion
|"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index d1873bcb58..46220cd1d8 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -56,7 +56,7 @@ type coqargs_pre = {
type coqargs_query =
| PrintTags | PrintWhere | PrintConfig
| PrintVersion | PrintMachineReadableVersion
- | PrintHelp of (unit -> unit)
+ | PrintHelp of (out_channel -> unit)
type coqargs_main =
| Queries of coqargs_query list
@@ -77,7 +77,7 @@ type t = {
(* Default options *)
val default : t
-val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
+val parse_args : help:(out_channel -> unit) -> init:t -> string list -> t * string list
val error_wrong_arg : string -> unit
val require_libs : t -> (string * string option * bool option) list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index fd275fdb1b..c905eff646 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -19,6 +19,21 @@ let coqc_init _copts ~opts =
Coqtop.init_color opts.Coqargs.config;
if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ()
+let () = Usage.add_to_usage "coqc" "file..." "\n\
+coqc specific options:\
+\n -o f.vo use f.vo as the output file name\
+\n -verbose compile and output the input file\
+\n -quick quickly compile .v files to .vio files (skip proofs)\
+\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\
+\n into fi.vo\
+\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\
+\n proofs in each fi.vio\
+\n\
+\nUndocumented:\
+\n -vio2vo [see manual]\
+\n -check-vio-tasks [see manual]\
+\n"
+
let coqc_main copts ~opts =
Topfmt.(in_phase ~phase:CompilationPhase)
Ccompile.compile_files opts copts;
@@ -53,7 +68,7 @@ let coqc_run copts ~opts () =
let custom_coqc = Coqtop.{
parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
- help = Usage.print_usage_coqc;
+ help = Usage.print_usage "coqc";
init = coqc_init;
run = coqc_run;
opts = Coqargs.default;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 95f9d9ef77..5194c7a128 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -159,7 +159,7 @@ let print_query opts = function
| PrintVersion -> Usage.version ()
| PrintMachineReadableVersion -> Usage.machine_readable_version ()
| PrintWhere -> print_endline (Envars.coqlib ())
- | PrintHelp f -> f ()
+ | PrintHelp f -> f stderr
| PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
| PrintTags -> print_style_tags opts.config
@@ -246,7 +246,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
type ('a,'b) custom_toplevel =
{ parse_extra : 'a extra_args_fn
- ; help : unit -> unit
+ ; help : out_channel -> unit
; init : 'a -> opts:Coqargs.t -> 'b
; run : 'a -> opts:Coqargs.t -> 'b -> unit
; opts : Coqargs.t
@@ -324,9 +324,14 @@ let coqtop_run run_mode ~opts state =
| Interactive -> Coqloop.loop ~opts ~state;
| Batch -> exit 0
+let () = Usage.add_to_usage "coqtop" "" "\n\
+coqtop specific options:\n\
+\n -batch batch mode (exits after interpretation of command line)\
+\n"
+
let coqtop_toplevel =
{ parse_extra = coqtop_parse_extra
- ; help = Usage.print_usage_coqtop
+ ; help = Usage.print_usage "coqtop"
; init = coqtop_init
; run = coqtop_run
; opts = Coqargs.default
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index e2339afbde..af1890bee5 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -17,7 +17,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
type ('a,'b) custom_toplevel =
{ parse_extra : 'a extra_args_fn
- ; help : unit -> unit
+ ; help : out_channel -> unit
; init : 'a -> opts:Coqargs.t -> 'b
; run : 'a -> opts:Coqargs.t -> 'b -> unit
; opts : Coqargs.t
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 011cc34987..636d4f8d5d 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -20,7 +20,8 @@ let machine_readable_version () =
(* print the usage of coqtop (or coqc) on channel co *)
let extra_usage = ref []
-let add_to_usage name text = extra_usage := (name,text) :: !extra_usage
+let add_to_usage name extra text =
+ extra_usage := (name,(extra,text)) :: !extra_usage
let print_usage_common co command =
output_string co command;
@@ -98,42 +99,13 @@ let print_usage_common co command =
\n -bytecode-compiler (yes|no) enable the vm_compute reduction machine\
\n -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
\n -h, -help, --help print this list of options\
-\n";
- List.iter (fun (name, text) ->
- output_string co
- ("\nWith the flag '-toploop "^name^
- "' these extra option are also available:\n"^
- text^"\n"))
- !extra_usage
+\n"
-(* print the usage on standard error *)
+(* print the usage *)
-let print_usage_coqtop () =
- print_usage_common stderr "Usage: coqtop <options>\n\n";
- output_string stderr "\n\
-coqtop specific options:\
-\n\
-\n -batch batch mode (exits just after argument parsing)\
-\n";
- flush stderr ;
- exit 1
-
-let print_usage_coqc () =
- print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n";
- output_string stderr "\n\
-coqc specific options:\
-\n\
-\n -o f.vo use f.vo as the output file name\
-\n -verbose compile and output the input file\
-\n -quick quickly compile .v files to .vio files (skip proofs)\
-\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\
-\n into fi.vo\
-\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\
-\n proofs in each fi.vio\
-\n\
-\nUndocumented:\
-\n -vio2vo [see manual]\
-\n -check-vio-tasks [see manual]\
-\n";
- flush stderr ;
- exit 1
+let print_usage binfile co =
+ let extra, text =
+ try List.assoc binfile !extra_usage
+ with Not_found -> ("","") in
+ print_usage_common co ("Usage: " ^ binfile ^ " <options> " ^ extra ^ "\n\n");
+ output_string co text
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 7d658579fd..7d80598b7e 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -13,10 +13,10 @@
val version : unit -> unit
val machine_readable_version : unit -> unit
-(** {6 Enable toploop plugins to insert some text in the usage message. } *)
-val add_to_usage : string -> string -> unit
+(** {6 [add_to_usage name extra_args extra_options] tell what extra
+ arguments or options to print when asking usage for command [name]. } *)
+val add_to_usage : string -> string -> string -> unit
(** {6 Prints the usage on the error output. } *)
-val print_usage_coqtop : unit -> unit
-val print_usage_coqc : unit -> unit
+val print_usage : string -> out_channel -> unit
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 ());
diff --git a/toplevel/workerLoop.mli b/toplevel/workerLoop.mli
index 685a10f6f3..8d6f0b1988 100644
--- a/toplevel/workerLoop.mli
+++ b/toplevel/workerLoop.mli
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(* Register a STM worker *)
+(* Register a STM worker of a given executable name *)
val start :
init:(unit -> unit) ->
- loop:(unit -> unit) -> unit
+ loop:(unit -> unit) -> string -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:58:02 +0000