[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)

We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.

This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.

This is a critical step towards handling the STM functionally.

1 files changed, 0 insertions, 107 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1e09a1c0d..d736975d3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -103,11 +103,6 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> Pp.str ""
 
-let vernac_error msg =
-  Topfmt.std_logger Feedback.Error msg;
-  flush_all ();
-  exit 1
-
 (* Reenable when we get back to feedback printing *)
 (* let is_end_of_input any = match any with *)
 (*     Stm.End_of_input -> true *)
@@ -247,105 +242,3 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
 let process_expr doc sid loc_ast =
   checknav_deep loc_ast;
   interp_vernac ~interactive:true ~check:true doc sid loc_ast
-
-let warn_file_no_extension =
-  CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
-         (fun (f,ext) ->
-          str "File \"" ++ str f ++
-            strbrk "\" has been implicitly expanded to \"" ++
-            str f ++ str ext ++ str "\"")
-
-let ensure_ext ext f =
-  if Filename.check_suffix f ext then f
-  else begin
-    warn_file_no_extension (f,ext);
-    f ^ ext
-  end
-
-let chop_extension f =
-  try Filename.chop_extension f with _ -> f
-
-let ensure_bname src tgt =
-  let src, tgt = Filename.basename src, Filename.basename tgt in
-  let src, tgt = chop_extension src, chop_extension tgt in
-  if src <> tgt then
-    vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
-                  str "Source: " ++ str src                                                ++ fnl () ++
-                  str "Target: " ++ str 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
-    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 ~mode ~doc ~f_in ~f_out=
-  let check_pending_proofs () =
-    let pfs = Proof_global.get_all_proof_names () in
-    if not (List.is_empty pfs) then
-      vernac_error (str "There are pending proofs: "
-                    ++ (pfs
-                        |> List.rev
-                        |> prlist_with_sep pr_comma Names.Id.print)
-                    ++ str ".")
-  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 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
-      Stm.set_compilation_hints long_f_dot_vo;
-      Aux_file.(start_aux_file
-        ~aux_file:(aux_file_name_for long_f_dot_vo)
-        ~v_file:long_f_dot_v);
-      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 ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
-      let _doc = Stm.join ~doc in
-      let wall_clock2 = Unix.gettimeofday () in
-      check_pending_proofs ();
-      Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
-      Aux_file.record_in_aux_at "vo_compile_time"
-        (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-      Aux_file.stop_aux_file ();
-      Dumpglob.end_dump_glob ()
-  | BuildVio ->
-      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 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 ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
-      let doc = Stm.finish ~doc in
-      check_pending_proofs ();
-      let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
-      Stm.reset_task_queue ()
-  | Vio2Vo ->
-      let open Filename in
-      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
-      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 ~verbosely ~mode ~doc ~f_in ~f_out =
-  ignore(CoqworkmgrApi.get 1);
-  compile ~verbosely ~mode ~doc ~f_in ~f_out;
-  CoqworkmgrApi.giveback 1