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

6 files changed, 9 insertions, 10 deletions

diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh
index 86bc50b5cd..70071b9d60 100755
--- a/test-suite/misc/4722.sh
+++ b/test-suite/misc/4722.sh
@@ -4,12 +4,12 @@ set -e
 # create test files
 mkdir -p misc/4722
 ln -sf toto misc/4722/tata
-touch misc/4722.v
+touch misc/bug_4722.v
 
 # run test
-$coqtop "-R" "misc/4722" "Foo" -top Top -load-vernac-source misc/4722.v
+$coqc "-R" "misc/4722" "Foo" -top Top misc/bug_4722.v
 
 # clean up test files
 rm misc/4722/tata
 rmdir misc/4722
-rm misc/4722.v
+rm misc/bug_4722.v
diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh
index 0ca2c97d24..5fc171649e 100755
--- a/test-suite/misc/7704.sh
+++ b/test-suite/misc/7704.sh
@@ -4,4 +4,4 @@ set -e
 
 export PATH=$BIN:$PATH
 
-${coqtop#"$BIN"} -compile misc/aux7704.v
+${coqc#"$BIN"} misc/aux7704.v
diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v
index 6fdcf67684..1c95211a71 100644
--- a/test-suite/misc/aux7704.v
+++ b/test-suite/misc/aux7704.v
@@ -1,4 +1,3 @@
-
 Goal True /\ True.
 Proof.
   split.
diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
index a15a8fbee9..8523358303 100755
--- a/test-suite/misc/deps-checksum.sh
+++ b/test-suite/misc/deps-checksum.sh
@@ -3,4 +3,4 @@ rm -f misc/deps/A/*.vo misc/deps/B/*.vo
 $coqc -R misc/deps/A A misc/deps/A/A.v
 $coqc -R misc/deps/B A misc/deps/B/A.v
 $coqc -R misc/deps/B A misc/deps/B/B.v
-$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v
+$coqc -R misc/deps/B A -R misc/deps/A A misc/deps/checksum.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
index 6bb2ba2da0..551515b0d6 100755
--- a/test-suite/misc/deps-order.sh
+++ b/test-suite/misc/deps-order.sh
@@ -10,12 +10,12 @@ R=$?
 times
 $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1
-$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1
+$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1
 S=$?
 if [ $R = 0 ] && [ $S = 0 ]; then
-    printf "coqdep and coqtop agree\n"
+    printf "coqdep and coqc agree\n"
     exit 0
 else
-    printf "coqdep and coqtop disagree\n"
+    printf "coqdep and coqc disagree\n"
     exit 1
 fi
diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh
index acb45b2292..af69370ce4 100755
--- a/test-suite/misc/deps-utf8.sh
+++ b/test-suite/misc/deps-utf8.sh
@@ -8,7 +8,7 @@ rm -f misc/deps/théorèmes/*.v
 tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX)
 $coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v
 R=$?
-$coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v
+$coqc -R misc/deps AlphaBêta misc/deps/αβ/εζ.v
 S=$?
 if [ $R = 0 ] && [ $S = 0 ]; then
     exit 0