[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

This PR deprecates the use of `coqtop` as a compiler.

There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.

We adapt the documentation and adapt the test-suite.

Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.

The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.

3 files changed, 41 insertions, 23 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index eaa050bdce..f822c68843 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -323,6 +323,12 @@ let usage batch =
   then Usage.print_usage_coqc ()
   else Usage.print_usage_coqtop ()
 
+let deprecated_coqc_warning = CWarnings.(create
+    ~name:"deprecate-compile-arg"
+    ~category:"toplevel"
+    ~default:Enabled
+    (fun opt_name -> Pp.(seq [str "The option "; str opt_name; str" is deprecated, please use coqc."])))
+
 (* Main parsing routine *)
 let parse_args init_opts arglist : coq_cmdopts * string list =
   let args = ref arglist in
@@ -436,10 +442,12 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
       Flags.compat_version := v;
       add_compat_require oval v
 
-    |"-compile" ->
+    |"-compile" as opt ->
+      deprecated_coqc_warning opt;
       add_compile oval false (next ())
 
-    |"-compile-verbose" ->
+    |"-compile-verbose" as opt ->
+      deprecated_coqc_warning opt;
       add_compile oval true (next ())
 
     |"-dump-glob" ->
@@ -519,7 +527,9 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
         CWarnings.set_flags (CWarnings.normalize_flags_string w);
         oval
 
-    |"-o" -> { oval with compilation_output_name = Some (next()) }
+    |"-o" as opt ->
+      deprecated_coqc_warning opt;
+      { oval with compilation_output_name = Some (next()) }
 
     |"-bytecode-compiler" ->
       { oval with enable_VM = get_bool opt (next ()) }
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index c43538017c..53bfeddf00 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -23,7 +23,7 @@ let machine_readable_version ret =
 let extra_usage = ref []
 let add_to_usage name text = extra_usage := (name,text) :: !extra_usage
 
-let print_usage_channel co command =
+let print_usage_common co command =
   output_string co command;
   output_string co "Coq options are:\n";
   output_string co
@@ -48,9 +48,6 @@ let print_usage_channel co command =
 \n  -lv f	                 (idem)\
 \n  -load-vernac-object f  load Coq object file f.vo\
 \n  -require path          load Coq library path and import it (Require Import path.)\
-\n  -compile f.v           compile Coq file f.v (implies -batch)\
-\n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
-\n  -o f.vo                use f.vo as the output file name\
 \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\
@@ -66,16 +63,15 @@ let print_usage_channel co command =
 \n  -quiet                 unset display of extra information (implies -w \"-all\")\
 \n  -w (w1,..,wn)          configure display of warnings\
 \n  -color (yes|no|auto)   configure color output\
+\n  -emacs                 tells Coq it is executed under Emacs\
 \n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
-\n  -batch                 batch mode (exits just after arguments parsing)\
 \n  -boot                  boot mode (implies -q and -batch)\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -diffs (on|off|removed) highlight differences between proof steps\
 \n  -stm-debug             STM debug mode (will trace every transaction)\
-\n  -emacs                 tells Coq it is executed under Emacs\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -impredicative-set     set sort Set impredicative\
@@ -101,21 +97,36 @@ let print_usage_channel co command =
 
 (* print the usage on standard error *)
 
-let print_usage = print_usage_channel stderr
-
 let print_usage_coqtop () =
-  print_usage "Usage: coqtop <options>\n\n";
+  print_usage_common stderr "Usage: coqtop <options>\n\n";
+  output_string stderr "\n\
+coqtop specific options:\
+\n\
+\n  -batch                 batch mode (exits just after arguments parsing)\
+\n\
+\nDeprecated options [use coqc instead]:\
+\n\
+\n  -compile f.v           compile Coq file f.v (implies -batch)\
+\n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
+\n  -o f.vo                use f.vo as the output file name\
+\n";
   flush stderr ;
   exit 1
 
 let print_usage_coqc () =
-  print_usage "Usage: coqc <options> <Coq options> file...\n\
-\noptions are:\
-\n  -verbose  compile verbosely\
-\n  -image f  specify an alternative executable for Coq\
-\n  -opt      run the native-code version of Coq\
-\n  -byte     run the bytecode version of Coq\
-\n  -t        keep temporary files\n\n";
+  print_usage_common stderr "Usage: coqc <options> <Coq options> file...";
+  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\
+\nDeprecated options:\
+\n\
+\n  -image f               specify an alternative executable for Coq\
+\n  -opt                   run the native-code version of Coq\
+\n  -byte                  run the bytecode version of Coq\
+\n  -t                     keep temporary files\
+\n";
   flush stderr ;
   exit 1
-
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index fbb0117d45..64170adaa4 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -13,9 +13,6 @@
 val version : int -> 'a
 val machine_readable_version : int -> 'a
 
-(** {6 Prints the usage on the error output, preceeded by a user-provided message. } *)
-val print_usage : string -> unit
-
 (** {6 Enable toploop plugins to insert some text in the usage message. } *)
 val add_to_usage : string -> string -> unit