Merge PR coq#19979: Rocquify usage messages

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

tools/coqdep/lib/args.ml

@@ -39,7 +39,7 @@ let warn_unknown_option =
 
 let usage () =
   let open Printf in
-  eprintf " usage: coqdep [options] <filename>+\n";
+  eprintf " usage: rocq dep [options] <filename>+\n";
   eprintf " options:\n";
   eprintf "  -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
   eprintf "  -sort : output the given file name ordered by dependencies\n";

tools/coqdoc/cmdArgs.ml

@@ -12,7 +12,7 @@
 open Common
 
 let banner () =
-  Printf.eprintf "This is coqdoc version %s\n" Coq_config.version;
+  Printf.eprintf "This is rocq doc version %s\n" Coq_config.version;
   flush stderr
 
 let normalize_path p =
@@ -226,11 +226,11 @@ let args_options = Arg.align [
   " First line comments of the form (** * ModuleName : text *) will be interpreted as subtitles";
   "--inline-notmono", arg_set (fun p -> { p with inline_notmono = true }),
   " Use a proportional width font for inline code (possibly with a different color)";
-  "--version", Arg.Unit (fun () -> banner()), " Display coqdoc version";
+  "--version", Arg.Unit (fun () -> banner()), " Display rocq doc version";
 ]
 
 let add_input_files f = prefs := { !prefs with files = what_file f :: !prefs.files }
-let usage_msg = "coqdoc [options] <input file>...\nAvailable options are:"
+let usage_msg = "rocq doc [options] <input file>...\nAvailable options are:"
 
 let single_hyphen_opts =
   ["-html"; "-latex"; "-texmacs"; "-raw"; "-dvi"; "-ps"; "-pdf"; "-stdout"; "-output"; "-directory"; "-gallina"; "-short"; "-light"; "-title"; "-body-only"; "-no-preamble"; "-with-header"; "-with-footer"; "-no-index"; "-multi-index"; "-index"; "-toc"; "-table-of-contents"; "-vernac-file"; "-tex-file"; "-preamble"; "-files-from"; "-files"; "-glob-from"; "-no-glob"; "-quiet"; "-verbose"; "-no-externals"; "-external"; "-coqlib_url"; "-coqlib"; "-latin1"; "-utf8"; "-charset"; "-inputenc"; "-interpolate"; "-raw-comments"; "-parse-comments"; "-plain-comments"; "-toc-depth"; "-no-lib-name"; "-lib-name"; "-lib-subtitles"; "-inline-notmono"; "-version"]

tools/coqworkmgr/rocqworkmgr.ml

@@ -158,7 +158,7 @@ let parse_args argv =
     "-j",Arg.Set_int max_tokens, "max number of concurrent jobs";
     "-d",Arg.Set debug, "do not detach (debug)"] in
   let usage =
-    "Prints on stdout an env variable assignment to be picked up by coq\n"^
+    "Prints on stdout an env variable assignment to be picked up by rocq\n"^
     "instances in order to limit the maximum number of concurrent workers.\n"^
     "The default value is 2.\n"^
     "Usage:" in

tools/rocqmakefile.ml

@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* Coq_makefile: automatically create a Makefile for a Coq development *)
+(* rocq makefile: automatically create a Makefile for a Rocq development *)
 
 open CoqProject_file
 open Printf
@@ -19,7 +19,7 @@ let usage_coq_makefile ~ok =
   let out = if ok then stdout else stderr in
   output_string out "Usage summary:\
 \n\
-\ncoq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\
+\nrocq makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\
 \n  ... [-I dir] ... [-R physicalpath logicalpath]\
 \n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
 \n  ... [-arg opt] ... [-docroot path] [-f file] [-o file]\

tools/rocqwc.mll

@@ -8,10 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* coqwc - counts the lines of spec, proof and comments in Coq sources
+(* rocq wc - counts the lines of spec, proof and comments in Coq sources
  * Copyright (C) 2003 Jean-Christophe Filliâtre *)
 
-(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
+(*s {\bf rocq wc.} Counts the lines of spec, proof and comments in a Coq source.
     It assumes the files to be lexically well-formed. *)
 
 (*i*){
@@ -250,12 +250,12 @@ let process_file f =
     update_totals ()
   with
     | Sys_error s ->
-        flush stdout; eprintf "coqwc: %s: %s\n" f s; flush stderr
+        flush stdout; eprintf "rocq wc: %s: %s\n" f s; flush stderr
 
 (*s Parsing of the command line. *)
 
 let usage () =
-  prerr_endline "usage: coqwc [options] [files]";
+  prerr_endline "usage: rocq wc [options] [files]";
   prerr_endline "Options are:";
   prerr_endline "  -p   print percentage of comments";
   prerr_endline "  -s   print only the spec size";

topbin/rocqnative.ml

@@ -292,7 +292,7 @@ struct
 
 let print_usage_channel co command =
   output_string co command;
-  output_string co "coqnative options are:\n";
+  output_string co "rocq native-precompile options are:\n";
   output_string co
 "  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -R dir coqdir          synonymous for -Q\
@@ -311,7 +311,7 @@ let print_usage_channel co command =
 let print_usage = print_usage_channel stderr
 
 let print_usage_coqnative () =
-  print_usage "Usage: coqnative <options> file\n\n"
+  print_usage "Usage: rocq native-precompile <options> file\n\n"
 
 let usage () =
   print_usage_coqnative ();

toplevel/coqc.ml

@@ -20,10 +20,10 @@ let coqc_init ((_,color_mode),_) injections ~opts =
   injections
 
 let coqc_specific_usage = Boot.Usage.{
-  executable_name = "coqc";
+  executable_name = "rocq compile";
   extra_args = "file...";
   extra_options = "\n\
-coqc specific options:\
+rocq compile specific options:\
 \n  -o f.vo                use f.vo as the output file name\
 \n  -verbose               compile and output the input file\
 \n  -noglob                do not dump globalizations\

toplevel/coqtop.ml

@@ -12,7 +12,7 @@ open Pp
 open Coqargs
 
 (** This file provides generic support for Coq executables + specific
-    support for the coqtop executable *)
+    support for the rocq repl executable *)
 
 let () = at_exit flush_all
 
@@ -80,7 +80,7 @@ let start_coq custom args =
   custom.run ~opts custom_opts state
 
 (** ****************************************)
-(** Specific support for coqtop executable *)
+(** Specific support for rocq repl executable *)
 
 let ltac_debug_answer = let open DebugHook.Answer in function
     | Prompt prompt ->
@@ -184,10 +184,10 @@ let coqtop_run ({ run_mode; color_mode },_) ~opts state =
   | Batch -> exit 0
 
 let coqtop_specific_usage = Boot.Usage.{
-  executable_name = "coqtop";
+  executable_name = "rocq repl";
   extra_args = "";
   extra_options = "\n\
-coqtop specific options:\n\
+rocq repl specific options:\n\
 \n  -batch                 batch mode (exits after interpretation of command line)\
 \n"
 }