Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes

36 files changed, 158 insertions, 130 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 03f991566e..4d0063115b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -22,6 +22,11 @@ Coqide
 
 Coqtop
 
+- the use of `coqtop` as a compiler has been deprecated, in favor of
+  `coqc`. Consequently option `-compile` will stop to be accepted in
+  the next release. `coqtop` is now reserved to interactive
+  use. (@ejgallego #9095)
+
 - new option -topfile filename, which will set the current module name
   (à la -top) based on the filename passed, taking into account the
   proper -R/-Q options. For example, given -R Foo foolib using
diff --git a/Makefile.build b/Makefile.build
index e683a6bda8..4f42768227 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -198,7 +198,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
 COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
-BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
+BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -w -deprecate-compile-arg -compile
 
 LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
 MLINCLUDES=$(LOCALINCLUDES)
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 29e87df6b8..8455d13377 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -10,7 +10,7 @@ In Coq source folder:
 opam switch 4.05.0+trunk+fp
 ./configure -local -debug
 make
-perf record -g bin/coqtop -compile file.v
+perf record -g bin/coqc file.v
 perf report -g fractal,callee --no-children
 
 To profile only part of a file, first load it using
@@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev
 
 ### For memory dump:
 
-CAMLRUNPARAM=T,mj bin/coqtop -compile file.v
+CAMLRUNPARAM=T,mj bin/coqc file.v
 
 In another terminal:
 
@@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated.
 
 ### For complete memory graph:
 
-CAMLRUNPARAM=T,gr bin/coqtop -compile file.v
+CAMLRUNPARAM=T,gr bin/coqc file.v
 
 In another terminal:
 
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 8b7214e2ab..903ee115c9 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -52,7 +52,7 @@ in interactive mode.
 It is not strictly mandatory in batch mode if it is not the first time
 the file is compiled and if the file itself did not change. When the
 proof does not begin with Proof using, the system records in an
-auxiliary file, produced along with the `.vo` file, the list of section
+auxiliary file, produced along with the ``.vo`` file, the list of section
 variables used.
 
 Automatic suggestion of proof annotations
@@ -154,22 +154,22 @@ to a worker process. The threshold can be configured with
 Batch mode
 ---------------
 
-When |Coq| is used as a batch compiler by running `coqc` or `coqtop`
--compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains,
-among other things, theorem statements and proofs. Hence to produce a
-.vo |Coq| need to process all the proofs of the `.v` file.
+When |Coq| is used as a batch compiler by running ``coqc``, it produces
+a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other
+things, theorem statements and proofs. Hence to produce a .vo |Coq|
+need to process all the proofs of the ``.v`` file.
 
 The asynchronous processing of proofs can decouple the generation of a
-compiled file (like the `.vo` one) that can be loaded by ``Require`` from the
+compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the
 generation and checking of the proof objects. The ``-quick`` flag can be
-passed to `coqc` or `coqtop` to produce, quickly, `.vio` files.
-Alternatively, when using a Makefile produced by `coq_makefile`,
+passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files.
+Alternatively, when using a Makefile produced by ``coq_makefile``,
 the ``quick`` target can be used to compile all files using the ``-quick`` flag.
 
-A `.vio` file can be loaded using ``Require`` exactly as a `.vo` file but
+A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but
 proofs will not be available (the Print command produces an error).
 Moreover, some universe constraints might be missing, so universes
-inconsistencies might go unnoticed. A `.vio` file does not contain proof
+inconsistencies might go unnoticed. A ``.vio`` file does not contain proof
 objects, but proof tasks, i.e. what a worker process can transform
 into a proof object.
 
@@ -177,52 +177,52 @@ Compiling a set of files with the ``-quick`` flag allows one to work,
 interactively, on any file without waiting for all the proofs to be
 checked.
 
-When working interactively, one can fully check all the `.v` files by
-running `coqc` as usual.
+When working interactively, one can fully check all the ``.v`` files by
+running ``coqc`` as usual.
 
-Alternatively one can turn each `.vio` into the corresponding `.vo`. All
+Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All
 .vio files can be processed in parallel, hence this alternative might
 be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to
-obtain a good scheduling for two workers to produce `a.vo`, `b.vo`, and
-`c.vo`. When using a Makefile produced by `coq_makefile`, the ``vio2vo`` target
-can be used for that purpose. Variable `J` should be set to the number
+obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and
+``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target
+can be used for that purpose. Variable ``J`` should be set to the number
 of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the
-.vo files obtained from `.vio` files are complete (they contain all proof
+.vo files obtained from ``.vio`` files are complete (they contain all proof
 terms and universe constraints), the satisfiability of all universe
 constraints has not been checked globally (they are checked to be
 consistent for every single proof). Constraints will be checked when
-these `.vo` files are (recursively) loaded with ``Require``.
+these ``.vo`` files are (recursively) loaded with ``Require``.
 
 There is an extra, possibly even faster, alternative: just check the
-proof tasks stored in `.vio` files without producing the `.vo` files. This
+proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This
 is possibly faster because all the proof tasks are independent, hence
 one can further partition the job to be done between workers. The
 ``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a
-good scheduling for 6 workers to check all the proof tasks of `a.vio`,
-`b.vio`, and `c.vio`. Auxiliary files are used to predict how long a proof
+good scheduling for 6 workers to check all the proof tasks of ``a.vio``,
+``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof
 task will take, assuming it will take the same amount of time it took
 last time. When using a Makefile produced by coq_makefile, the
-``checkproofs`` target can be used to check all `.vio` files. Variable `J`
+``checkproofs`` target can be used to check all ``.vio`` files. Variable ``J``
 should be set to the number of workers, e.g. ``make checkproofs J=6``. As
-when converting `.vio` files to `.vo` files, universe constraints are not
+when converting ``.vio`` files to ``.vo`` files, universe constraints are not
 checked to be globally consistent. Hence this compilation mode is only
 useful for quick regression testing and on developments not making
-heavy use of the `Type` hierarchy.
+heavy use of the ``Type`` hierarchy.
 
 Limiting the number of parallel workers
 --------------------------------------------
 
 Many |Coq| processes may run on the same computer, and each of them may
-start many additional worker processes. The `coqworkmgr` utility lets
+start many additional worker processes. The ``coqworkmgr`` utility lets
 one limit the number of workers, globally.
 
 The utility accepts the ``-j`` argument to specify the maximum number of
-workers (defaults to 2). `coqworkmgr` automatically starts in the
+workers (defaults to 2). ``coqworkmgr`` automatically starts in the
 background and prints an environment variable assignment
 like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable
 in all the shells from which |Coq| processes will be started. If one
 uses just one terminal running the bash shell, then
 ``export ‘coqworkmgr -j 4‘`` will do the job.
 
-After that, all |Coq| processes, e.g. `coqide` and `coqc`, will respect the
+After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the
 limit, globally.
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 9bc67147f7..1b4d2315aa 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -163,14 +163,14 @@ and ``coqtop``, unless stated otherwise:
   is equivalent to runningRequire dirpath.
 :-require dirpath: Load |Coq| compiled library dirpath and import it.
   This is equivalent to running Require Import dirpath.
-:-batch: Exit just after argument parsing. Available for `coqtop` only.
-:-compile *file.v*: Compile file *file.v* into *file.vo*. This option
+:-batch: Exit just after argument parsing. Available for ``coqtop`` only.
+:-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option
   implies -batch (exit just after argument parsing). It is available only
-  for `coqtop`, as this behavior is the purpose of `coqc`.
-:-compile-verbose *file.v*: Same as -compile but also output the
+  for `coqtop`, as this behavior is the purpose of ``coqc``.
+:-compile-verbose *file.v*: Deprecated. Use ``coqc -verbose``. Same as -compile but also output the
   content of *file.v* as it is compiled.
 :-verbose: Output the content of the input file as it is compiled.
-  This option is available for `coqc` only; it is the counterpart of
+  This option is available for ``coqc`` only; it is the counterpart of
   -compile-verbose.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
@@ -211,11 +211,11 @@ and ``coqtop``, unless stated otherwise:
   (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being
   compiled, *file.glob* is used.
 :-no-glob: Disable the dumping of references for global names.
-:-image *file*: Set the binary image to be used by `coqc` to be *file*
+:-image *file*: Set the binary image to be used by ``coqc`` to be *file*
   instead of the standard one. Not of general use.
 :-bindir *directory*: Set the directory containing |Coq| binaries to be
-  used by `coqc`. It is equivalent to doing export COQBIN= *directory*
-  before launching `coqc`.
+  used by ``coqc``. It is equivalent to doing export COQBIN= *directory*
+  before launching ``coqc``.
 :-where: Print the location of |Coq|’s standard library and exit.
 :-config: Print the locations of |Coq|’s binaries, dependencies, and
   libraries, then exit.
diff --git a/man/coqtop.1 b/man/coqtop.1
index 084adfe453..addfb54672 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -85,22 +85,6 @@ load Coq library
 and import it (Require Import path.)
 
 .TP
-.BI \-compile \ filename.v
-compile Coq file
-.I filename.v 
-(implies 
-.B \-batch
-)
-
-.TP
-.BI \-compile\-verbose \ filename.v
-verbosely compile Coq file
-.I filename.v
-(implies 
-.B \-batch
-)
-
-.TP
 .B \-where
 print Coq's standard library location and exit
 
@@ -125,8 +109,6 @@ batch mode (exits just after arguments parsing)
 .B \-boot
 boot mode (implies
 .B \-q
-and
-.B \-batch
 )
 
 .TP
diff --git a/stm/stm.ml b/stm/stm.ml
index dfe5581ed5..0165b3c029 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1671,7 +1671,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_debug (Pp.str "STM: sending back a fat state");
+        if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 37091a49e5..111bd52a33 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -38,14 +38,15 @@ LIB := ..
 BIN := $(shell cd ..; pwd)/bin/
 COQFLAGS?=
 
-coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS)
+coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS)
 coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS)
 coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 coqdoc := $(BIN)coqdoc
