[stm] [flags] Move document mode flags to the STM.

We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.

Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.

In particular:

== Added flags ==

- `Safe_typing.allow_delayed_constants`
  Allow delayed constants in the kernel.

- `Flags.record_aux_file`
  Output `Proof using` information from the kernel.

- `System.trust_file_cache`
  Assume that the file system won't change during our run.

== Deleted flags ==

- `Flags.compilation_mode`
- `Flags.batch_mode`

Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.

The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.

5 files changed, 151 insertions, 105 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 1d5406770..8f676c656 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -32,7 +32,7 @@ let load_rcfile sid =
     try
       if !rcfile_specified then
         if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac false sid !rcfile
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
@@ -43,7 +43,7 @@ let load_rcfile sid =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac false sid inferedrc
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid inferedrc
 	with Not_found -> sid
 	(*
 	Flags.if_verbose
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c159a1c6a..0624c9bed 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -9,7 +9,6 @@
 open Pp
 open CErrors
 open Libnames
-open Coqinit
 
 let () = at_exit flush_all
 
@@ -121,6 +120,14 @@ let print_memory_stat () =
 
 let _ = at_exit print_memory_stat
 
+(******************************************************************************)
+(* Deprecated                                                                 *)
+(******************************************************************************)
+let _remove_top_ml () = Mltop.remove ()
+
+(******************************************************************************)
+(* Engagement                                                                 *)
+(******************************************************************************)
 let impredicative_set = ref Declarations.PredicativeSet
 let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
 let set_type_in_type () =
@@ -129,14 +136,18 @@ let set_type_in_type () =
 let engage () =
   Global.set_engagement !impredicative_set
 
-let set_batch_mode () = Flags.batch_mode := true
-
+(******************************************************************************)
+(* Interactive toplevel name                                                  *)
+(******************************************************************************)
 let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
 let toplevel_name = ref toplevel_default_name
 let set_toplevel_name dir =
   if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name");
   toplevel_name := dir
 
+(******************************************************************************)
+(* Input/Output State                                                         *)
+(******************************************************************************)
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> strbrk "The inputstate option is deprecated and discouraged.")
@@ -164,21 +175,22 @@ let outputstate () =
     let fname = CUnix.make_suffix !outputstate ".coq" in
     States.extern_state fname
 
-let set_include d p implicit =
-  let p = dirpath_of_string p in
-  push_include d p implicit
-
+(******************************************************************************)
+(* Interactive Load File Simulation                                           *)
+(******************************************************************************)
 let load_vernacular_list = ref ([] : (string * bool) list)
+
 let add_load_vernacular verb s =
   load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
+
 let load_vernacular sid =
   List.fold_left
-    (fun sid (s,v) ->
-      let s = Loadpath.locate_file s in
+    (fun sid (f_in, verbosely) ->
+      let s = Loadpath.locate_file f_in in
       if !Flags.beautify then
-	Flags.(with_option beautify_file (Vernac.load_vernac v sid) s)
+	Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid) f_in
       else
-	Vernac.load_vernac v sid s)
+	Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid s)
     sid (List.rev !load_vernacular_list)
 
 let load_vernacular_obj = ref ([] : string list)
@@ -187,6 +199,13 @@ let load_vernac_obj () =
   let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in
   Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj)
 
+(******************************************************************************)
+(* Required Modules                                                           *)
+(******************************************************************************)
+let set_include d p implicit =
+  let p = dirpath_of_string p in
+  Coqinit.push_include d p implicit
+
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
   let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in
@@ -209,10 +228,23 @@ let add_compat_require v =
   | Flags.V8_7 -> add_require "Coq.Compat.Coq87"
   | Flags.VOld | Flags.Current -> ()
 
-let compile_list = ref ([] : (bool * string) list)
+(******************************************************************************)
+(* File Compilation                                                           *)
+(******************************************************************************)
 
 let glob_opt = ref false
 
+let compile_list = ref ([] : (bool * string) list)
+let _compilation_list : Stm.stm_doc_type list ref = ref []
+
+let compilation_mode = ref Vernac.BuildVo
+let compilation_output_name = ref None
+
+let batch_mode = ref false
+let set_batch_mode () =
+  System.trust_file_cache := false;
+  batch_mode := true
+
 let add_compile verbose s =
   set_batch_mode ();
   Flags.quiet := true;
