Imported Upstream version 8.5~beta1+dfsg

1 files changed, 177 insertions, 202 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cb90909e..176a6c33 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,22 +9,38 @@
 (* Parsing of vernacular. *)
 
 open Pp
-open Lexer
+open Errors
 open Util
 open Flags
 open System
 open Vernacexpr
-open Vernacinterp
-open Ppvernac
-open Compat
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-exception DuringCommandInterp of Util.loc * exn
+(* The navigation vernac commands will be handled separately *)
 
-exception HasNotFailed
+let rec is_navigation_vernac = function
+  | VernacResetInitial
+  | VernacResetName _
+  | VernacBacktrack _
+  | VernacBackTo _
+  | VernacBack _ -> true
+  | VernacTime l ->
+    List.exists
+      (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
+  | c -> is_deep_navigation_vernac c
+
+and is_deep_navigation_vernac = function
+  | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+  | _ -> false
+
+(* NB: Reset is now allowed again as asked by A. Chlipala *)
+
+let is_reset = function
+  | VernacResetInitial | VernacResetName _ -> true
+  | _ -> false
 
 (* When doing Load on a file, two behaviors are possible:
 
@@ -50,85 +66,35 @@ let _ =
       Goptions.optread  = (fun () -> !atomic_load);
       Goptions.optwrite = ((:=) atomic_load) }
 
-(* Specifies which file is read. The intermediate file names are
-   discarded here. The Drop exception becomes an error. We forget
-   if the error ocurred during interpretation or not *)
-
-let raise_with_file file exc =
-  let (cmdloc,re) =
-    match exc with
-      | DuringCommandInterp(loc,e) -> (loc,e)
-      | e -> (dummy_loc,e)
-  in
-  let (inner,inex) =
-    match re with
-      | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
-          ((b, f, loc), e)
-      | Loc.Exc_located (loc, e) when loc <> dummy_loc ->
-          ((false,file, loc), e)
-      | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
-  in
-  raise (Error_in_file (file, inner, disable_drop inex))
-
-let real_error = function
-  | Loc.Exc_located (_, e) -> e
-  | Error_in_file (_, _, e) -> e
-  | e -> e
-
-let user_error loc s = Util.user_err_loc (loc,"_",str s)
+(* In case of error, register the file being currently Load'ed and the
+   inner file in which the error has been encountered. Any intermediate files
+   between the two are discarded. *)
 
-(** Timeout handling *)
+type location_files = { outer : string; inner : string }
 
-(** A global default timeout, controled by option "Set Default Timeout n".
-    Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
+let files_of_exn : location_files Exninfo.t = Exninfo.make ()
 
-let default_timeout = ref None
+let get_exn_files e = Exninfo.get e files_of_exn
 
-let _ =
-  Goptions.declare_int_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "the default timeout";
-      Goptions.optkey   = ["Default";"Timeout"];
-      Goptions.optread  = (fun () -> !default_timeout);
-      Goptions.optwrite = ((:=) default_timeout) }
-
-(** When interpreting a command, the current timeout is initially
-    the default one, but may be modified locally by a Timeout command. *)
-
-let current_timeout = ref None
+let add_exn_files e f = Exninfo.add e files_of_exn f
 
-(** Installing and de-installing a timer.
-    Note: according to ocaml documentation, Unix.alarm isn't available
-    for native win32. *)
+let raise_with_file f (e, info) =
+  let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in
+  iraise (e, add_exn_files info { outer = f; inner = inner_f })
 
-let timeout_handler _ = raise Timeout
-
-let set_timeout n =
-  let psh =
-    Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-  ignore (Unix.alarm n);
-  Some psh
-
-let default_set_timeout () =
-  match !current_timeout with
-    | Some n -> set_timeout n
-    | None -> None
-
-let restore_timeout = function
-  | None -> ()
-  | Some psh ->
-    (* stop alarm *)
-    ignore(Unix.alarm 0);
-    (* restore handler *)
-    Sys.set_signal Sys.sigalrm psh
+let disable_drop = function
+  | Drop -> Errors.error "Drop is forbidden."
+  | e -> e
 
+let user_error loc s = Errors.user_err_loc (loc,"_",str s)
 
 (* Open an utf-8 encoded file and skip the byte-order mark if any *)
 
 let open_utf8_file_in fname =
   let is_bom s =
-    Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF
+    Int.equal (Char.code s.[0]) 0xEF &&
+    Int.equal (Char.code s.[1]) 0xBB &&
+    Int.equal (Char.code s.[2]) 0xBF
   in
   let in_chan = open_in fname in
   let s = "   " in
@@ -141,7 +107,7 @@ let open_utf8_file_in fname =
    the file we parse seems a bit risky to me.  B.B.  *)
 
 let open_file_twice_if verbosely fname =
