Merge remote-tracking branch 'origin/master' into stm+doc_hook

10 files changed, 92 insertions, 110 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 8934385091..2f63410761 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -73,14 +73,18 @@ let ensure_bname src tgt =
 
 let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
 
-let ensure_v v = ensure ".v" v v
-let ensure_vo v vo = ensure ".vo" v vo
-let ensure_vio v vio = ensure ".vio" v vio
-
 let ensure_exists f =
   if not (Sys.file_exists f) then
     fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
+let ensure_exists_with_prefix f_in f_out src_suffix tgt_suffix =
+  let long_f_dot_src = ensure src_suffix f_in f_in in
+  ensure_exists long_f_dot_src;
+  let long_f_dot_tgt = match f_out with
+    | None -> chop_extension long_f_dot_src ^ tgt_suffix
+    | Some f -> ensure tgt_suffix long_f_dot_src f in
+  long_f_dot_src, long_f_dot_tgt
+
 (* Compile a vernac file *)
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
@@ -102,12 +106,9 @@ let compile opts copts ~echo ~f_in ~f_out =
   match copts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
-      let long_f_dot_v = ensure_v f_in in
-      ensure_exists long_f_dot_v;
-      let long_f_dot_vo =
-        match f_out with
-        | None -> long_f_dot_v ^ "o"
-        | Some f -> ensure_vo long_f_dot_v f in
+
+      let long_f_dot_v, long_f_dot_vo =
+        ensure_exists_with_prefix f_in f_out ".v" ".vo" in
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
@@ -138,13 +139,8 @@ let compile opts copts ~echo ~f_in ~f_out =
       Flags.record_aux_file := false;
       Dumpglob.noglob ();
 