@@ -226,21 +258,66 @@ let add_compile verbose s =
   in
   compile_list := (verbose,s) :: !compile_list
 
-let compile_file (v,f) =
+let compile_file mode (verbosely,f_in) =
   if !Flags.beautify then
-    Flags.(with_option beautify_file (Vernac.compile v) f)
+    Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~f_in ~f_out:None) f_in
   else
-    Vernac.compile v f
+    Vernac.compile ~verbosely ~mode ~f_in ~f_out:None
 
 let compile_files () =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
+    let mode = !compilation_mode in
     List.iter (fun vf ->
         States.unfreeze init_state;
-        compile_file vf)
+        compile_file mode vf)
       (List.rev !compile_list)
 
+(******************************************************************************)
+(* VIO Dispatching                                                            *)
+(******************************************************************************)
+
+let vio_tasks = ref []
+let add_vio_task f =
+  set_batch_mode ();
+  Flags.quiet := true;
+  vio_tasks := f :: !vio_tasks
+let check_vio_tasks () =
+  let rc =
+    List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+      true (List.rev !vio_tasks) in
+  if not rc then exit 1
+
+(* vio files *)
+let vio_files = ref []
+let vio_files_j = ref 0
+let vio_checking = ref false
+let add_vio_file f =
+  set_batch_mode ();
+  Flags.quiet := true;
+  vio_files := f :: !vio_files
+
+let set_vio_checking_j opt j =
+  try 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 schedule_vio_checking () =
+  if !vio_files <> [] && !vio_checking then
+    Vio_checking.schedule_vio_checking !vio_files_j !vio_files
+
+let schedule_vio_compilation () =
+  if !vio_files <> [] && not !vio_checking then
+    Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
+
+(******************************************************************************)
+(* UI Options                                                                 *)
+(******************************************************************************)
 (** Options for proof general *)
 
 let set_emacs () =
