aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml12
-rw-r--r--checker/votour.ml55
-rw-r--r--kernel/safe_typing.ml6
-rw-r--r--kernel/safe_typing.mli6
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--lib/system.ml45
-rw-r--r--lib/system.mli4
-rw-r--r--library/global.ml5
-rw-r--r--library/library.ml89
-rw-r--r--library/library.mli2
-rw-r--r--tools/coq_makefile.ml10
-rw-r--r--tools/coqc.ml2
-rw-r--r--tools/coqdep_common.ml13
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/stm.ml44
-rw-r--r--toplevel/stm.mli3
-rw-r--r--toplevel/vernac.ml43
18 files changed, 242 insertions, 102 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 366eb3695..5a1671fe6 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -301,12 +301,11 @@ let intern_from_file (dir, f) =
let (md,table,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
- let (md:Cic.library_disk) = System.marshal_in f ch in
- let digest = System.digest_in f ch in
- let (table:Cic.opaque_table) = System.marshal_in f ch in
+ let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
+ let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
+ let (table:Cic.opaque_table), pos, checksum =
+ System.marshal_in_segment f ch in
(* Verification of the final checksum *)
- let pos = pos_in ch in
- let checksum = System.digest_in f ch in
let () = close_in ch in
let ch = open_in f in
if not (String.equal (Digest.channel ch pos) checksum) then
@@ -315,6 +314,9 @@ let intern_from_file (dir, f) =
if dir <> md.md_name then
errorlabstrm "intern_from_file"
(name_clash_message dir md.md_name f);
+ if tasks <> None then
+ errorlabstrm "intern_from_file"
+ (str "The file "++str f++str " contains unfinished tasks");
(* Verification of the unmarshalled values *)
Validate.validate !Flags.debug Values.v_lib md;
Validate.validate !Flags.debug Values.v_opaques table;
diff --git a/checker/votour.ml b/checker/votour.ml
index 95f1ee85a..3f82b638f 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -126,6 +126,7 @@ let rec visit v o pos =
let l = read_line () in
try
if l = "u" then let info = pop () in visit info.typ info.obj info.pos
+ else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0)
else
let v',o',pos' = children.(int_of_string l) in
push (get_name v) v o pos;
@@ -134,28 +135,48 @@ let rec visit v o pos =
(** Loading the vo *)
-let opaque = ref false
+type segment = {
+ name : string;
+ mutable pos : int;
+ typ : Values.value;
+}
let visit_vo f =
- Printf.printf "Welcome to votour !\n";
- Printf.printf "Enjoy your guided tour of a Coq .vo\n";
- Printf.printf "Object sizes are in words\n";
- Printf.printf "At prompt, <n> enters the <n>-th child and u goes up\n%!";
+ Printf.printf "\nWelcome to votour !\n";
+ Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n";
+ Printf.printf "Object sizes are in words (%d bits)\n" Sys.word_size;
+ Printf.printf
+ "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
+ let segments = [|
+ {name="library"; pos=0; typ=Values.v_lib};
+ {name="STM tasks"; pos=0; typ=Opt Any};
+ {name="opaque proof terms"; pos=0; typ=Values.v_opaques};
+ |] in
let ch = open_in_bin f in
- let _magic = input_binary_int ch in
- let lib = (input_value ch : Obj.t) in (* actually Cic.library_disk *)
- let _ = Digest.input ch in
- let tbl = (input_value ch : Obj.t) in (* actually Cic.opaque_table *)
- let () = close_in ch in
- let o = if !opaque then tbl else lib in
- let ty = if !opaque then Values.v_opaques else Values.v_lib in
+ let magic = input_binary_int ch in
+ Printf.printf "File format: %d\n%!" magic;
+ for i=0 to Array.length segments - 1 do
+ let pos = input_binary_int ch in
+ segments.(i).pos <- pos_in ch;
+ seek_in ch pos;
+ ignore(Digest.input ch);
+ done;
+ Printf.printf "The file has %d segments, choose the one to visit:\n"
+ (Array.length segments);
+ Array.iteri (fun i { name; pos } ->
+ Printf.printf " %d: %s, starting at byte %d\n" i name pos)
+ segments;
+ Printf.printf "# %!";
+ let l = read_line () in
+ let seg = int_of_string l in
+ seek_in ch segments.(seg).pos;
+ let o = (input_value ch : Obj.t) in
let () = CObj.register_shared_size o in
let () = init () in
- visit ty o []
+ visit segments.(seg).typ o []
let main =
if not !Sys.interactive then
- Arg.parse ["-opaques",Arg.Set opaque,"visit the table of opaque terms"]
- visit_vo
- ("votour: guided tour of a Coq .vo file\n"^
- "Usage: votour [opts] foo.vo")
+ Arg.parse [] visit_vo
+ ("votour: guided tour of a Coq .vo or .vi file\n"^
+ "Usage: votour file.v[oi]")
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 66bc90789..3e9b646c1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -657,9 +657,11 @@ let start_library dir senv =
modvariant = LIBRARY;
imports = senv.imports }
-let export senv dir =
+let export compilation_mode senv dir =
let senv =
- try join_safe_environment senv
+ try
+ if compilation_mode = Flags.BuildVi then senv (* FIXME: cleanup future*)
+ else join_safe_environment senv
with e -> Errors.errorlabstrm "future" (Errors.print e)
in
let () = check_current_library dir senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index dcdb866bf..e2d1e37e9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -115,8 +115,10 @@ type native_library = Nativecode.global list
val start_library : DirPath.t -> module_path safe_transformer
-val export : safe_environment -> DirPath.t ->
- module_path * compiled_library * native_library
+val export :
+ Flags.compilation_mode ->
+ safe_environment -> DirPath.t ->
+ module_path * compiled_library * native_library
val import : compiled_library -> Digest.t ->
(module_path * Nativecode.symbol array) safe_transformer
diff --git a/lib/flags.ml b/lib/flags.ml
index b79f80d22..0cefc90c4 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,6 +45,8 @@ let boot = ref false
let batch_mode = ref false
+type compilation_mode = BuildVo | BuildVi
+let compilation_mode = ref BuildVo
let coq_slave_mode = ref (-1)
let coq_slaves_number = ref 1
diff --git a/lib/flags.mli b/lib/flags.mli
index 0b7adf33f..f0b676641 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,6 +11,8 @@
val boot : bool ref
val batch_mode : bool ref
+type compilation_mode = BuildVo | BuildVi
+val compilation_mode : compilation_mode ref
val coq_slave_mode : int ref
val coq_slaves_number : int ref
diff --git a/lib/system.ml b/lib/system.ml
index 015124e5b..aa6671116 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -114,17 +114,49 @@ let try_remove filename =
msg_warning
(str"Could not remove file " ++ str filename ++ str" which is corrupted!")
-let error_corrupted file = error (file ^ " is corrupted, try to rebuild it.")
+let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.")
+
+let input_binary_int f ch =
+ try input_binary_int ch
+ with
+ | End_of_file -> error_corrupted f "premature end of file"
+ | Failure s -> error_corrupted f s
+let output_binary_int ch x = output_binary_int ch x; flush ch
let marshal_out ch v = Marshal.to_channel ch v []; flush ch
let marshal_in filename ch =
try Marshal.from_channel ch
- with End_of_file | Failure _ -> error_corrupted filename
+ with
+ | End_of_file -> error_corrupted filename "premature end of file"
+ | Failure s -> error_corrupted filename s
let digest_out = Digest.output
let digest_in filename ch =
try Digest.input ch
- with End_of_file | Failure _ -> error_corrupted filename
+ with
+ | End_of_file -> error_corrupted filename "premature end of file"
+ | Failure s -> error_corrupted filename s
+
+let marshal_out_segment f ch v =
+ let start = pos_out ch in
+ output_binary_int ch 0; (* dummy value for stop *)
+ marshal_out ch v;
+ let stop = pos_out ch in
+ seek_out ch start;
+ output_binary_int ch stop;
+ seek_out ch stop;
+ digest_out ch (Digest.file f)
+
+let marshal_in_segment f ch =
+ let stop = (input_binary_int f ch : int) in
+ let v = marshal_in f ch in
+ let digest = digest_in f ch in
+ v, stop, digest
+
+let skip_in_segment f ch =
+ let stop = (input_binary_int f ch : int) in
+ seek_in ch stop;
+ stop, digest_in f ch
exception Bad_magic_number of string
@@ -136,11 +168,12 @@ let raw_extern_intern magic =
and intern_state filename =
try
let channel = open_in_bin filename in
- if not (Int.equal (input_binary_int channel) magic) then
+ if not (Int.equal (input_binary_int filename channel) magic) then
raise (Bad_magic_number filename);
channel
- with End_of_file | Failure _ | Sys_error _ ->
- error_corrupted filename
+ with
+ | End_of_file -> error_corrupted filename "premature end of file"
+ | Failure s | Sys_error s -> error_corrupted filename s
in
(extern_state,intern_state)
diff --git a/lib/system.mli b/lib/system.mli
index 2513ca19d..2e286a40c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -52,6 +52,10 @@ val marshal_in : string -> in_channel -> 'a
val digest_out : out_channel -> Digest.t -> unit
val digest_in : string -> in_channel -> Digest.t
+val marshal_out_segment : string -> out_channel -> 'a -> unit
+val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
+val skip_in_segment : string -> in_channel -> int * Digest.t
+
(** {6 Sending/receiving once with external executable } *)
val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
diff --git a/library/global.ml b/library/global.ml
index dac840ddb..9515ff1a8 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -24,7 +24,8 @@ end = struct
let global_env = ref Safe_typing.empty_environment
let join_safe_environment () =
- global_env := Safe_typing.join_safe_environment !global_env
+ if !Flags.compilation_mode <> Flags.BuildVi then
+ global_env := Safe_typing.join_safe_environment !global_env
let () =
Summary.declare_summary "Global environment"
@@ -127,7 +128,7 @@ let mind_of_delta_kn kn =
(** Operations on libraries *)
let start_library dir = globalize (Safe_typing.start_library dir)
-let export s = Safe_typing.export (safe_env ()) s
+let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s
let import cenv digest = globalize (Safe_typing.import cenv digest)
diff --git a/library/library.ml b/library/library.ml
index c3cc02fef..8b390832f 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -214,32 +214,51 @@ let locate_absolute_library dir =
let pref, base = split_dirpath dir in
let loadpath = Loadpath.expand_root_path pref in
let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
- try
- let name = (Id.to_string base)^".vo" in
- let _, file = System.where_in_path ~warn:false loadpath name in
- (dir, file)
- with Not_found ->
- (* Last chance, removed from the file system but still in memory *)
- if library_is_loaded dir then
- (dir, library_full_filename dir)
- else
- raise LibNotFound
+ let find ext =
+ try
+ let name = Id.to_string base ^ ext in
+ let _, file = System.where_in_path ~warn:false loadpath name in
+ [file]
+ with Not_found -> [] in
+ match find ".vo" @ find ".vi" with
+ | [] -> raise LibNotFound
+ | [file] -> dir, file
+ | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+ msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+ str vo ++ str " because it is more recent");
+ dir, vi
+ | [vo;vi] -> dir, vo
+ | _ -> assert false
let locate_qualified_library warn qid =
- try
- (* Search library in loadpath *)
- let dir, base = repr_qualid qid in
- let loadpath = Loadpath.expand_path dir in
- let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
- let name = Id.to_string base ^ ".vo" in
- let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name
- in
- let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in
- (* Look if loaded *)
- if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
- (* Otherwise, look for it in the file system *)
- else (LibInPath, dir, file)
- with Not_found -> raise LibNotFound
+ (* Search library in loadpath *)
+ let dir, base = repr_qualid qid in
+ let loadpath = Loadpath.expand_path dir in
+ let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
+ let find ext =
+ try
+ let name = Id.to_string base ^ ext in
+ let lpath, file =
+ System.where_in_path ~warn (List.map fst loadpath) name in
+ [lpath, file]
+ with Not_found -> [] in
+ let lpath, file =
+ match find ".vo" @ find ".vi" with
+ | [] -> raise LibNotFound
+ | [lpath, file] -> lpath, file
+ | [lpath_vo, vo; lpath_vi, vi]
+ when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+ msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+ str vo ++ str " because it is more recent");
+ lpath_vi, vi
+ | [lpath_vo, vo; _ ] -> lpath_vo, vo
+ | _ -> assert false
+ in
+ let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in
+ (* Look if loaded *)
+ if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir)
+ (* Otherwise, look for it in the file system *)
+ else (LibInPath, dir, file)
let error_unmapped_dir qid =
let prefix, _ = repr_qualid qid in
@@ -289,10 +308,7 @@ let fetch_opaque_table dp (f,pos,digest) =
let ch = System.with_magic_number_check raw_intern_library f in
let () = seek_in ch pos in
if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
- let table = (System.marshal_in f ch : Term.constr array) in
- (* Check of the final digest (the one also covering the opaques) *)
- let pos' = pos_in ch in
- let digest' = System.digest_in f ch in
+ let table, pos', digest' = System.marshal_in_segment f ch in
let () = close_in ch in
let ch' = open_in f in
if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty;
@@ -370,12 +386,11 @@ let mk_library md digest =
let intern_from_file f =
let ch = System.with_magic_number_check raw_intern_library f in
- let lmd = (System.marshal_in f ch : library_disk) in
- let pos = pos_in ch in
- let digest = System.digest_in f ch in
+ let lmd, _, digest_lmd = System.marshal_in_segment f ch in
+ let pos, digest = System.skip_in_segment f ch in
register_library_filename lmd.md_name f;
add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
- let library = mk_library lmd digest in
+ let library = mk_library lmd digest_lmd in
close_in ch;
library
@@ -607,7 +622,8 @@ let error_recursively_dependent_library dir =
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
-let save_library_to dir f =
+let save_library_to ?todo dir f =
+ let f = if todo = None then f ^ "o" else f ^ "i" in
Lazyconstr.reset_indirect_opaque_creator ();
let cenv, seg, ast = Declaremods.end_library dir in
let table = OpaqueTables.dump () in
@@ -623,10 +639,9 @@ let save_library_to dir f =
let (f',ch) = raw_extern_library f in
try
(* Writing vo payload *)
- System.marshal_out ch md; (* env + objs *)
- System.digest_out ch (Digest.file f'); (* 1st checksum *)
- System.marshal_out ch table; (* opaques *)
- System.digest_out ch (Digest.file f'); (* 2nd checksum *)
+ System.marshal_out_segment f' ch md; (* env + objs *)
+ System.marshal_out_segment f' ch todo; (* STM tasks *)
+ System.marshal_out_segment f' ch table; (* opaques *)
close_out ch;
(* Writing native code files *)
if not !Flags.no_native_compiler then
diff --git a/library/library.mli b/library/library.mli
index 8ed3afd66..530209485 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -37,7 +37,7 @@ val import_module : bool -> qualid located -> unit
val start_library : string -> DirPath.t * string
(** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : DirPath.t -> string -> unit
+val save_library_to : ?todo:'a -> DirPath.t -> string -> unit
(** {6 Interrogate the status of libraries } *)
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index bf2a09180..eefad3442 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -297,7 +297,7 @@ let clean sds sps =
print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
end;
if !some_vfile then
- print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n";
+ print "\trm -f $(VOFILES) $(VOFILES:.vo=.vi) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n";
print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
print "\t- rm -rf html mlihtml uninstall_me.sh\n";
List.iter
@@ -353,7 +353,7 @@ let implicit () =
in
let v_rules () =
print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "%.vi: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.g: %.v\n\t$(GALLINA) $<\n\n";
print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
@@ -520,10 +520,10 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
begin match vfiles with
|[] -> ()
|l ->
- print "VOFILES:=$(VFILES:.v=.vo)\n";
+ print "VO=vo\n";
+ print "VOFILES:=$(VFILES:.v=.$(VO))\n";
classify_files_by_root "VOFILES" l inc;
print "GLOBFILES:=$(VFILES:.v=.glob)\n";
- print "VIFILES:=$(VFILES:.v=.vi)\n";
print "GFILES:=$(VFILES:.v=.g)\n";
print "HTMLFILES:=$(VFILES:.v=.html)\n";
print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"
@@ -616,7 +616,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
end;
if !some_vfile then
begin
- print "spec: $(VIFILES)\n\n";
+ print "quick:\n\t$(MAKE) all VO=vi\n";
print "gallina: $(GFILES)\n\n";
print "html: $(GLOBFILES) $(VFILES)\n";
print "\t- mkdir -p html\n";
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 89ab64b67..3b01f90c4 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -117,7 +117,7 @@ let parse_args () =
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
|"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
|"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
- |"-impredicative-set"|"-vm"|"-no-native-compiler"
+ |"-impredicative-set"|"-vm"|"-no-native-compiler"|"-quick"
|"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem ->
parse (cfiles,o::args) rem
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 4dcd10ece..a952881c8 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -298,7 +298,7 @@ let canonize f =
| (f,_) :: _ -> escape f
| _ -> escape f
-let rec traite_fichier_Coq verbose f =
+let rec traite_fichier_Coq suffixe verbose f =
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
@@ -314,7 +314,7 @@ let rec traite_fichier_Coq verbose f =
addQueue deja_vu_v str;
try
let file_str = safe_assoc verbose f str in
- printf " %s%s" (canonize file_str) !suffixe
+ printf " %s%s" (canonize file_str) suffixe
with Not_found ->
if verbose && not (Hashtbl.mem coqlibKnown str) then
warning_module_notfound f str
@@ -325,7 +325,7 @@ let rec traite_fichier_Coq verbose f =
addQueue deja_vu_v [str];
try
let file_str = Hashtbl.find vKnown [str] in
- printf " %s%s" (canonize file_str) !suffixe
+ printf " %s%s" (canonize file_str) suffixe
with Not_found ->
if not (Hashtbl.mem coqlibKnown [str]) then
warning_notfound f s
@@ -359,7 +359,7 @@ let rec traite_fichier_Coq verbose f =
let file_str = Hashtbl.find vKnown [str] in
let canon = canonize file_str in
printf " %s.v" canon;
- traite_fichier_Coq true (canon ^ ".v")
+ traite_fichier_Coq suffixe true (canon ^ ".v")
with Not_found -> ()
end
| AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
@@ -417,7 +417,10 @@ let coq_dependencies () =
let ename = escape name in
let glob = if !option_noglob then "" else " "^ename^".glob" in
printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
- traite_fichier_Coq true (name ^ ".v");
+ traite_fichier_Coq !suffixe true (name ^ ".v");
+ printf "\n";
+ printf "%s.vi: %s.v" ename ename;
+ traite_fichier_Coq ".vi" true (name ^ ".v");
printf "\n";
flush stdout)
(List.rev !vAccu)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b75a22558..ad3ce7879 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -320,6 +320,7 @@ let parse_args arglist =
|"-q" -> no_load_rc ()
|"-quality" -> term_quality := true; no_load_rc ()
|"-quiet"|"-silent" -> Flags.make_silent true
+ |"-quick" -> Flags.compilation_mode := BuildVi
|"-time" -> Flags.time := true
|"-unicode" -> add_require "Utf8_core"
|"-v"|"--version" -> Usage.version (exitcode ())
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index fe8cc66a8..f800b49fb 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -594,6 +594,8 @@ module Slaves : sig
val set_reach_known_state :
(?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit
+ type tasks
+ val dump : unit -> tasks
end = struct (* {{{ *)
@@ -604,6 +606,7 @@ end = struct (* {{{ *)
val pop : 'a t -> 'a
val push : 'a t -> 'a -> unit
val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
+ val dump : 'a t -> 'a list
end = struct (* {{{ *)
@@ -639,6 +642,13 @@ end = struct (* {{{ *)
while not (Queue.is_empty q) || !n < j do Condition.wait cn m done;
Mutex.unlock m
+ let dump (q,m,_,_,_) =
+ let l = ref [] in
+ Mutex.lock m;
+ while not (Queue.is_empty q) do l := Queue.pop q :: !l done;
+ Mutex.unlock m;
+ List.rev !l
+
end (* }}} *)
module SlavesPool : sig
@@ -745,10 +755,11 @@ end = struct (* {{{ *)
let cancel_switch_of_task = function
| TaskBuildProof (_,_,_,_,c,_) -> c
+ let build_proof_here_core eop () =
+ !reach_known_state ~cache:`No eop;
+ Proof_global.return_proof ()
let build_proof_here (id,valid) eop =
- Future.create (State.exn_on id ~valid) (fun () ->
- !reach_known_state ~cache:`No eop;
- Proof_global.return_proof ())
+ Future.create (State.exn_on id ~valid) (build_proof_here_core eop)
let slave_respond msg =
match msg with
@@ -818,13 +829,22 @@ end = struct (* {{{ *)
let queue : task TQueue.t = TQueue.create ()
let wait_all_done () =
- TQueue.wait_until_n_are_waiting_and_queue_empty
- (SlavesPool.n_slaves ()) queue
+ if not (SlavesPool.is_empty ()) then
+ TQueue.wait_until_n_are_waiting_and_queue_empty
+ (SlavesPool.n_slaves ()) queue
let build_proof ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
let cancel_switch = ref false in
if SlavesPool.is_empty () then
- build_proof_here exn_info stop, cancel_switch
+ if !Flags.compilation_mode = Flags.BuildVi then begin
+ let force () : Entries.proof_output list Future.assignement =
+ try `Val (build_proof_here_core stop ()) with e -> `Exn e in
+ let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
+ TQueue.push queue
+ (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,name));
+ f, cancel_switch
+ end else
+ build_proof_here exn_info stop, cancel_switch
else
let f, assign = Future.create_delegate (State.exn_on id ~valid) in
Pp.feedback (Interface.InProgress 1);
@@ -1024,6 +1044,15 @@ end = struct (* {{{ *)
flush_all (); exit 1
done
+ (* For external users this name is nicer than request *)
+ type tasks = request list
+ let dump () =
+ assert(SlavesPool.is_empty ()); (* ATM, we allow that only if no slaves *)
+ let tasks = TQueue.dump queue in
+ prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks));
+ let tasks = List.map request_of_task tasks in
+ tasks
+
end (* }}} *)
(* Runs all transactions needed to reach a state *)
@@ -1408,6 +1437,9 @@ let join () =
jab (VCS.get_branch_pos VCS.Branch.master);
VCS.print ()
+type tasks = Slaves.tasks
+let dump () = Slaves.dump ()
+
let merge_proof_branch qast keep brname =
let brinfo = VCS.get_branch brname in
let qed fproof = { qast; keep; brname; brinfo; fproof } in
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 3c5bd63db..d821a2536 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -40,6 +40,9 @@ val finish : unit -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)
val join : unit -> unit
+(* To save to disk an incomplete document *)
+type tasks
+val dump : unit -> tasks
(* Id of the tip of the current branch *)
val get_current_state : unit -> Stateid.t
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index eaa5b7549..27735d2d9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -305,7 +305,6 @@ and read_vernac_file verbosely s =
close_input in_chan input; (* we must close the file first *)
match e with
| End_of_input ->
- Stm.join ();
if do_beautify () then
pr_new_syntax (Loc.make_loc (max_int,max_int)) None
| _ -> raise_with_file fname (disable_drop e)
@@ -341,15 +340,33 @@ let load_vernac verb file =
(* 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.DirPath.to_string ldir ^ "\n");
- if !Flags.xml_export then Hook.get f_xml_start_library ();
- let _ = load_vernac verbosely long_f_dot_v in
- let pfs = Pfedit.get_all_proof_names () in
- if not (List.is_empty pfs) then
- (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1);
- if !Flags.xml_export then Hook.get f_xml_end_library ();
- Library.save_library_to ldir (long_f_dot_v ^ "o");
- Dumpglob.end_dump_glob ()
-
+ let check_pending_proofs () =
+ let pfs = Pfedit.get_all_proof_names () in
+ if not (List.is_empty pfs) then
+ (pperrnl (str "Error: 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
+ 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");
+ if !Flags.xml_export then Hook.get f_xml_start_library ();
+ 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;
+ Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
+ (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+ Aux_file.stop_aux_file ();
+ if !Flags.xml_export then Hook.get f_xml_end_library ();
+ Dumpglob.end_dump_glob ()
+ | BuildVi ->
+ let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
+ Dumpglob.noglob ();
+ let _ = load_vernac verbosely long_f_dot_v in
+ Stm.finish ();
+ check_pending_proofs ();
+ let todo = Stm.dump () in
+ Library.save_library_to ~todo ldir long_f_dot_v
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 19:15:18 +0000