-  let paths = Library.get_load_paths () in
+  let paths = Loadpath.get_paths () in
   let _,longfname =
     find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
   let in_chan = open_utf8_file_in longfname in
@@ -159,23 +125,24 @@ let close_input in_chan (_,verb) =
   with e when Errors.noncritical e -> ()
 
 let verbose_phrase verbch loc =
-  let loc = unloc loc in
+  let loc = Loc.unloc loc in
   match verbch with
     | Some ch ->
 	let len = snd loc - fst loc in
 	let s = String.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
-        message s;
+        ppnl (str s);
         pp_flush()
-    | _ -> ()
+    | None -> ()
 
 exception End_of_input
 
-let parse_sentence (po, verbch) =
+let parse_sentence = Flags.with_option Flags.we_are_parsing
+  (fun (po, verbch) ->
   match Pcoq.Gram.entry_parse Pcoq.main_entry po with
     | Some (loc,_ as com) -> verbose_phrase verbch loc; com
-    | None -> raise End_of_input
+    | None -> raise End_of_input)
 
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
@@ -191,120 +158,106 @@ let set_formatter_translator() =
   Format.set_max_boxes max_int
 
 let pr_new_syntax loc ocom =
-  let loc = unloc loc in
+  let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
-  let fs = States.freeze () in
+  let fs = States.freeze ~marshallable:`No in
   let com = match ocom with
     | Some VernacNop -> mt()
-    | Some com -> pr_vernac com
+    | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
     msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
-    msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+    msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
-let rec vernac_com interpfun checknav (loc,com) =
-  let rec interp = function
-    | VernacLoad (verbosely, fname) ->
-	let fname = expand_path_macros fname in
-        (* translator state *)
-        let ch = !chan_beautify in
-        let cs = Lexer.com_state() in
-        let cl = !Pp.comments in
-        (* end translator state *)
-        (* coqdoc state *)
-        let cds = Dumpglob.coqdoc_freeze() in
-          if !Flags.beautify_file then
-	    begin
-              let _,f = find_file_in_path ~warn:(Flags.is_verbose())
-		(Library.get_load_paths ())
-		(make_suffix fname ".v") in
-		chan_beautify := open_out (f^beautify_suffix);
-		Pp.comments := []
-            end;
-          begin
-	    try
-	      read_vernac_file verbosely (make_suffix fname ".v");
-              if !Flags.beautify_file then close_out !chan_beautify;
-              chan_beautify := ch;
-              Lexer.restore_com_state cs;
-              Pp.comments := cl;
-              Dumpglob.coqdoc_unfreeze cds
-	    with reraise ->
-	      if !Flags.beautify_file then close_out !chan_beautify;
-              chan_beautify := ch;
-              Lexer.restore_com_state cs;
-              Pp.comments := cl;
-              Dumpglob.coqdoc_unfreeze cds;
-	      raise reraise
-	  end
-
-    | VernacList l -> List.iter (fun (_,v) -> interp v) l
-
-    | v when !just_parsing -> ()
+let save_translator_coqdoc () =
+  (* translator state *)
+  let ch = !chan_beautify in
+  let cl = !Pp.comments in
+  let cs = Lexer.com_state() in
+  (* end translator state *)
+  let coqdocstate = Lexer.location_table () in
+  ch,cl,cs,coqdocstate
+
+let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
+  if !Flags.beautify_file then close_out !chan_beautify;
+  chan_beautify := ch;
+  Pp.comments := cl;
+  Lexer.restore_com_state cs;
+  Lexer.restore_location_table coqdocstate
+
+(* For coqtop -time, we display the position in the file,
+   and a glimpse of the executed command *)
+
+let display_cmd_header loc com =
+  let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
+  let noblank s =
+    for i = 0 to String.length s - 1 do
+      match s.[i] with
+	| ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~'
+	| _ -> ()
+    done;
+    s
+  in
+  let (start,stop) = Loc.unloc loc in
+  let safe_pr_vernac x =
+    try Ppvernac.pr_vernac x
+    with e -> str (Printexc.to_string e) in
+  let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
+  in
+  Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
+	 str (" ["^cmd^"] "));
+  Pp.flush_all ()
 
-    | VernacFail v ->
-	begin try
-	  (* If the command actually works, ignore its effects on the state *)
-	  States.with_state_protection
-	    (fun v -> interp v; raise HasNotFailed) v
-	with e when Errors.noncritical e -> match real_error e with
-	  | HasNotFailed ->
-	      errorlabstrm "Fail" (str "The command has not failed !")
-	  | e ->
-	      (* Anomalies are re-raised by the next line *)
-	      let msg = Errors.print_no_anomaly e in
-	      if_verbose msgnl
-		(str "The command has indeed failed with message:" ++
-		 fnl () ++ str "=> " ++ hov 0 msg)
+let rec vernac_com verbosely checknav (loc,com) =
+  let interp = function
+    | VernacLoad (verbosely, fname) ->
+	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+	let st = save_translator_coqdoc () in
+	if !Flags.beautify_file then
+	  begin
+            let paths = Loadpath.get_paths () in
+            let _,f = find_file_in_path ~warn:(Flags.is_verbose())
+	      paths
+	      (CUnix.make_suffix fname ".v") in
+	    chan_beautify := open_out (f^beautify_suffix);
+	    Pp.comments := []
+          end;
+	begin
+	  try
+            read_vernac_file verbosely (CUnix.make_suffix fname ".v");
+	    restore_translator_coqdoc st;
+	  with reraise ->
+            let reraise = Errors.push reraise in
+	    restore_translator_coqdoc st;
+	    iraise reraise
 	end
 
-    | VernacTime v ->
-	  let tstart = System.get_time() in
-          interp v;
-	  let tend = System.get_time() in
-          msgnl (str"Finished transaction in " ++
-                   System.fmt_time_difference tstart tend)
-
-    | VernacTimeout(n,v) ->
-	  current_timeout := Some n;
-	  interp v
+    | v when !just_parsing -> ()
 
-    | v ->
-	  let psh = default_set_timeout () in
-	  try
-            States.with_heavy_rollback interpfun
-              Cerrors.process_vernac_interp_error v;
-	    restore_timeout psh
-	  with reraise -> restore_timeout psh; raise reraise
+    | v -> Stm.interp verbosely (loc,v)
   in
     try
       checknav loc com;
-      current_timeout := !default_timeout;
       if do_beautify () then pr_new_syntax loc (Some com);
+      if !Flags.time then display_cmd_header loc com;
+      let com = if !Flags.time then VernacTime [loc,com] else com in
       interp com
-    with any ->
+    with reraise ->
+      let (reraise, info) = Errors.push reraise in
       Format.set_formatter_out_channel stdout;
-      raise (DuringCommandInterp (loc, any))
+      let loc' = Option.default Loc.ghost (Loc.get_loc info) in
+      if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
+      else iraise (reraise, info)
 
 and read_vernac_file verbosely s =
   Flags.make_warn verbosely;
-  let interpfun =
-    if verbosely then Vernacentries.interp
-    else Flags.silently Vernacentries.interp
-  in
   let checknav loc cmd =
     if is_navigation_vernac cmd && not (is_reset cmd) then
 	user_error loc "Navigation commands forbidden in files"
   in
-  let end_inner_command cmd =
-    if !atomic_load || is_reset cmd then
-      Lib.mark_end_of_command () (* for Reset in coqc or coqtop -l *)
-    else
-      Backtrack.mark_command cmd; (* for Show Script, cf bug #2820 *)
-  in
   let (in_chan, fname, input) =
     open_file_twice_if verbosely s in
   try
@@ -312,19 +265,20 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com interpfun checknav loc_ast;
-      end_inner_command (snd loc_ast);
+      vernac_com verbosely checknav loc_ast;
       pp_flush ()
     done
-  with reraise ->   (* whatever the exception *)
+  with any ->   (* whatever the exception *)
+    let (e, info) = Errors.push any in
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
-    match real_error reraise with
+    match e with
       | End_of_input ->
-          if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
-      | _ -> raise_with_file fname reraise
+          if do_beautify () then
+            pr_new_syntax (Loc.make_loc (max_int,max_int)) None
+      | _ -> raise_with_file fname (disable_drop e, info)
 
-(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
+(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
    considered as non-state-preserving, in which case we add it to the
    Backtrack stack (triggering a save of a frozen state and the generation
@@ -335,43 +289,64 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr ?(preserving=false) loc_ast =
-  vernac_com Vernacentries.interp checknav loc_ast;
-  if not preserving && not (is_navigation_vernac (snd loc_ast)) then
-    Backtrack.mark_command (snd loc_ast)
-
-(* raw_do_vernac : Pcoq.Gram.parsable -> unit
- * vernac_step . parse_sentence *)
-let raw_do_vernac po = eval_expr (parse_sentence (po,None))
-
-(* XML output hooks *)
-let xml_start_library = ref (fun _ -> ())
-let xml_end_library = ref (fun _ -> ())
-
-let set_xml_start_library f = xml_start_library := f
-let set_xml_end_library f = xml_end_library := f
+let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
-    Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
     read_vernac_file verb file;
     if !Flags.beautify_file then close_out !chan_beautify;
-  with reraise ->
+  with any ->
+    let (e, info) = Errors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
-    raise_with_file file reraise
+    raise_with_file file (disable_drop e, info)
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
-  let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
-  Dumpglob.start_dump_glob long_f_dot_v;
-  Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
-  if !Flags.xml_export then !xml_start_library ();
-  let _ = load_vernac verbosely long_f_dot_v in
-  if Pfedit.get_all_proof_names () <> [] then
-    (message "Error: There are pending proofs"; exit 1);
-  if !Flags.xml_export then !xml_end_library ();
-  Dumpglob.end_dump_glob ();
-  Library.save_library_to ldir (long_f_dot_v ^ "o")
+  let check_pending_proofs () =
+    let pfs = Pfedit.get_all_proof_names () in
+    if not (List.is_empty pfs) then
+      (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+  match !Flags.compilation_mode with
+  | BuildVo ->
+      let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+      Stm.set_compilation_hints long_f_dot_v;
+      Aux_file.start_aux_file_for long_f_dot_v;
+      Dumpglob.start_dump_glob long_f_dot_v;
+      Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+      let wall_clock1 = Unix.gettimeofday () in
+      let _ = load_vernac verbosely long_f_dot_v in
+      Stm.join ();
+      let wall_clock2 = Unix.gettimeofday () in
+      check_pending_proofs ();
+      Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ());
+      Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
+        (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+      Aux_file.stop_aux_file ();
+      Dumpglob.end_dump_glob ()
+  | BuildVio ->
+      let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
+      Dumpglob.noglob ();
+      Stm.set_compilation_hints long_f_dot_v;
+      let _ = load_vernac verbosely long_f_dot_v in
+      Stm.finish ();
+      check_pending_proofs ();
+      Stm.snapshot_vio ldir long_f_dot_v;
+      Stm.reset_task_queue ()
+  | Vio2Vo ->
+      let open Filename in
+      let open Library in
+      Dumpglob.noglob ();
+      let f = if check_suffix f ".vio" then chop_extension f else f in
+      let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+      Stm.set_compilation_hints lfdv;
+      let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
+      Library.save_library_raw lfdv lib univs proofs
+
+let compile v f = 
+  ignore(CoqworkmgrApi.get 1);
+  compile v f;
+  CoqworkmgrApi.giveback 1
+