@@ -296,14 +373,15 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy
     (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
 
 exception NoCoqLib
-let usage () =
+
+let usage batch =
   begin
   try
   Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
-  init_load_path ();
+  Coqinit.init_load_path ();
   with NoCoqLib -> usage_no_coqlib ()
   end;
-  if !Flags.batch_mode then Usage.print_usage_coqc ()
+  if batch then Usage.print_usage_coqc ()
   else begin
     Mltop.load_ml_objects_raw_rex
       (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
@@ -389,47 +467,10 @@ let get_error_resilience opt = function
 
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
-let vio_tasks = ref []
-
-let add_vio_task f =
-  set_batch_mode ();
-  Flags.quiet := true;
-  vio_tasks := f :: !vio_tasks
-
-let check_vio_tasks () =
-  let rc =
-    List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
-      true (List.rev !vio_tasks) in
-  if not rc then exit 1
-
-let vio_files = ref []
-let vio_files_j = ref 0
-let vio_checking = ref false
-let add_vio_file f =
-  set_batch_mode ();
-  Flags.quiet := true;
-  vio_files := f :: !vio_files
-
-let set_vio_checking_j opt j =
-  try 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 is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
   | _ -> false
 
-let schedule_vio_checking () =
-  if !vio_files <> [] && !vio_checking then
-    Vio_checking.schedule_vio_checking !vio_files_j !vio_files
-let schedule_vio_compilation () =
-  if !vio_files <> [] && not !vio_checking then
-    Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
-
 let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
   try
@@ -464,7 +505,7 @@ let parse_args arglist =
     (* Complex options with many args *)
     |"-I"|"-include" ->
       begin match rem with
-      | d :: rem -> push_ml_include d; args := rem
+      | d :: rem -> Coqinit.push_ml_include d; args := rem
       | [] -> error_missing_arg opt
       end
     |"-Q" ->
@@ -522,7 +563,7 @@ let parse_args arglist =
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
     |"-feedback-glob" -> Dumpglob.feedback_glob ()
     |"-exclude-dir" -> System.exclude_directory (next ())
-    |"-init-file" -> set_rcfile (next ())
+    |"-init-file" -> Coqinit.set_rcfile (next ())
     |"-inputstate"|"-is" -> set_inputstate (next ())
     |"-load-ml-object" -> Mltop.dir_ml_load (next ())
     |"-load-ml-source" -> Mltop.dir_ml_use (next ())
@@ -537,7 +578,9 @@ let parse_args arglist =
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
-    |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo
+    |"-vio2vo" ->
+      add_compile false (next ());
+      compilation_mode := Vernac.Vio2Vo
     |"-toploop" -> set_toploop (next ())
     |"-w" | "-W" ->
       let w = next () in
@@ -545,7 +588,7 @@ let parse_args arglist =
       else
         let w = CWarnings.get_flags () ^ "," ^ w in
         CWarnings.set_flags (CWarnings.normalize_flags_string w)
-    |"-o" -> Flags.compilation_output_name := Some (next())
+    |"-o" -> compilation_output_name := Some (next())
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
@@ -557,15 +600,15 @@ let parse_args arglist =
     |"-batch" -> set_batch_mode ()
     |"-test-mode" -> Flags.test_mode := true
     |"-beautify" -> Flags.beautify := true
-    |"-boot" -> Flags.boot := true; no_load_rc ()
+    |"-boot" -> Flags.boot := true; Coqinit.no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
     |"-color" -> set_color (next ())
     |"-config"|"--config" -> print_config := true
-    |"-debug" -> set_debug ()
+    |"-debug" -> Coqinit.set_debug ()
     |"-stm-debug" -> Flags.stm_debug := true
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode
     |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
@@ -578,9 +621,11 @@ let parse_args arglist =
       else Flags.native_compiler := true
     |"-output-context" -> output_context := true
     |"-profile-ltac" -> Flags.profile_ltac := true
-    |"-q" -> no_load_rc ()
+    |"-q" -> Coqinit.no_load_rc ()
     |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
-    |"-quick" -> Flags.compilation_mode := Flags.BuildVio
+    |"-quick" ->
+      Safe_typing.allow_delayed_constants := true;
+      compilation_mode := Vernac.BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
     |"-type-in-type" -> set_type_in_type ()
@@ -615,7 +660,7 @@ let init_toplevel arglist =
       if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
       if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
-      init_load_path ();
+      Coqinit.init_load_path ();
       Option.iter Mltop.load_ml_object_raw !toploop;
       let extras = !toploop_init extras in
       if not (CList.is_empty extras) then begin
@@ -627,19 +672,19 @@ let init_toplevel arglist =
       inputstate ();
       Mltop.init_known_plugins ();
       engage ();
-      if (not !Flags.batch_mode || CList.is_empty !compile_list)
+      if (not !batch_mode || CList.is_empty !compile_list)
          && Global.env_is_initial ()
       then Declaremods.start_library !toplevel_name;
       load_vernac_obj ();
       require ();
-      (* XXX: This is incorrect in batch mode, as we will initialize
-         the STM before having done Declaremods.start_library, thus
-         state 1 is invalid. This bug was present in 8.5/8.6. *)
-      Stm.init ();
-      let sid  = load_rcfile (Stm.get_current_state ()) in
+      Stm.(init { doc_type = Interactive Names.DirPath.empty });
+      let sid  = Coqinit.load_rcfile (Stm.get_current_state ()) in
       (* XXX: We ignore this for now, but should be threaded to the toplevels *)
       let _sid = load_vernacular sid in
       compile_files ();
+      (* All these tasks use coqtop as a driver to invoke more coqtop,
+       * they should be really orthogonal to coqtop.
+       *)
       schedule_vio_checking ();
       schedule_vio_compilation ();
       check_vio_tasks ();
@@ -647,13 +692,13 @@ let init_toplevel arglist =
     with any ->
       flush_all();
       let extra =
-        if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
         then None
         else Some (str "Error during initialization: ")
       in
       fatal_error ?extra any
   end;
-  if !Flags.batch_mode then begin
+  if !batch_mode then begin
     flush_all();
     if !output_context then
       Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 892d64d91..ac2be7e16 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,7 +15,6 @@ val init_toplevel : string list -> unit
 
 val start : unit -> unit
 
-
 (* For other toploops *)
 val toploop_init : (string list -> string list) ref
 val toploop_run : (unit -> unit) ref
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1b020bc87..cb89dc8ff 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -113,13 +113,13 @@ let vernac_error msg =
 (*     Stm.End_of_input -> true *)
 (*   | _ -> false *)
 
-let rec interp_vernac sid (loc,com) =
+let rec interp_vernac ~check ~interactive sid (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-        load_vernac verbosely sid f
+        load_vernac ~verbosely ~check ~interactive sid f
     | v ->
 
       (* XXX: We need to run this before add as the classification is
@@ -142,17 +142,16 @@ let rec interp_vernac sid (loc,com) =
       (* Main STM interaction *)
       if ntip <> `NewTip then
         anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
+
       (* Due to bug #5363 we cannot use observe here as we should,
          it otherwise reveals bugs *)
       (* Stm.observe nsid; *)
-
-      let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in
-      if check_proof then Stm.finish ();
+      if check then Stm.finish ();
 
       (* We could use a more refined criteria that depends on the
          vernac. For now we imitate the old approach and rely on the
          classification. *)
-      let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+      let print_goals = interactive && not !Flags.quiet &&
                         is_proof_step && Proof_global.there_are_pending_proofs () in
 
       if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
@@ -167,7 +166,7 @@ let rec interp_vernac sid (loc,com) =
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
          things, so we better avoid it while we investigate *)
-      if not !Flags.batch_mode then ignore(Stm.edit_at sid);
+      if interactive then ignore(Stm.edit_at sid);
       let (reraise, info) = CErrors.push reraise in
       let info = begin
         match Loc.get_loc info with
@@ -176,7 +175,7 @@ let rec interp_vernac sid (loc,com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac verbosely sid file =
+and load_vernac ~verbosely ~check ~interactive sid file =
   let ft_beautify, close_beautify =
     if !Flags.beautify_file then
       let chan_beautify = open_out (file^beautify_suffix) in
@@ -217,7 +216,7 @@ and load_vernac verbosely sid file =
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
-      let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in
+      let nsid = Flags.silently (interp_vernac ~check ~interactive !rsid) (loc, ast) in
       rsid := nsid
     done;
     !rsid
@@ -245,7 +244,7 @@ and load_vernac verbosely sid file =
 
 let process_expr sid loc_ast =
   checknav_deep loc_ast;
-  interp_vernac sid loc_ast
+  interp_vernac ~interactive:true ~check:true sid loc_ast
 
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
@@ -282,8 +281,10 @@ let ensure_exists f =
   if not (Sys.file_exists f) then
     vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+
 (* Compile a vernac file *)
-let compile verbosely f =
+let compile ~verbosely ~mode ~f_in ~f_out=
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
     if not (List.is_empty pfs) then
@@ -293,12 +294,12 @@ let compile verbosely f =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
-  match !Flags.compilation_mode with
-  | Flags.BuildVo ->
-      let long_f_dot_v = ensure_v f in
+  match mode with
+  | BuildVo ->
+      let long_f_dot_v = ensure_v f_in in
       ensure_exists long_f_dot_v;
       let long_f_dot_vo =
-        match !Flags.compilation_output_name with
+        match f_out with
         | None -> long_f_dot_v ^ "o"
         | Some f -> ensure_vo long_f_dot_v f in
       let ldir = Flags.verbosely Library.start_library long_f_dot_vo in
@@ -309,7 +310,7 @@ let compile verbosely f =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
+      let _ = load_vernac ~verbosely ~check:true ~interactive:false (Stm.get_current_state ()) long_f_dot_v in
       Stm.join ();
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -318,32 +319,31 @@ let compile verbosely f =
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
-  | Flags.BuildVio ->
-      let long_f_dot_v = ensure_v f in
+  | BuildVio ->
+      let long_f_dot_v = ensure_v f_in in
       ensure_exists long_f_dot_v;
       let long_f_dot_vio =
-        match !Flags.compilation_output_name with
+        match f_out with
         | None -> long_f_dot_v ^ "io"
         | Some f -> ensure_vio long_f_dot_v f in
       let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_vio;
-      let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
+      let _ = load_vernac ~verbosely ~check:false ~interactive:false (Stm.get_current_state ()) long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
       Stm.snapshot_vio ldir long_f_dot_vio;
       Stm.reset_task_queue ()
-  | Flags.Vio2Vo ->
+  | 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, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
+      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
       Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile v f =
+let compile ~verbosely ~mode ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile v f;
+  compile ~verbosely ~mode ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index bccf560e1..410dcf0d4 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -17,7 +17,9 @@ val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.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
     and print errors in form of exceptions. *)
-val load_vernac : bool -> Stateid.t -> string -> Stateid.t
+val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stateid.t -> string -> Stateid.t
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
-val compile : bool -> string -> unit
+val compile : verbosely:bool -> mode:compilation_mode -> f_in:string -> f_out:string option -> unit