Aux_file: cache information at compile time for later (re)use

For a file dir/a.v the corresponding aux file dir/.a.aux can store
arbitrary data.  It maps a "Loc.t * string" (key) to a "string" (value).

Pretty much anything can fit in this schema, but ATM I see only the
following possible uses:

1) record inferred data, like the set of section variable used, so that
   one can later use this info to process proofs asynchronously (i.e.
   compute their discharged type without knowing the proof term).
2) record timings (how long it takes to build a proof term or check it),
   so that one can take smarter scheduling decisions
3) record a bloated proof trace for automatic tactics, so that one can
   replay it faster (a sort of cache).  For that to be useful an Ltac
   API is required.

The .aux file contains the path of the .v and its md5 hash.  When loaded
it defaults to the empty map is the file is not there or if the .v file
changed.

Not finding some data in the .aux file cannot be a failure, but finding
it may help in many ways.

The current file format is very simple but human readable.  It is
generated/parsed using printf/scanf and in particular the %S formatter
for the value string.  The file format is private to the Aux_file
module: only an abstract interface is provided.

The current file format is not robust in face of local changes.
Any change invalidates the md5 hash (and the Loc.t is very likely to
change too).

3 files changed, 105 insertions, 0 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
new file mode 100644
index 000000000..98f1a51b8
--- /dev/null
+++ b/lib/aux_file.ml
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The file format is a header
+ *     ("COQAUX%d %s %s\n" version hex_hash path)
+ * followed by an arbitrary number of entries
+ *     ("%d %d %s %S\n" loc_begin loc_end key value)  *)
+
+open Filename
+
+let version = 1
+
+let oc = ref None
+
+let aux_file_name_for vfile =
+  dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
+
+let start_aux_file_for vfile =
+  oc := Some (open_out (aux_file_name_for vfile));
+  Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n"
+    version (Digest.to_hex (Digest.file vfile)) (CUnix.strip_path vfile)
+
+let stop_aux_file () =
+  close_out (Option.get !oc);
+  oc := None
+
+let recording () = not (Option.is_empty !oc)
+
+module H = Map.Make(struct type t = int * int let compare = compare end)
+module M = Map.Make(String)
+type data = string M.t
+type aux_file = data H.t
+
+let empty_aux_file = H.empty
+
+let get aux loc key = M.find key (H.find (Loc.unloc loc) aux)
+
+let record_in_aux_at loc key v =
+  Option.iter (fun oc ->
+    let i, j = Loc.unloc loc in
+    Printf.fprintf oc "%d %d %s %S\n" i j key v)
+  !oc
+
+let current_loc = ref Loc.ghost
+
+let record_in_aux_set_at loc = current_loc := loc
+
+let record_in_aux key v = record_in_aux_at !current_loc key v
+
+exception Outdated
+
+let load_aux_file_for vfile =
+  let ret3 x y z = x, y, z in
+  let ret4 x y z t = x, y, z, t in
+  let h = ref empty_aux_file in
+  let add loc k v =
+    let m = try H.find loc !h with Not_found -> M.empty in
+    h := H.add loc (M.add k v m) !h in
+  let aux_fname = aux_file_name_for vfile in
+  try
+    let ic = open_in aux_fname in
+    let ver, hash, fname = Scanf.fscanf ic "COQAUX%d %s %s\n" ret3 in
+    if ver <> version then raise (Failure "aux file version mismatch");
+    if fname <> CUnix.strip_path vfile then
+      raise (Failure "aux file name mismatch");
+    if Digest.to_hex (Digest.file vfile) <> hash then raise Outdated;
+    while true do
+      let i, j, k, v = Scanf.fscanf ic "%d %d %s %S\n" ret4 in
+      add (i,j) k v;
+    done;
+    raise End_of_file
+  with
+  | End_of_file -> !h
+  | Outdated -> empty_aux_file
+  | Sys_error s | Scanf.Scan_failure s
+  | Failure s | Invalid_argument s ->
+     Pp.(msg_error (str"Error loading file "++str aux_fname++str" : "++str s));
+     empty_aux_file
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
new file mode 100644
index 000000000..b24515c99
--- /dev/null
+++ b/lib/aux_file.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type aux_file
+
+val load_aux_file_for : string -> aux_file
+val get : aux_file -> Loc.t -> string -> string
+val empty_aux_file : aux_file
+
+val start_aux_file_for : string -> unit
+val stop_aux_file : unit -> unit 
+val recording : unit -> bool
+
+val record_in_aux_at : Loc.t -> string -> string -> unit
+val record_in_aux : string -> string -> unit
+val record_in_aux_set_at : Loc.t -> unit
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 833182bce..d36fba36c 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -28,3 +28,4 @@ Serialize
 Xml_utils
 CUnix
 Envars
+Aux_file