[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.

2 files changed, 30 insertions, 11 deletions

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 9ecd8f19ce..8f6c4c0968 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo =
   (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *)
   let libflag = "-coqlib %{project_root}" in
   (* The final build rule *)
-  let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in
+  let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -w -deprecate-compile-arg -compile %s))" libflag eflag cflag source in
   let all_targets = gen_coqc_targets vo in
   pp_rule fmt all_targets deps action
 
diff --git a/tools/coqc.ml b/tools/coqc.ml
index ae841212a7..0f65823740 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -32,8 +32,9 @@ let verbose = ref false
 let rec make_compilation_args = function
   | [] -> []
   | file :: fl ->
-      (if !verbose then "-compile-verbose" else "-compile")
-      :: file :: (make_compilation_args fl)
+    "-w" :: "-deprecate-compile-arg"
+    :: (if !verbose then "-compile-verbose" else "-compile")
+    :: file :: (make_compilation_args fl)
 
 (* compilation of files [files] with command [command] and args [args] *)
 
@@ -61,16 +62,28 @@ let usage () =
 (* parsing of the command line *)
 let extra_arg_needed = ref true
 
+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."])))
+
 let parse_args () =
   let rec parse (cfiles,args) = function
     | [] ->
 	List.rev cfiles, List.rev args
     | ("-verbose" | "--verbose") :: rem ->
 	verbose := true ; parse (cfiles,args) rem
-    | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
+    | "-image" :: f :: rem ->
+      deprecated_coqc_warning "-image";
+      image := f; parse (cfiles,args) rem
     | "-image" :: [] ->	usage ()
-    | "-byte" :: rem -> use_bytecode := true; parse (cfiles,args) rem
-    | "-opt" :: rem -> use_bytecode := false; parse (cfiles,args) rem
+    | "-byte" :: rem ->
+      deprecated_coqc_warning "-byte";
+      use_bytecode := true; parse (cfiles,args) rem
+    | "-opt" :: rem ->
+      deprecated_coqc_warning "-opt";
+      use_bytecode := false; parse (cfiles,args) rem
 
 (* Informative options *)
 
@@ -87,7 +100,7 @@ let parse_args () =
         Envars.set_coqlib ~fail:(fun x -> x);
         Envars.print_config stdout Coq_config.all_src_dirs;
         exit 0
-      
+
     | ("-print-version" | "--print-version") :: _ ->
         Usage.machine_readable_version 0
 
@@ -97,7 +110,7 @@ let parse_args () =
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-profile"|"-echo" |"-quiet"
       |"-silent"|"-m"|"-beautify"|"-strict-implicit"
-      |"-impredicative-set"|"-vm"
+      |"-impredicative-set"|"-vm"|"-test-mode"|"-emacs"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       |"-stm-debug"
@@ -108,22 +121,28 @@ let parse_args () =
 
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
-      |"-load-ml-source"|"-require"|"-load-ml-object"
+      |"-load-ml-source"|"-require"|"-load-ml-object"|"-async-proofs-cache"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"|"-topfile"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
-      |"-o"|"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler"
+      |"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler"
       as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
 	    | []        -> usage ()
 	end
+    | "-o" :: rem->
+        begin
+          match rem with
+            | s :: rem' -> parse (cfiles,s::"-o"::args) rem'
+            | []        -> usage ()
+        end
     | ("-I"|"-include" as o) :: s :: rem -> parse (cfiles,s::o::args) rem
 
 (* Options for coqtop : c) options with 1 argument and possibly more *)
 
     | ("-R"|"-Q" as o) :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
-    | ("-schedule-vio-checking"
+    | ("-schedule-vio-checking"|"-vio2vo"
       |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem ->
         let nodash, rem =
           CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in