+coqtop := $(BIN)coqtop -batch -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite
 coqtopbyte := $(BIN)coqtop.byte
 
-coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source
-coqtopcompile := $(coqtop) -async-proofs-cache force -compile
+coqc_interactive := $(coqc) -async-proofs-cache force
+coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force
 coqdep := $(BIN)coqdep -coqlib $(LIB)
 
 VERBOSE?=
@@ -60,12 +61,8 @@ SINGLE_QUOTE="
 #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
 # wrap the arguments in parens, but only if they exist
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
-# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
-has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
-get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload))
 get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1)))
 
-
 bogomips:=
 ifneq (,$(wildcard /proc/cpuinfo))
   sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
@@ -209,7 +206,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
 	@echo "TEST      $<  $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...still active"; \
@@ -231,7 +228,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -297,7 +294,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...could not be prepared" ; \
@@ -316,7 +313,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -342,7 +339,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
 	    $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
@@ -367,7 +364,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -392,7 +389,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  output=$*.out.real; \
-	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	  $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
@@ -431,7 +428,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	  echo $(call log_intro,$<); \
 	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
 	  tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \
-	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	  $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
@@ -486,7 +483,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+	  res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
@@ -517,7 +514,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	      echo $(log_success); \
 	      echo "    $<...still wished"; \
@@ -531,7 +528,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG
 # Additional dependencies for module tests
 $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
 modules/%.vo: modules/%.v
-	$(HIDE)$(coqtop) -R modules Mods -compile $<
+	$(HIDE)$(coqc) -R modules Mods $<
 
 #######################################################################
 # Miscellaneous tests
@@ -550,7 +547,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	  echo $(call log_intro,$<); \
 	  export BIN="$(BIN)"; \
 	  export coqc="$(coqc)"; \
-	  export coqtop="$(coqtop)"; \
+	  export coqtop="$(coqc_boot)"; \
 	  export coqdep="$(coqdep)"; \
 	  export coqtopbyte="$(coqtopbyte)"; \
 	  "$<" 2>&1; R=$$?; times; \
@@ -591,7 +588,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  $(coqc) -quick -R vio vio $* 2>&1 && \
-	  $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
+	  $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \
 	  $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
index 5838dcd8a7..9aefb10172 100644
--- a/test-suite/bugs/closed/bug_4836.v
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
+(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_7811.v b/test-suite/bugs/closed/bug_7811.v
index fee330f22d..155f3285b7 100644
--- a/test-suite/bugs/closed/bug_7811.v
+++ b/test-suite/bugs/closed/bug_7811.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *)
 (* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3
    coqtop version 8.8.0 (May 2018) *)
diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v
index c5e1953829..31217ca75e 100644
--- a/test-suite/complexity/constructor.v
+++ b/test-suite/complexity/constructor.v
@@ -214,3 +214,4 @@ Fixpoint expand (n : nat) : Prop :=
 
 Example Expand : expand 2500.
 Time constructor. (* ~0.45 secs *)
+Qed.
diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v
index 86698fa872..c2c566930b 100644
--- a/test-suite/complexity/f_equal.v
+++ b/test-suite/complexity/f_equal.v
@@ -12,3 +12,4 @@ end.
 
 Goal stupid 23 = stupid 23.
 Timeout 5 Time f_equal.
+Abort.
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
index a76fa19d3c..298a07c1c4 100644
--- a/test-suite/complexity/injection.v
+++ b/test-suite/complexity/injection.v
@@ -111,3 +111,4 @@ Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 ->
 Proof.
 intros.
 Timeout 10 Time injection H.
+Abort.
diff --git a/test-suite/complexity/ring.v b/test-suite/complexity/ring.v
index 51f7c4dabc..2d585ce5c5 100644
--- a/test-suite/complexity/ring.v
+++ b/test-suite/complexity/ring.v
@@ -5,3 +5,4 @@ Require Import ZArith.
 Open Scope Z_scope.
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
 Timeout 5 Time intro; ring.
+Abort.
diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index 04fa59075b..1c119b8e42 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -50,3 +50,4 @@ Infix "+" := Zadd : Z_scope.
 
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
 Timeout 5 Time intro; ring.
+Abort.
diff --git a/test-suite/complexity/setoid_rewrite.v b/test-suite/complexity/setoid_rewrite.v
index 2e3b006ef0..10b270ccad 100644
--- a/test-suite/complexity/setoid_rewrite.v
+++ b/test-suite/complexity/setoid_rewrite.v
@@ -8,3 +8,4 @@ Variable f : nat -> Prop.
 Goal forall U:Prop, f 100 <-> U.
 intros U.
 Timeout 5 Time setoid_replace U with False.
+Abort.
diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v
index d2ea527516..0c9915c84e 100644
--- a/test-suite/complexity/unification.v
+++ b/test-suite/complexity/unification.v
@@ -49,3 +49,4 @@ Goal
    ))))
 .
 Timeout 2 Time try refine (refl_equal _).
+Abort.
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
diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v
index 7658ce718e..440fe46003 100644
--- a/test-suite/output/FunExt.v
+++ b/test-suite/output/FunExt.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-async-proofs" "no") -*- *)
 Require Import FunctionalExtensionality.
 
 (* Basic example *)
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 72d5a9253a..7a64b7eb45 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -50,4 +50,4 @@ myAnd1 True True
 r 2 3
      : Prop
 Notation Cn := Foo.FooCn
-Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn
+Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
index cd667bbd00..a53b52396f 100644
--- a/test-suite/output/RecognizePluginWarning.v
+++ b/test-suite/output/RecognizePluginWarning.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-w" "extraction-logical-axiom") -*- *)
 
 (* Test that mentioning a warning defined in plugins works. The failure
 mode here is that these result in a warning about unknown warnings, since the
diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v
index 60faac8dd9..c875051bdc 100644
--- a/test-suite/output/Show.v
+++ b/test-suite/output/Show.v
@@ -5,7 +5,7 @@
 Theorem nums : forall (n m : nat), n = m -> (S n) = (S m).
 Proof.
   intros.
-  induction n as [| n'].  
+  induction n as [| n'].
   induction m as [| m'].
   Show.
 Admitted.
diff --git a/test-suite/output/UnclosedBlocks.v b/test-suite/output/UnclosedBlocks.v
index 854bd6a6d5..b9ba579246 100644
--- a/test-suite/output/UnclosedBlocks.v
+++ b/test-suite/output/UnclosedBlocks.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; coq-prog-args: ("-compile" "UnclosedBlocks.v") *)
 Module Foo.
   Module Closed.
   End Closed.
diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v
index c6e0054641..618b8fd42f 100644
--- a/test-suite/output/UsePluginWarning.v
+++ b/test-suite/output/UsePluginWarning.v
@@ -1,5 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *)
-
+(* -*- mode: coq; coq-prog-args: ("-w" "-extraction-logical-axiom") -*- *)
 Require Extraction.
 Axiom foo : Prop.
 
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index 5f1926f142..5f7e3ab9dd 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -11,3 +11,4 @@ Undo.
 simpl (0 + _).
 Show.
 Undo.
+Abort.
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index 179dec3fb0..c987d66c5f 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-async-proofs" "no") -*- *)
 (* Set Printing Existential Instances. *)
 Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
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
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