Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.

Reviewed-by: maximedenes
Ack-by: ppedrot

28 files changed, 539 insertions, 536 deletions

diff --git a/Makefile.build b/Makefile.build
index 4f42768227..5775569712 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) -w -deprecate-compile-arg -compile
+BOOTCOQC=$(TIMER) $(COQC) -boot $(COQOPTS)
 
 LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
 MLINCLUDES=$(LOCALINCLUDES)
@@ -281,7 +281,7 @@ ifndef ORDER_ONLY_SEP
 $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.))
 endif
 
-VO_TOOLS_DEP := $(COQTOPBEST)
+VO_TOOLS_DEP := $(COQC)
 ifdef VALIDATE
  VO_TOOLS_DEP += $(CHICKEN)
 endif
@@ -351,6 +351,9 @@ coqbyte: $(TOPBYTE) $(CHICKENBYTE)
 $(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
 	rm -f $@ && cp $< $@
 
+$(COQC): $(COQCOPT:.opt=.$(BEST))
+	rm -f $@ && cp $< $@
+
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
@@ -377,17 +380,6 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
 			 $(SYSMOD) -package compiler-libs.toplevel \
 			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
 
-# For coqc
-COQCCMO:=config/config.cma clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
-
-$(COQC): $(call bestobj, $(COQCCMO))
-	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, $(SYSMOD))
-
-$(COQCBYTE): $(COQCCMO)
-	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(call ocamlbyte, $(SYSMOD))
-
 ###########################################################################
 # other tools
 ###########################################################################
@@ -784,8 +776,7 @@ $(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $(
 coqlib: theories plugins
 ifdef QUICK
 	$(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio'
-	$(HIDE)$(BOOTCOQC:-compile=-schedule-vio2vo) $(NJOBS) \
-		$(THEORIESVO) $(PLUGINSVO)
+	$(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(PLUGINSVO)
 endif
 
 coqlib.timing.diff: theories.timing.diff plugins.timing.diff
diff --git a/Makefile.common b/Makefile.common
index 2dced04967..f998ea867b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -32,6 +32,7 @@ COQWCBYTE:=bin/coqwc.byte$(EXE)
 COQDOC:=bin/coqdoc$(EXE)
 COQDOCBYTE:=bin/coqdoc.byte$(EXE)
 COQC:=bin/coqc$(EXE)
+COQCOPT:=bin/coqc.opt$(EXE)
 COQCBYTE:=bin/coqc.byte$(EXE)
 COQWORKMGR:=bin/coqworkmgr$(EXE)
 COQWORKMGRBYTE:=bin/coqworkmgr.byte$(EXE)
diff --git a/configure.ml b/configure.ml
index 6f5ade3b9a..ef38651a4d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -19,7 +19,7 @@ let vo_magic = 8991
 let state_magic = 58991
 let distributed_exec =
   ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
-   "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
+   "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
 
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 205f4455a3..e157696294 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -546,5 +546,5 @@ let islave_init ~opts extra_args =
 
 let () =
   let open Coqtop in
-  let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in
+  let custom = { init = islave_init; run = loop; opts = Coqargs.default } in
   start_coq custom
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 2f8129bbfd..be8ef24a09 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -118,18 +118,38 @@ module Make(T : Task) () = struct
   let spawn id =
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
+      (* Filter arguments for slaves. *)
       let rec set_slave_opt = function
         | [] -> !async_proofs_flags_for_workers @
                 ["-worker-id"; name;
                  "-async-proofs-worker-priority";
-                   CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
-        | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-vio2vo"
+                 CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+        (* Options to discard: 0 arguments *)
+        | ("-emacs"|"-emacs-U"|"-batch")::tl ->
+          set_slave_opt tl
+        (* Options to discard: 1 argument *)
+        | ("-async-proofs" |"-vio2vo" | "-o"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
+          |"-async-proofs-cache"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
           set_slave_opt tl
-        | x::tl -> x :: set_slave_opt tl in
+        (* We need to pass some options with one argument *)
+        | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
+          | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file"
+          | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names"
+          | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
+          x :: a :: set_slave_opt tl
+        (* We need to pass some options with two arguments *)
+        | ( "-R" | "-Q" as x) :: a1 :: a2 :: tl ->
+          x :: a1 :: a2 :: set_slave_opt tl
+        (* Finally we pass all options starting in '-'; check this is safe w.r.t the weird vio* option set *)
+        | x :: tl when x.[0] = '-' ->
+          x :: set_slave_opt tl
+        (* We assume this is a file, filter out *)
+        | _ :: tl ->
+          set_slave_opt tl
+      in
       let args =
         Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
       let env = Array.append (T.extra_env ()) (Unix.environment ()) in
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c55e15858a..cafc9a744c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -42,7 +42,7 @@ coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestS
 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
+coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite
 coqtopbyte := $(BIN)coqtop.byte
 
 coqc_interactive := $(coqc) -async-proofs-cache force
diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh
index a327f4248b..afc415b2da 100755
--- a/test-suite/misc/exitstatus.sh
+++ b/test-suite/misc/exitstatus.sh
@@ -1,8 +1,5 @@
 #!/bin/sh
-$coqtop -load-vernac-source misc/exitstatus/illtyped.v
-N=$?
 $coqc misc/exitstatus/illtyped.v
 P=$?
-printf "On ill-typed input, coqtop returned %s.\n" "$N"
 printf "On ill-typed input, coqc returned %s.\n" "$P"
-if [ $N = 1 ] && [ $P = 1 ]; then exit 0; else exit 1; fi
+if [ $P = 1 ]; then exit 0; else exit 1; fi
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 8f6c4c0968..6681b79e38 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 -w -deprecate-compile-arg -compile %s))" libflag eflag cflag source in
+  let action = sprintf "(chdir %%{project_root} (run coqc -boot %s %s %s %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
deleted file mode 100644
index 0f65823740..0000000000
--- a/tools/coqc.ml
+++ /dev/null
@@ -1,182 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Coq compiler : coqc *)
-
-(** For improving portability, coqc is now an OCaml program instead
-    of a shell script. We use as much as possible the Sys and Filename
-    module for better portability, but the Unix module is still used
-    here and there (with explicitly qualified function names Unix.foo).
-
-    We process here the commmand line to extract names of files to compile,
-    then we compile them one by one while passing by the rest of the command
-    line to a process running "coqtop -batch -compile <file>".
-*)
-
-(* Environment *)
-
-let environment = Unix.environment ()
-
-let use_bytecode = ref false
-let image = ref ""
-
-let verbose = ref false
-
-let rec make_compilation_args = function
-  | [] -> []
-  | file :: 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] *)
-
-let compile command args files =
-  let args' = command :: args @ (make_compilation_args files) in
-  match Sys.os_type with
-  | "Win32" ->
-     let pid =
-        Unix.create_process_env command (Array.of_list args') environment
-        Unix.stdin Unix.stdout Unix.stderr
-     in
-     let status = snd (Unix.waitpid [] pid) in
-     let errcode =
-       match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c
-     in
-     exit errcode
-  | _ ->
-     Unix.execvpe command (Array.of_list args') environment
-
-let usage () =
-  Usage.print_usage_coqc () ;
-  flush stderr ;
-  exit 1
-
-(* 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 ->
-      deprecated_coqc_warning "-image";
-      image := f; parse (cfiles,args) rem
-    | "-image" :: [] ->	usage ()
-    | "-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 *)
-
-    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-
-    | ("-v"|"--version") :: _ -> Usage.version 0
-
-    | ("-where") :: _ ->
-        Envars.set_coqlib ~fail:(fun x -> x);
-        print_endline (Envars.coqlib ());
-        exit 0
-
-    | ("-config" | "--config") :: _ ->
-        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
-
-(* Options for coqtop : a) options with 0 argument *)
-
-    | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
-      |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
-      |"-q"|"-profile"|"-echo" |"-quiet"
-      |"-silent"|"-m"|"-beautify"|"-strict-implicit"
-      |"-impredicative-set"|"-vm"|"-test-mode"|"-emacs"
-      |"-indices-matter"|"-quick"|"-type-in-type"
-      |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
-      |"-stm-debug"
-      as o) :: rem ->
-	parse (cfiles,o::args) rem
-
-(* Options for coqtop : b) options with 1 argument *)
-
-    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
-      |"-load-vernac-source"|"-l"|"-load-vernac-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"
-      |"-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"|"-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
-        extra_arg_needed := false;
-        parse (cfiles, List.rev nodash @ s :: o :: args) rem
-
-    | f :: rem ->
-	if Sys.file_exists f then
-	  parse (f::cfiles,args) rem
-	else
-	  let fv = f ^ ".v" in
-	  if Sys.file_exists fv then
-	    parse (fv::cfiles,args) rem
-	  else begin
-	    prerr_endline ("coqc: "^f^": no such file or directory") ;
-	    exit 1
-	  end
-  in
-  parse ([],[]) (List.tl (Array.to_list Sys.argv))
-
-(* main: we parse the command line, define the command to compile files
- * and then call the compilation on each file *)
-
-let main () =
-  let cfiles, args = parse_args () in
-    if cfiles = [] && !extra_arg_needed then begin
-      prerr_endline "coqc: too few arguments" ;
-      usage ()
-    end;
-    let coqtopname =
-      if !image <> "" then !image
-      else System.get_toplevel_path ~byte:!use_bytecode "coqtop"
-    in
-      (*  List.iter (compile coqtopname args) cfiles*)
-      Unix.handle_unix_error (compile coqtopname args) cfiles
-
-let _ = Printexc.print main ()
diff --git a/tools/dune b/tools/dune
index 31b70fb06c..204bd09535 100644
--- a/tools/dune
+++ b/tools/dune
@@ -16,13 +16,6 @@
  (libraries coq.lib))
 
 (executable
- (name coqc)
- (public_name coqc)
- (package coq)
- (modules coqc)
- (libraries coq.toplevel))
-
-(executable
  (name coqworkmgr)
  (public_name coqworkmgr)
  (package coq)
diff --git a/topbin/coqc_bin.ml b/topbin/coqc_bin.ml
new file mode 100644
index 0000000000..d711c81124
--- /dev/null
+++ b/topbin/coqc_bin.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Main coqc initialization *)
+let _ =
+  Coqc.main ()
diff --git a/topbin/dune b/topbin/dune
index 52f472d149..f42e4d6fc2 100644
--- a/topbin/dune
+++ b/topbin/dune
@@ -20,11 +20,19 @@
  (modes byte)
  (link_flags -linkall))
 
+(executable
+ (name coqc_bin)
+ (public_name coqc)
+ (package coq)
+ (modules coqc_bin)
+ (libraries coq.toplevel)
+ (link_flags -linkall))
+
 ; Workers
 (executables
  (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin)
  (public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt)
  (package coq)
- (modules :standard \ coqtop_byte_bin coqtop_bin)
+ (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin)
  (libraries coq.toplevel)
  (link_flags -linkall))
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index b248b87880..df2b983029 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Coqargs
+open Coqcargs
 
 let fatal_error msg =
   Topfmt.std_logger Feedback.Error msg;
@@ -81,7 +82,7 @@ let ensure_exists f =
     fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
-let compile opts ~echo ~f_in ~f_out =
+let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
@@ -95,7 +96,7 @@ let compile opts ~echo ~f_in ~f_out =
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.stm_flags in
-  match opts.compilation_mode with
+  match copts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
       let long_f_dot_v = ensure_v f_in in
@@ -179,47 +180,47 @@ let compile opts ~echo ~f_in ~f_out =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile opts ~echo ~f_in ~f_out =
+let compile opts copts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile opts ~echo ~f_in ~f_out;
+  compile opts copts ~echo ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file opts (f_in, echo) =
-  let f_out = opts.compilation_output_name in
+let compile_file opts copts (f_in, echo) =
+  let f_out = copts.compilation_output_name in
   if !Flags.beautify then
     Flags.with_option Flags.beautify_file
-      (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in
+      (fun f_in -> compile opts copts ~echo ~f_in ~f_out) f_in
   else
-    compile opts ~echo ~f_in ~f_out
+    compile opts copts ~echo ~f_in ~f_out
 
-let compile_files opts =
-  let compile_list = List.rev opts.compile_list in
-  List.iter (compile_file opts) compile_list
+let compile_files opts copts =
+  let compile_list = List.rev copts.compile_list in
+  List.iter (compile_file opts copts) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
 (******************************************************************************)
-let check_vio_tasks opts =
+let check_vio_tasks copts =
   let rc =
     List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
-      true (List.rev opts.vio_tasks) in
+      true (List.rev copts.vio_tasks) in
   if not rc then fatal_error Pp.(str "VIO Task Check failed")
 
 (* vio files *)
-let schedule_vio opts =
-  if opts.vio_checking then
-    Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files
+let schedule_vio copts =
+  if copts.vio_checking then
+    Vio_checking.schedule_vio_checking copts.vio_files_j copts.vio_files
   else
-    Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files
+    Vio_checking.schedule_vio_compilation copts.vio_files_j copts.vio_files
 
-let do_vio opts =
+let do_vio opts copts =
   (* We must initialize the loadpath here as the vio scheduling
      process happens outside of the STM *)
-  if opts.vio_files <> [] || opts.vio_tasks <> [] then
+  if copts.vio_files <> [] || copts.vio_tasks <> [] then
     let iload_path = build_load_path opts in
     List.iter Mltop.add_coq_path iload_path;
 
   (* Vio compile pass *)
-  if opts.vio_files <> [] then schedule_vio opts;
+  if copts.vio_files <> [] then schedule_vio copts;
   (* Vio task pass *)
-  if opts.vio_tasks <> [] then check_vio_tasks opts
+  if copts.vio_tasks <> [] then check_vio_tasks copts
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 757c91c408..29a76eb966 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -10,10 +10,10 @@
 
 (** [load_init_vernaculars opts ~state] Load vernaculars from
    the init (rc) file *)
-val load_init_vernaculars : Coqargs.coq_cmdopts -> state:Vernac.State.t-> Vernac.State.t
+val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t
 
 (** [compile_files opts] compile files specified in [opts] *)
-val compile_files : Coqargs.coq_cmdopts -> unit
+val compile_files : Coqargs.t -> Coqcargs.t -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
-val do_vio : Coqargs.coq_cmdopts -> unit
+val do_vio : Coqargs.t -> Coqcargs.t -> unit
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index f822c68843..74c016101a 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -31,10 +31,9 @@ let set_type_in_type () =
 
 (******************************************************************************)
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
 type color = [`ON | `AUTO | `OFF]
 
-type coq_cmdopts = {
+type t = {
 
   load_init   : bool;
   load_rcfile : bool;
@@ -45,21 +44,10 @@ type coq_cmdopts = {
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
-  (* XXX: Fusion? *)
-  batch_mode : bool;
-  compilation_mode : compilation_mode;
-
   toplevel_name : Stm.interactive_top;
 
-  compile_list: (string * bool) list;  (* bool is verbosity  *)
-  compilation_output_name : string option;
-
   load_vernacular_list : (string * bool) list;
-
-  vio_checking: bool;
-  vio_tasks   : (int list * string) list;
-  vio_files   : string list;
-  vio_files_j : int;
+  batch : bool;
 
   color : color;
 
@@ -67,6 +55,7 @@ type coq_cmdopts = {
   indices_matter : bool;
   enable_VM : bool;
   enable_native_compiler : bool;
+
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
@@ -85,13 +74,12 @@ type coq_cmdopts = {
   print_emacs : bool;
 
   inputstate  : string option;
-  outputstate : string option;
 
 }
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
-let default_opts = {
+let default = {
 
   load_init   = true;
   load_rcfile = true;
@@ -101,20 +89,10 @@ let default_opts = {
   vo_includes = [];
   vo_requires = [];
 
-  batch_mode = false;
-  compilation_mode = BuildVo;
-
   toplevel_name = Stm.TopLogical default_toplevel;
 
-  compile_list = [];
-  compilation_output_name = None;
-
   load_vernacular_list = [];
-
-  vio_checking = false;
-  vio_tasks    = [];
-  vio_files    = [];
-  vio_files_j  = 0;
+  batch = false;
 
   color = `AUTO;
 
@@ -142,7 +120,6 @@ let default_opts = {
   (* Quiet / verbosity options should be here *)
 
   inputstate  = None;
-  outputstate = None;
 }
 
 (******************************************************************************)
@@ -168,44 +145,9 @@ let add_compat_require opts v =
   | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
   | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
 
-let set_batch_mode opts =
-  (* XXX: This should be in the argument record *)
-  Flags.quiet := true;
-  System.trust_file_cache := true;
-  { opts with batch_mode = true }
-
-let add_compile opts verbose s =
-  let opts = set_batch_mode opts in
-  if not opts.glob_opt then Dumpglob.dump_to_dotglob ();
-  (* make the file name explicit; needed not to break up Coq loadpath stuff. *)
-  let s =
-    let open Filename in
-    if is_implicit s
-    then concat current_dir_name s
-    else s
-  in
-  { opts with compile_list = (s,verbose) :: opts.compile_list }
-
 let add_load_vernacular opts verb s =
   { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list }
 
-let add_vio_task opts f =
-  let opts = set_batch_mode opts in
-  { opts with vio_tasks = f :: opts.vio_tasks }
-
-let add_vio_file opts f =
-  let opts = set_batch_mode opts in
-  { opts with vio_files = f :: opts.vio_files }
-
-let set_vio_checking_j opts opt j =
-  try { opts with vio_files_j = int_of_string j }
-  with Failure _ ->
-    prerr_endline ("The first argument of " ^ opt ^ " must the number");
-    prerr_endline "of concurrent workers to be used (a positive integer).";
-    prerr_endline "Makefiles generated by coq_makefile should be called";
-    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
-    exit 1
-
 (** Options for proof general *)
 let set_emacs opts =
   Printer.enable_goal_tags_printing := true;
@@ -225,22 +167,11 @@ let set_inputstate opts s =
   warn_deprecated_inputstate ();
   { opts with inputstate = Some s }
 
-let warn_deprecated_outputstate =
-  CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
-         (fun () ->
-          Pp.strbrk "The outputstate option is deprecated and discouraged.")
-
-let set_outputstate opts s =
-  warn_deprecated_outputstate ();
-  { opts with outputstate = Some s }
-
 let exitcode opts = if opts.filter_opts then 2 else 0
 
 (******************************************************************************)
 (* Parsing helpers                                                            *)
 (******************************************************************************)
-let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
-
 let get_bool opt = function
   | "yes" | "on" -> true
   | "no" | "off" -> false
@@ -285,16 +216,6 @@ let get_cache opt = function
   | "force" -> Some Stm.AsyncOpts.Force
   | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
 
-let is_not_dash_option = function
-  | Some f when String.length f > 0 && f.[0] <> '-' -> true
-  | _ -> false
-
-let rec add_vio_args peek next oval =
-  if is_not_dash_option (peek ()) then
-    let oval = add_vio_file oval (next ()) in
-    add_vio_args peek next oval
-  else oval
-
 let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
   try
@@ -311,7 +232,7 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy
 
 exception NoCoqLib
 
-let usage batch =
+let usage help =
   begin
     try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
     with NoCoqLib -> usage_no_coqlib ()
@@ -319,18 +240,10 @@ let usage batch =
   let lp = Coqinit.toplevel_init_load_path () in
   (* Necessary for finding the toplevels below *)
   List.iter Mltop.add_coq_path lp;
-  if 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."])))
+  help ()
 
 (* Main parsing routine *)
-let parse_args init_opts arglist : coq_cmdopts * string list =
+let parse_args ~help ~init arglist : t * string list =
   let args = ref arglist in
   let extras = ref [] in
   let rec parse oval = match !args with
@@ -342,10 +255,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
       | x::rem -> args := rem; x
       | [] -> error_missing_arg opt
     in
-    let peek_next () = match !args with
-      | x::_ -> Some x
-      | [] -> None
-    in
     let noval = begin match opt with
 
     (* Complex options with many args *)
@@ -371,23 +280,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
       | _ -> error_missing_arg opt
       end
 
-    (* Options with two arg *)
-    |"-check-vio-tasks" ->
-      let tno = get_task_list (next ()) in
-      let tfile = next () in
-      add_vio_task oval (tno,tfile)
-
-    |"-schedule-vio-checking" ->
-      let oval = { oval with vio_checking = true } in
-      let oval = set_vio_checking_j oval opt (next ()) in
-      let oval = add_vio_file oval (next ()) in
-      add_vio_args peek_next next oval
-
-    |"-schedule-vio2vo" ->
-      let oval = set_vio_checking_j oval opt (next ()) in
-      let oval = add_vio_file oval (next ()) in
-      add_vio_args peek_next next oval
-
     (* Options with one arg *)
     |"-coqlib" ->
       Envars.set_user_coqlib (next ());
@@ -442,14 +334,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
       Flags.compat_version := v;
       add_compat_require oval v
 
-    |"-compile" as opt ->
-      deprecated_coqc_warning opt;
-      add_compile oval false (next ())
-
-    |"-compile-verbose" as opt ->
-      deprecated_coqc_warning opt;
-      add_compile oval true (next ())
-
     |"-dump-glob" ->
       Dumpglob.dump_into_file (next ());
       { oval with glob_opt = true }
@@ -466,9 +350,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
     |"-inputstate"|"-is" ->
       set_inputstate oval (next ())
 
-    |"-outputstate" ->
-      set_outputstate oval (next ())
-
     |"-load-ml-object" ->
       Mltop.dir_ml_load (next ()); oval
 
@@ -514,10 +395,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
     |"-control-channel" ->
       Spawned.control_channel := get_host_port opt (next()); oval
 
-    |"-vio2vo" ->
-      let oval = add_compile oval false (next ()) in
-      { oval with compilation_mode = Vio2Vo }
-
     |"-w" | "-W" ->
       let w = next () in
       if w = "none" then
@@ -527,10 +404,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
         CWarnings.set_flags (CWarnings.normalize_flags_string w);
         oval
 
-    |"-o" as opt ->
-      deprecated_coqc_warning opt;
-      { oval with compilation_output_name = Some (next()) }
-
     |"-bytecode-compiler" ->
       { oval with enable_VM = get_bool opt (next ()) }
 
@@ -558,7 +431,9 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
       { oval with stm_flags = { oval.stm_flags with
         Stm.AsyncOpts.async_proofs_never_reopen_branch = true
       }}
-    |"-batch" -> set_batch_mode oval
+    |"-batch" ->
+      Flags.quiet := true;
+      { oval with batch = true }
     |"-test-mode" -> Flags.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
     |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; }
@@ -588,13 +463,12 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
       Flags.quiet := true;
       Flags.make_warn false;
       oval
-    |"-quick" -> { oval with compilation_mode = BuildVio }
     |"-list-tags" -> { oval with print_tags = true }
     |"-time" -> { oval with time = true }
     |"-type-in-type" -> set_type_in_type (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
     |"-where" -> { oval with print_where = true }
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage oval.batch_mode; oval
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval
     |"-v"|"--version" -> Usage.version (exitcode oval)
     |"-print-version"|"--print-version" ->
       Usage.machine_readable_version (exitcode oval)
@@ -607,13 +481,13 @@ let parse_args init_opts arglist : coq_cmdopts * string list =
     parse noval
   in
   try
-    parse init_opts
+    parse init
   with any -> fatal_error any
 
 (******************************************************************************)
 (* Startup LoadPath and Modules                                               *)
 (******************************************************************************)
-(* prelude_data == From Coq Require Export Prelude. *)
+(* prelude_data == From Coq Require Import Prelude. *)
 let prelude_data = "Prelude", Some "Coq", Some false
 
 let require_libs opts =
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index e645b0c126..c9a7a0fd56 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -8,12 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
 type color = [`ON | `AUTO | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
-type coq_cmdopts = {
+type t = {
 
   load_init   : bool;
   load_rcfile : bool;
@@ -23,22 +22,10 @@ type coq_cmdopts = {
   vo_includes : Mltop.coq_path list;
   vo_requires : (string * string option * bool option) list;
 
-  (* Fuse these two? Currently, [batch_mode] is only used to
-     distinguish coqc / coqtop in help display. *)
-  batch_mode : bool;
-  compilation_mode : compilation_mode;
-
   toplevel_name : Stm.interactive_top;
 
-  compile_list: (string * bool) list;  (* bool is verbosity  *)
-  compilation_output_name : string option;
-
   load_vernacular_list : (string * bool) list;
-
-  vio_checking: bool;
-  vio_tasks   : (int list * string) list;
-  vio_files   : string list;
-  vio_files_j : int;
+  batch : bool;
 
   color : color;
 
@@ -63,18 +50,14 @@ type coq_cmdopts = {
 
   print_emacs : bool;
 
-  (* Quiet / verbosity options should be here *)
-
   inputstate  : string option;
-  outputstate : string option;
-
 }
 
 (* Default options *)
-val default_opts : coq_cmdopts
+val default : t
 
-val parse_args : coq_cmdopts -> string list -> coq_cmdopts * string list
-val exitcode : coq_cmdopts -> int
+val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
+val exitcode : t -> int
 
-val require_libs : coq_cmdopts -> (string * string option * bool option) list
-val build_load_path : coq_cmdopts -> Mltop.coq_path list
+val require_libs : t -> (string * string option * bool option) list
+val build_load_path : t -> Mltop.coq_path list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
new file mode 100644
index 0000000000..d4107177a7
--- /dev/null
+++ b/toplevel/coqc.ml
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let set_noninteractive_mode () =
+  Flags.quiet := true;
+  System.trust_file_cache := true
+
+let outputstate opts =
+  Option.iter (fun ostate_file ->
+    let fname = CUnix.make_suffix ostate_file ".coq" in
+    States.extern_state fname) opts.Coqcargs.outputstate
+
+let coqc_main () =
+  (* Careful because init_toplevel will call Summary.init_summaries,
+     thus options such as `quiet` have to be set after the main
+     initialisation is run. *)
+  let coqc_init ~opts args =
+    set_noninteractive_mode ();
+    let opts, args = Coqtop.(coqtop_toplevel.init) ~opts args in
+    opts, args
+  in
+  let opts, extras =
+    Topfmt.(in_phase ~phase:Initialization)
+      Coqtop.(init_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in
+
+  let copts = Coqcargs.parse extras in
+
+  if not opts.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ();
+
+  Topfmt.(in_phase ~phase:CompilationPhase)
+    Ccompile.compile_files opts copts;
+
+  (* Careful this will modify the load-path and state so after this
+     point some stuff may not be safe anymore. *)
+  Topfmt.(in_phase ~phase:CompilationPhase)
+    Ccompile.do_vio opts copts;
+
+  (* Allow the user to output an arbitrary state *)
+  outputstate copts;
+
+  flush_all();
+  if opts.Coqargs.output_context then begin
+    let sigma, env = Pfedit.get_current_context () in
+    Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
+  end;
+  CProfile.print_profile ()
+
+let main () =
+  let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in
+  try
+    coqc_main ();
+    exit 0
+  with exn ->
+    flush_all();
+    Topfmt.print_err_exn exn;
+    flush_all();
+    let exit_code =
+      if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1
+    in
+    exit exit_code
diff --git a/toplevel/coqc.mli b/toplevel/coqc.mli
new file mode 100644
index 0000000000..6049c5e188
--- /dev/null
+++ b/toplevel/coqc.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val main : unit -> unit
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
new file mode 100644
index 0000000000..7445619d26
--- /dev/null
+++ b/toplevel/coqcargs.ml
@@ -0,0 +1,174 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+
+type t =
+  { compilation_mode : compilation_mode
+
+  ; compile_list: (string * bool) list  (* bool is verbosity  *)
+  ; compilation_output_name : string option
+
+  ; vio_checking : bool
+  ; vio_tasks    : (int list * string) list
+  ; vio_files    : string list
+  ; vio_files_j  : int
+
+  ; echo : bool
+
+  ; outputstate : string option;
+  }
+
+let default =
+  { compilation_mode = BuildVo
+
+  ; compile_list = []
+  ; compilation_output_name = None
+
+  ; vio_checking = false
+  ; vio_tasks    = []
+  ; vio_files    = []
+  ; vio_files_j  = 0
+
+  ; echo = false
+
+  ; outputstate = None
+  }
+
+let depr opt =
+  Feedback.msg_warning Pp.(seq[str "Option "; str opt; str " is a noop and deprecated"])
+
+(* XXX Remove this duplication with Coqargs *)
+let fatal_error exn =
+  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
+  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  exit exit_code
+
+let error_missing_arg s =
+  prerr_endline ("Error: extra argument expected after option "^s);
+  prerr_endline "See -help for the syntax of supported options";
+  exit 1
+
+let add_compile ?echo copts s =
+  (* make the file name explicit; needed not to break up Coq loadpath stuff. *)
+  let echo = Option.default copts.echo echo in
+  let s =
+    let open Filename in
+    if is_implicit s
+    then concat current_dir_name s
+    else s
+  in
+  { copts with compile_list = (s,echo) :: copts.compile_list }
+
+let add_vio_task opts f =
+  { opts with vio_tasks = f :: opts.vio_tasks }
+
+let add_vio_file opts f =
+  { opts with vio_files = f :: opts.vio_files }
+
+let set_vio_checking_j opts opt j =
+  try { opts with vio_files_j = int_of_string j }
+  with Failure _ ->
+    prerr_endline ("The first argument of " ^ opt ^ " must the number");
+    prerr_endline "of concurrent workers to be used (a positive integer).";
+    prerr_endline "Makefiles generated by coq_makefile should be called";
+    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
+    exit 1
+
+let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
+
+let is_not_dash_option = function
+  | Some f when String.length f > 0 && f.[0] <> '-' -> true
+  | _ -> false
+
+let rec add_vio_args peek next oval =
+  if is_not_dash_option (peek ()) then
+    let oval = add_vio_file oval (next ()) in
+    add_vio_args peek next oval
+  else oval
+
+let warn_deprecated_outputstate =
+  CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
+         (fun () ->
+          Pp.strbrk "The outputstate option is deprecated and discouraged.")
+
+let set_outputstate opts s =
+  warn_deprecated_outputstate ();
+  { opts with outputstate = Some s }
+
+let parse arglist : t =
+  let echo = ref false in
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse (oval : t) = match !args with
+    | [] ->
+      (oval, List.rev !extras)
+    | opt :: rem ->
+      args := rem;
+      let next () = match !args with
+        | x::rem -> args := rem; x
+        | [] -> error_missing_arg opt
+      in
+      let peek_next () = match !args with
+        | x::_ -> Some x
+        | [] -> None
+      in
+      let noval : t = begin match opt with
+        (* Deprecated options *)
+        | "-opt"
+        | "-byte" as opt ->
+          depr opt;
+          oval
+        | "-image" as opt ->
+          depr opt;
+          let _ = next () in
+          oval
+        (* Verbose == echo mode *)
+        | "-verbose" ->
+          echo := true;
+          oval
+        (* Output filename *)
+        | "-o" ->
+          { oval with compilation_output_name = Some (next ()) }
+        | "-quick" ->
+          { oval with compilation_mode = BuildVio }
+        | "-check-vio-tasks" ->
+          let tno = get_task_list (next ()) in
+          let tfile = next () in
+          add_vio_task oval (tno,tfile)
+
+        | "-schedule-vio-checking" ->
+          let oval = { oval with vio_checking = true } in
+          let oval = set_vio_checking_j oval opt (next ()) in
+          let oval = add_vio_file oval (next ()) in
+          add_vio_args peek_next next oval
+
+        | "-schedule-vio2vo" ->
+          let oval = set_vio_checking_j oval opt (next ()) in
+          let oval = add_vio_file oval (next ()) in
+          add_vio_args peek_next next oval
+
+        | "-vio2vo" ->
+          let oval = add_compile ~echo:false oval (next ()) in
+          { oval with compilation_mode = Vio2Vo }
+
+        | "-outputstate" ->
+          set_outputstate oval (next ())
+
+        | s ->
+          extras := s :: !extras;
+          oval
+      end in
+      parse noval
+  in
+  try
+    let opts, extra = parse default in
+    List.fold_left add_compile opts extra
+  with any -> fatal_error any
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
new file mode 100644
index 0000000000..7792056b24
--- /dev/null
+++ b/toplevel/coqcargs.mli
@@ -0,0 +1,30 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+
+type t =
+  { compilation_mode : compilation_mode
+
+  ; compile_list: (string * bool) list  (* bool is verbosity  *)
+  ; compilation_output_name : string option
+
+  ; vio_checking : bool
+  ; vio_tasks    : (int list * string) list
+  ; vio_files    : string list
+  ; vio_files_j  : int
+
+  ; echo : bool
+
+  ; outputstate : string option
+  }
+
+val default : t
+val parse : string list -> t
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 7d03484412..0cc22ba31d 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit
 
 (** Last document seen after `Drop` *)
 val drop_last_doc : Vernac.State.t option ref
-val drop_args : Coqargs.coq_cmdopts option ref
+val drop_args : Coqargs.t option ref
 
 (** Main entry point of Coq: read and execute vernac commands. *)
-val loop : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit
+val loop : opts:Coqargs.t -> state:Vernac.State.t -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 56622abc92..6ef0aa390d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -58,11 +58,6 @@ let inputstate opts =
     let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
     States.intern_state fname) opts.inputstate
 
-let outputstate opts =
-  Option.iter (fun ostate_file ->
-    let fname = CUnix.make_suffix ostate_file ".coq" in
-    States.extern_state fname) opts.outputstate
-
 (******************************************************************************)
 (* Fatal Errors                                                               *)
 (******************************************************************************)
@@ -102,7 +97,7 @@ let init_color opts =
     else
       false
   in
-  if Proof_diffs.show_diffs () && not term_color && not opts.batch_mode then
+  if Proof_diffs.show_diffs () && not term_color then
     (prerr_endline "Error: -diffs requires enabling -color"; exit 1);
   Topfmt.init_terminal_output ~color:term_color
 
@@ -148,116 +143,114 @@ let init_gc () =
              Gc.space_overhead = 120}
 
 (** Main init routine *)
-let init_toplevel init_opts custom_init arglist =
+let init_toplevel ~help ~init custom_init arglist =
   (* Coq's init process, phase 1:
      OCaml parameters, basic structures, and IO
    *)
   CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-  let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
 
   Lib.init();
 
   (* Coq's init process, phase 2:
      Basic Coq environment, load-path, plugins.
    *)
-  let res = begin
-    try
-      let opts,extras = parse_args init_opts arglist in
-      memory_stat := opts.memory_stat;
-
-      (* If we have been spawned by the Spawn module, this has to be done
-       * early since the master waits us to connect back *)
-      Spawned.init_channels ();
-      Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
-      if opts.print_where then begin
-        print_endline (Envars.coqlib ());
-        exit (exitcode opts)
-      end;
-      if opts.print_config then begin
-        Envars.print_config stdout Coq_config.all_src_dirs;
-        exit (exitcode opts)
-      end;
-      if opts.print_tags then begin
-        print_style_tags opts;
-        exit (exitcode opts)
-      end;
-      if opts.filter_opts then begin
-        print_string (String.concat "\n" extras);
-        exit 0;
-      end;
-      let top_lp = Coqinit.toplevel_init_load_path () in
-      List.iter Mltop.add_coq_path top_lp;
-      let opts, extras = custom_init ~opts extras in
-      if not (CList.is_empty extras) then begin
-        prerr_endline ("Don't know what to do with "^String.concat " " extras);
-        prerr_endline "See -help for the list of supported options";
-        exit 1
-      end;
-      Flags.if_verbose print_header ();
-      Mltop.init_known_plugins ();
-      Global.set_engagement opts.impredicative_set;
-      Global.set_indices_matter opts.indices_matter;
-      Global.set_VM opts.enable_VM;
-      Global.set_native_compiler opts.enable_native_compiler;
-
-      (* Allow the user to load an arbitrary state here *)
-      inputstate opts;
-
-      (* This state will be shared by all the documents *)
-      Stm.init_core ();
-
-      (* Coq init process, phase 3: Stm initialization, backtracking state.
-
-         It is essential that the module system is in a consistent
-         state before we take the first snapshot. This was not
-         guaranteed in the past, but now is thanks to the STM API.
-
-         We split the codepath here depending whether coqtop is called
-         in interactive mode or not.  *)
-
-      (* The condition for starting the interactive mode is a bit
-         convoluted, we should really refactor batch/compilation_mode
-         more. *)
-      if (not opts.batch_mode
-          || CList.(is_empty opts.compile_list && is_empty opts.vio_files && is_empty opts.vio_tasks))
-      (* Interactive *)
-      then begin
-        let iload_path = build_load_path opts in
-        let require_libs = require_libs opts in
-        let stm_options = opts.stm_flags in
-        let open Vernac.State in
-        let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
-            Stm.new_doc
-            Stm.{ doc_type = Interactive opts.toplevel_name;
-                  iload_path; require_libs; stm_options;
-                } in
-        let state = { doc; sid; proof = None; time = opts.time } in
-        Some (Ccompile.load_init_vernaculars opts ~state), opts
-      (* Non interactive: we perform a sequence of compilation steps *)
-      end else begin
-        Ccompile.compile_files opts;
-        (* Careful this will modify the load-path and state so after
-           this point some stuff may not be safe anymore. *)
-        Ccompile.do_vio opts;
-        (* Allow the user to output an arbitrary state *)
-        outputstate opts;
-        None, opts
-      end;
-    with any ->
-      flush_all();
-      fatal_error_exn any
-  end in
-  Feedback.del_feeder init_feeder;
-  res
+  let opts, extras = parse_args ~help ~init arglist in
+  memory_stat := opts.memory_stat;
+
+  (* If we have been spawned by the Spawn module, this has to be done
+   * early since the master waits us to connect back *)
+  Spawned.init_channels ();
+  Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+  if opts.print_where then begin
+    print_endline (Envars.coqlib ());
+    exit (exitcode opts)
+  end;
+  if opts.print_config then begin
+    Envars.print_config stdout Coq_config.all_src_dirs;
+    exit (exitcode opts)
+  end;
+  if opts.print_tags then begin
+    print_style_tags opts;
+    exit (exitcode opts)
+  end;
+  if opts.filter_opts then begin
+    print_string (String.concat "\n" extras);
+    exit 0;
+  end;
+  let top_lp = Coqinit.toplevel_init_load_path () in
+  List.iter Mltop.add_coq_path top_lp;
+  let opts, extras = custom_init ~opts extras in
+  Flags.if_verbose print_header ();
+  Mltop.init_known_plugins ();
+
+  Global.set_engagement opts.impredicative_set;
+  Global.set_indices_matter opts.indices_matter;
+  Global.set_VM opts.enable_VM;
+  Global.set_native_compiler opts.enable_native_compiler;
+
+  (* Allow the user to load an arbitrary state here *)
+  inputstate opts;
+
+  (* This state will be shared by all the documents *)
+  Stm.init_core ();
+
+  (* Coq init process, phase 3: Stm initialization, backtracking state.
+
+     It is essential that the module system is in a consistent
+     state before we take the first snapshot. This was not
+     guaranteed in the past, but now is thanks to the STM API.
+  *)
+  opts, extras
+
+type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
 
 type custom_toplevel =
-  { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list
-  ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit
-  ; opts : Coqargs.coq_cmdopts
+  { init : init_fn
+  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
+  ; opts : Coqargs.t
   }
 
+
+let init_toploop opts =
+  let iload_path = build_load_path opts in
+  let require_libs = require_libs opts in
+  let stm_options = opts.stm_flags in
+  let open Vernac.State in
+  let doc, sid =
+    Stm.(new_doc
+           { doc_type = Interactive opts.toplevel_name;
+             iload_path; require_libs; stm_options;
+           }) in
+  let state = { doc; sid; proof = None; time = opts.time } in
+  Ccompile.load_init_vernaculars opts ~state, opts
+
+(* To remove in 8.11 *)
+let call_coqc args =
+  let remove str arr = Array.(of_list List.(filter (fun l -> not String.(equal l str)) (to_list arr))) in
+  let coqc_name = Filename.remove_extension (System.get_toplevel_path "coqc") in
+  let args = remove "-compile" args in
+  Unix.execv coqc_name args
+
+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."])))
+
+let rec coqc_deprecated_check args acc extras =
+  match extras with
+  | [] -> acc
+  | "-o" :: _ :: rem ->
+    deprecated_coqc_warning "-o";
+    coqc_deprecated_check args acc rem
+  | ("-compile"|"-compile-verbose") :: file :: rem ->
+    deprecated_coqc_warning "-compile";
+    call_coqc args
+  | x :: rem ->
+    coqc_deprecated_check args (x::acc) rem
+
 let coqtop_init ~opts extra =
   init_color opts;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
@@ -266,20 +259,28 @@ let coqtop_init ~opts extra =
 let coqtop_toplevel =
   { init = coqtop_init
   ; run = Coqloop.loop
-  ; opts = Coqargs.default_opts
+  ; opts = Coqargs.default
   }
 
 let start_coq custom =
-  match init_toplevel custom.opts custom.init (List.tl (Array.to_list Sys.argv)) with
-  (* Batch mode *)
-  | Some state, opts when not opts.batch_mode ->
-    custom.run ~opts ~state;
-    exit 1
-  | _ , opts ->
-    flush_all();
-    if opts.output_context then begin
-      let sigma, env = Pfedit.get_current_context () in
-      Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
-    end;
-    CProfile.print_profile ();
-    exit 0
+  let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
+  (* Init phase *)
+  let state, opts =
+    try
+      let opts, extras =
+        init_toplevel
+          ~help:Usage.print_usage_coqtop ~init:default custom.init
+          (List.tl (Array.to_list Sys.argv)) in
+      let extras = coqc_deprecated_check Sys.argv [] extras in
+      if not (CList.is_empty extras) then begin
+        prerr_endline ("Don't know what to do with "^String.concat " " extras);
+        prerr_endline "See -help for the list of supported options";
+        exit 1
+      end;
+      init_toploop opts
+    with any ->
+      flush_all();
+      fatal_error_exn any in
+  Feedback.del_feeder init_feeder;
+  if not opts.batch then custom.run ~opts ~state;
+  exit 0
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index c95d0aca55..300a7a039b 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -12,14 +12,24 @@
     [init] is used to do custom command line argument parsing.
     [run] launches a custom toplevel.
 *)
-open Coqargs
+
+type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
 
 type custom_toplevel =
-  { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list
-  ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit
-  ; opts : Coqargs.coq_cmdopts
+  { init : init_fn
+  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
+  ; opts : Coqargs.t
   }
 
+(** [init_toplevel ~help ~init custom_init arg_list]
+    Common Coq initialization and argument parsing *)
+val init_toplevel
+  :  help:(unit -> unit)
+  -> init:Coqargs.t
+  -> init_fn
+  -> string list
+  -> Coqargs.t * string list
+
 val coqtop_toplevel : custom_toplevel
 
 (** The Coq main module. [start custom] will parse the command line,
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 732744eb42..ddd11fd160 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -2,8 +2,10 @@ Vernac
 Usage
 Coqinit
 Coqargs
+Coqcargs
 G_toplevel
 Coqloop
 Ccompile
 Coqtop
 WorkerLoop
+Coqc
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 53bfeddf00..277f8b7367 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -48,11 +48,6 @@ let print_usage_common 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  -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\
-\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
-\n                         proofs in each fi.vio\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config, --config      print Coq's configuration information and exit\
@@ -67,7 +62,7 @@ let print_usage_common co command =
 \n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
-\n  -boot                  boot mode (implies -q and -batch)\
+\n  -boot                  boot mode (allows to overload the `Coq` library prefix)\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -diffs (on|off|removed) highlight differences between proof steps\
@@ -84,8 +79,8 @@ let print_usage_common co command =
 \n                         (use environment variable\
 \n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
 \n                          for full Gc stats dump)\
-\n  -bytecode-compiler (yes|no) controls the vm_compute machinery\
-\n  -native-compiler (yes|no|ondemand) controls the native_compute machinery\
+\n  -bytecode-compiler (yes|no)        enable the vm_compute reduction machine\
+\n  -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
 \n  -h, -help, --help      print this list of options\
 \n";
   List.iter (fun (name, text) ->
@@ -102,7 +97,7 @@ let print_usage_coqtop () =
   output_string stderr "\n\
 coqtop specific options:\
 \n\
-\n  -batch                 batch mode (exits just after arguments parsing)\
+\n  -batch                 batch mode (exits just after argument parsing)\
 \n\
 \nDeprecated options [use coqc instead]:\
 \n\
@@ -120,6 +115,15 @@ 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  -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\
+\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
+\n                         proofs in each fi.vio\
+\n\
+\nUndocumented:\
+\n  -vio2vo                [see manual]\
+\n  -check-vio-tasks       [see manual]\
 \n\
 \nDeprecated options:\
 \n\
@@ -127,6 +131,7 @@ coqc specific options:\
 \n  -opt                   run the native-code version of Coq\
 \n  -byte                  run the bytecode version of Coq\
 \n  -t                     keep temporary files\
+\n  -outputstate file      save summary state in file \
 \n";
   flush stderr ;
   exit 1
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index e4e9a87365..f922ad8fee 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -23,7 +23,7 @@ let arg_init init ~opts extra_args =
 let start ~init ~loop =
   let open Coqtop in
   let custom = {
-    opts = Coqargs.default_opts;
+    opts = Coqargs.default;
     init = arg_init init;
     run = (fun ~opts:_ ~state:_ -> loop ());
   } in
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index b4b893a3fd..ed93267665 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -335,6 +335,7 @@ type execution_phase =
   | LoadingPrelude
   | LoadingRcFile
   | InteractiveLoop
+  | CompilationPhase
 
 let default_phase = ref InteractiveLoop
 
@@ -373,7 +374,9 @@ let pr_phase ?loc () =
      Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc)
   | _, Some loc -> Some (pr_loc loc)
   | ParsingCommandLine, _
-  | Initialization, _ -> None
+  | Initialization, _
+  | CompilationPhase, _ ->
+    None
   | InteractiveLoop, _ ->
      (* Note: interactive messages such as "foo is defined" are not located *)
      None
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 5f84c5edee..b0e3b3772c 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -60,6 +60,7 @@ type execution_phase =
   | LoadingPrelude
   | LoadingRcFile
   | InteractiveLoop
+  | CompilationPhase
 
 val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b