-      let long_f_dot_v = ensure_v f_in in
-      ensure_exists long_f_dot_v;
-
-      let long_f_dot_vio =
-        match f_out with
-        | None -> long_f_dot_v ^ "io"
-        | Some f -> ensure_vio long_f_dot_v f in
+      let long_f_dot_v, long_f_dot_vio =
+        ensure_exists_with_prefix f_in f_out ".v" ".vio" in
 
       (* We need to disable error resiliency, otherwise some errors
          will be ignored in batch mode. c.f. #6707
@@ -175,13 +171,15 @@ let compile opts copts ~echo ~f_in ~f_out =
       Stm.reset_task_queue ()
 
   | Vio2Vo ->
-      let open Filename in
+
       Flags.record_aux_file := false;
       Dumpglob.noglob ();
-      let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in
-      let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in
-      let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
-      Library.save_library_raw lfdv sum lib univs proofs
+      let long_f_dot_vio, long_f_dot_vo =
+        ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
+      let sum, lib, univs, disch, tasks, proofs =
+        Library.load_library_todo long_f_dot_vio in
+      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs disch proofs tasks in
+      Library.save_library_raw long_f_dot_vo sum lib univs proofs
 
 let compile opts copts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
@@ -205,16 +203,22 @@ let compile_files opts copts =
 (******************************************************************************)
 let check_vio_tasks copts =
   let rc =
-    List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+    List.fold_left (fun acc (n,f) ->
+        let f_in = ensure ".vio" f f in
+        ensure_exists f_in;
+        Vio_checking.check_vio (n,f_in) && acc)
       true (List.rev copts.vio_tasks) in
   if not rc then fatal_error Pp.(str "VIO Task Check failed")
 
 (* vio files *)
 let schedule_vio copts =
+  let l =
+    List.map (fun f -> let f_in = ensure ".vio" f f in ensure_exists f_in; f_in)
+      copts.vio_files in
   if copts.vio_checking then
-    Vio_checking.schedule_vio_checking copts.vio_files_j copts.vio_files
+    Vio_checking.schedule_vio_checking copts.vio_files_j l
   else
-    Vio_checking.schedule_vio_compilation copts.vio_files_j copts.vio_files
+    Vio_checking.schedule_vio_compilation copts.vio_files_j l
 
 let do_vio opts copts =
   (* We must initialize the loadpath here as the vio scheduling
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 319f5c8ad6..ec43dbb1d7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -34,7 +34,7 @@ let set_type_in_type () =
 
 (******************************************************************************)
 
-type color = [`ON | `AUTO | `OFF]
+type color = [`ON | `AUTO | `EMACS | `OFF]
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
@@ -171,7 +171,7 @@ let add_load_vernacular opts verb s =
 (** Options for proof general *)
 let set_emacs opts =
   Printer.enable_goal_tags_printing := true;
-  { opts with color = `OFF; print_emacs = true }
+  { opts with color = `EMACS; print_emacs = true }
 
 let set_color opts = function
 | "yes" | "on" -> { opts with color = `ON }
@@ -184,10 +184,6 @@ let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
 
-let warn_deprecated_boot =
-  CWarnings.create ~name:"deprecated-boot" ~category:"noop"
-         (fun () -> Pp.strbrk "The -boot option is deprecated, please use -q and/or -coqlib options instead.")
-
 let set_inputstate opts s =
   warn_deprecated_inputstate ();
   { opts with inputstate = Some s }
@@ -488,9 +484,6 @@ let parse_args ~help ~init arglist : t * string list =
       { oval with batch = true }
     |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
-    |"-boot" ->
-      warn_deprecated_boot ();
-      { oval with load_rcfile = false; }
     |"-bt" -> Backtrace.record_backtrace true; oval
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 9bcfdca332..d7f9819bee 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type color = [`ON | `AUTO | `OFF]
+type color = [`ON | `AUTO | `EMACS | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 7445619d26..2279ce5505 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -56,6 +56,13 @@ let error_missing_arg s =
   prerr_endline "See -help for the syntax of supported options";
   exit 1
 
+let check_compilation_output_name_consistency args =
+  match args.compilation_output_name, args.compile_list with
+  | Some _, _::_::_ ->
+    prerr_endline ("Error: option -o is not valid when more than one");
+    prerr_endline ("file have to be compiled")
+  | _ -> ()
+
 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
@@ -82,7 +89,22 @@ let set_vio_checking_j opts opt j =
     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 set_compilation_mode opts mode =
+  match opts.compilation_mode with
+  | BuildVo -> { opts with compilation_mode = mode }
+  | mode' when mode <> mode' ->
+    prerr_endline "Options -quick and -vio2vo are exclusive";
+    exit 1
+  | _ -> opts
+
+let get_task_list s =
+  List.map (fun s ->
+      try int_of_string s
+      with Failure _ ->
+        prerr_endline "Option -check-vio-tasks expects a comma-separated list";
+        prerr_endline "of integers followed by a list of files";
+        exit 1)
+    (Str.split (Str.regexp ",") s)
 
 let is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
@@ -138,7 +160,7 @@ let parse arglist : t =
         | "-o" ->
           { oval with compilation_output_name = Some (next ()) }
         | "-quick" ->
-          { oval with compilation_mode = BuildVio }
+          set_compilation_mode oval BuildVio
         | "-check-vio-tasks" ->
           let tno = get_task_list (next ()) in
           let tfile = next () in
@@ -157,7 +179,7 @@ let parse arglist : t =
 
         | "-vio2vo" ->
           let oval = add_compile ~echo:false oval (next ()) in
-          { oval with compilation_mode = Vio2Vo }
+          set_compilation_mode oval Vio2Vo
 
         | "-outputstate" ->
           set_outputstate oval (next ())
@@ -170,5 +192,7 @@ let parse arglist : t =
   in
   try
     let opts, extra = parse default in
-    List.fold_left add_compile opts extra
+    let args = List.fold_left add_compile opts extra in
+    check_compilation_output_name_consistency args;
+    args
   with any -> fatal_error any
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 087cd67f3a..de447db51f 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -279,7 +279,7 @@ let extract_default_loc loc doc_id sid : Loc.t option =
   | None ->
     try
       let doc = Stm.get_doc doc_id in
-      Option.cata fst None Stm.(get_ast ~doc sid)
+      Option.cata (fun {CAst.loc} -> loc) None Stm.(get_ast ~doc sid)
     with _ -> loc
 
 (** Coqloop Console feedback handler *)
@@ -383,22 +383,22 @@ let rec vernac_loop ~state =
   try
     let input = top_buffer.tokens in
     match read_sentence ~state input with
-    | Some { v = VernacBacktrack(bid,_,_) } ->
+    | Some (VernacBacktrack(bid,_,_)) ->
       let bid = Stateid.of_int bid in
       let doc, res = Stm.edit_at ~doc:state.doc bid in
       assert (res = `NewTip);
       let state = { state with doc; sid = bid } in
       vernac_loop ~state
 
-    | Some { v = VernacQuit } ->
+    | Some VernacQuit ->
       exit 0
 
-    | Some { v = VernacDrop } ->
+    | Some VernacDrop ->
       if Mltop.is_ocaml_top()
       then (drop_last_doc := Some state; state)
       else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
 
-    | Some { v = VernacControl c; loc } ->
+    | Some VernacControl { loc; v=c } ->
       let nstate = Vernac.process_expr ~state (make ?loc c) in
       top_goal_print ~doc:state.doc c state.proof nstate.proof;
       vernac_loop ~state:nstate
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8fae561be8..b769405cf6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -113,6 +113,7 @@ let fatal_error_exn exn =
 let init_color opts =
   let has_color = match opts.color with
   | `OFF -> false
+  | `EMACS -> false
   | `ON -> true
   | `AUTO ->
     Terminal.has_style Unix.stdout &&
@@ -133,10 +134,13 @@ let init_color opts =
       Topfmt.default_styles (); false                 (* textual markers, no color *)
     end
   in
-  if not term_color then
-    Proof_diffs.write_color_enabled term_color;
-  if Proof_diffs.show_diffs () && not term_color then
-    (prerr_endline "Error: -diffs requires enabling -color"; exit 1);
+  if opts.color = `EMACS then
+    Topfmt.set_emacs_print_strings ()
+  else if not term_color then begin
+      Proof_diffs.write_color_enabled term_color;
+    if Proof_diffs.show_diffs () then
+      (prerr_endline "Error: -diffs requires enabling -color"; exit 1)
+  end;
   Topfmt.init_terminal_output ~color:term_color
 
 let print_style_tags opts =
@@ -220,7 +224,6 @@ let init_toplevel ~help ~init custom_init arglist =
   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;
@@ -268,34 +271,10 @@ let init_toploop opts =
   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);
+  Flags.if_verbose print_header ();
   opts, extra
 
 let coqtop_toplevel =
@@ -313,7 +292,6 @@ let start_coq custom =
         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";
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index f2025858d7..0cac024300 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,7 +21,7 @@ type vernac_toplevel =
   | VernacControl of vernac_control
 
 module Toplevel_ : sig
-  val vernac_toplevel : vernac_toplevel CAst.t option Entry.t
+  val vernac_toplevel : vernac_toplevel option Entry.t
 end = struct
   let gec_vernac s = Entry.create ("toplevel:" ^ s)
   let vernac_toplevel = gec_vernac "vernac_toplevel"
@@ -34,14 +34,14 @@ open Toplevel_
 GRAMMAR EXTEND Gram
   GLOBAL: vernac_toplevel;
   vernac_toplevel: FIRST
-    [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) }
-      | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) }
+    [ [ IDENT "Drop"; "." -> { Some VernacDrop }
+      | IDENT "Quit"; "." -> { Some VernacQuit }
       | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
-        { Some (CAst.make (VernacBacktrack (n,m,p))) }
+        { Some (VernacBacktrack (n,m,p)) }
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None
-              | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) }
+              | Some v -> Some (VernacControl v) }
       ]
     ]
   ;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 7074215afe..29948d50b2 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -42,12 +42,12 @@ let print_usage_common co command =
 \n\
 \n  -load-ml-object f      load ML object file f\
 \n  -load-ml-source f      load ML file f\
-\n  -load-vernac-source f  load Coq file f.v (Load f.)\
+\n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
 \n  -l f                   (idem)\
-\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)\
-\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  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
+\n  -lv f	           (idem)\
+\n  -load-vernac-object path  load Coq library path (Require path)\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config, --config      print Coq's configuration information and exit\
@@ -74,9 +74,9 @@ let print_usage_common co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
-\n  -set \"Foo Bar\"       enable Foo Bar (as Set Foo Bar. in a file)\
-\n  -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\
-\n  -unset \"Foo Bar\"     disable Foo Bar (as Unset Foo Bar. in a file)\
+\n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
+\n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
+\n  -unset \"Foo Bar\"       disable Foo Bar (as Unset Foo Bar. in a file)\
 \n  -time                  display the time taken by each command\
 \n  -profile-ltac          display the time taken by each (sub)tactic\
 \n  -m, --memory           display total heap size at program exit\
@@ -102,18 +102,12 @@ let print_usage_coqtop () =
 coqtop specific options:\
 \n\
 \n  -batch                 batch mode (exits just after argument 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_common stderr "Usage: coqc <options> <Coq options> file...";
+  print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n";
   output_string stderr "\n\
 coqc specific options:\
 \n\
@@ -128,14 +122,6 @@ coqc specific options:\
 \nUndocumented:\
 \n  -vio2vo                [see manual]\
 \n  -check-vio-tasks       [see manual]\
-\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  -outputstate file      save summary state in file \
 \n";
   flush stderr ;
   exit 1
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6c6379ec5e..c41f16c95b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -20,12 +20,12 @@ open Vernacprop
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-let checknav_simple {CAst.loc;v=cmd} =
+let checknav_simple ({ CAst.loc; _ } as cmd) =
   if is_navigation_vernac cmd && not (is_reset cmd) then
     CErrors.user_err ?loc (str "Navigation commands forbidden in files.")
 
-let checknav_deep {CAst.loc;v=ast} =
-  if is_deep_navigation_vernac ast then
+let checknav_deep ({ CAst.loc; _ } as cmd) =
+  if is_deep_navigation_vernac cmd then
     CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
 
 (* Echo from a buffer based on position.
@@ -163,10 +163,7 @@ let beautify_pass ~doc ~comments ~ids ~filename =
      set the comments, then we call print. This has to be done for
      each file. *)
   Pputils.beautify_comments := comments;
-  List.iter (fun id ->
-      Option.iter (fun (loc,ast) ->
-          pr_new_syntax ?loc ft_beautify (Some ast))
-        (Stm.get_ast ~doc id)) ids;
+  List.iter (fun id -> pr_new_syntax ft_beautify (Stm.get_ast ~doc id)) ids;
 
   (* Is this called so comments at EOF are printed? *)
   pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) ft_beautify None;
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 1269540235..197891707c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -24,7 +24,7 @@ end
     expected to handle and print errors in form of exceptions, however
     care is taken so the state machine is left in a consistent
     state. *)
-val process_expr : state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t
+val process_expr : state:State.t -> Vernacexpr.vernac_control -> State.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle