# HG changeset patch # User boehmes # Date 1269415363 -3600 # Node ID 63f0d628edffa4f4963c846b7865247b1706329a # Parent a336af707767880e088eac6df7503f2d6e77a064 remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation) diff -r a336af707767 -r 63f0d628edff src/Tools/Cache_IO/cache_io.ML --- a/src/Tools/Cache_IO/cache_io.ML Tue Mar 23 19:03:05 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ -(* Title: Tools/Cache_IO/cache_io.ML - Author: Sascha Boehme, TU Muenchen - -Cache for output of external processes. -*) - -signature CACHE_IO = -sig - val with_tmp_file: string -> (Path.T -> 'a) -> 'a - val run: (Path.T -> string) -> Path.T -> string list - val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list - - type cache - val make: Path.T -> cache - val cache_path_of: cache -> Path.T - val cached: cache -> (Path.T -> string) -> Path.T -> string list - val cached': cache -> (Path.T -> Path.T -> string) -> Path.T -> - string list * string list -end - -structure Cache_IO : CACHE_IO = -struct - -fun with_tmp_file name f = - let - val path = File.tmp_path (Path.explode (name ^ serial_string ())) - val x = Exn.capture f path - val _ = try File.rm path - in Exn.release x end - -fun run' make_cmd in_path = - with_tmp_file "cache-io-" (fn out_path => - let - val (out2, _) = bash_output (make_cmd in_path out_path) - val out1 = the_default [] (try (rev o File.fold_lines cons out_path) []) - in (out1, split_lines out2) end) - -fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path) - - - -abstype cache = Cache of { - path: Path.T, - table: (int * (int * int * int) Symtab.table) Synchronized.var } -with - - -fun cache_path_of (Cache {path, ...}) = path - - -fun load cache_path = - let - fun err () = error ("Cache IO: corrupted cache file: " ^ - File.shell_path cache_path) - - fun int_of_string s = - (case read_int (explode s) of - (i, []) => i - | _ => err ()) - - fun split line = - (case space_explode " " line of - [key, len1, len2] => (key, int_of_string len1, int_of_string len2) - | _ => err ()) - - fun parse line ((i, l), tab) = - if i = l - then - let val (key, l1, l2) = split line - in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end - else ((i+1, l), tab) - in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end - -fun make path = - let val table = if File.exists path then load path else (1, Symtab.empty) - in Cache {path=path, table=Synchronized.var (Path.implode path) table} end - - -fun get_hash_key path = - let - val arg = File.shell_path path - val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg) - in - if res = 0 then hd (split_lines out) - else error ("Cache IO: failed to generate hash key for file " ^ arg) - end - -fun load_cached_result cache_path (p, len1, len2) = - let - fun load line (i, xsp) = - if i < p then (i+1, xsp) - else if i < p + len1 then (i+1, apfst (cons line) xsp) - else if i < p + len2 then (i+1, apsnd (cons line) xsp) - else (i, xsp) - in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end - -fun cached' (Cache {path=cache_path, table}) make_cmd in_path = - let val key = get_hash_key in_path - in - (case Symtab.lookup (snd (Synchronized.value table)) key of - SOME pos => load_cached_result cache_path pos - | NONE => - let - val res as (out, err) = run' make_cmd in_path - val (l1, l2) = pairself length res - val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 - val lines = map (suffix "\n") (header :: out @ err) - - val _ = Synchronized.change table (fn (p, tab) => - if Symtab.defined tab key then (p, tab) - else - let val _ = File.append_list cache_path lines - in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end) - in res end) - end - -fun cached cache make_cmd = - snd o cached' cache (fn in_path => fn _ => make_cmd in_path) - -end -end diff -r a336af707767 -r 63f0d628edff src/Tools/Cache_IO/etc/settings --- a/src/Tools/Cache_IO/etc/settings Tue Mar 23 19:03:05 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -ISABELLE_CACHE_IO="$COMPONENT" - -COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key" - diff -r a336af707767 -r 63f0d628edff src/Tools/Cache_IO/lib/scripts/compute_hash_key --- a/src/Tools/Cache_IO/lib/scripts/compute_hash_key Tue Mar 23 19:03:05 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -#!/usr/bin/env perl -# -# Author: Sascha Boehme, TU Muenchen -# -# Compute MD5 hash key. - -use strict; -use warnings; -use Digest::MD5; - - -# argument - -my $file = $ARGV[0]; - - -# compute MD5 hash key - -my $md5 = Digest::MD5->new; -open FILE, "<$file" or die "ERROR: Failed to open '$file' ($!)"; -$md5->addfile(*FILE); -close FILE; -print $md5->b64digest . "\n"; - diff -r a336af707767 -r 63f0d628edff src/Tools/cache_io.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/cache_io.ML Wed Mar 24 08:22:43 2010 +0100 @@ -0,0 +1,121 @@ +(* Title: Tools/Cache_IO/cache_io.ML + Author: Sascha Boehme, TU Muenchen + +Cache for output of external processes. +*) + +signature CACHE_IO = +sig + val with_tmp_file: string -> (Path.T -> 'a) -> 'a + val run: (Path.T -> string) -> Path.T -> string list + val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list + + type cache + val make: Path.T -> cache + val cache_path_of: cache -> Path.T + val cached: cache -> (Path.T -> string) -> Path.T -> string list + val cached': cache -> (Path.T -> Path.T -> string) -> Path.T -> + string list * string list +end + +structure Cache_IO : CACHE_IO = +struct + +fun with_tmp_file name f = + let + val path = File.tmp_path (Path.explode (name ^ serial_string ())) + val x = Exn.capture f path + val _ = try File.rm path + in Exn.release x end + +fun run' make_cmd in_path = + with_tmp_file "cache-io-" (fn out_path => + let + val (out2, _) = bash_output (make_cmd in_path out_path) + val out1 = the_default [] (try (rev o File.fold_lines cons out_path) []) + in (out1, split_lines out2) end) + +fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path) + + + +abstype cache = Cache of { + path: Path.T, + table: (int * (int * int * int) Symtab.table) Synchronized.var } +with + + +fun cache_path_of (Cache {path, ...}) = path + + +fun load cache_path = + let + fun err () = error ("Cache IO: corrupted cache file: " ^ + File.shell_path cache_path) + + fun int_of_string s = + (case read_int (explode s) of + (i, []) => i + | _ => err ()) + + fun split line = + (case space_explode " " line of + [key, len1, len2] => (key, int_of_string len1, int_of_string len2) + | _ => err ()) + + fun parse line ((i, l), tab) = + if i = l + then + let val (key, l1, l2) = split line + in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end + else ((i+1, l), tab) + in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end + +fun make path = + let val table = if File.exists path then load path else (1, Symtab.empty) + in Cache {path=path, table=Synchronized.var (Path.implode path) table} end + + +fun get_hash_key path = + let + val arg = File.shell_path path + val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg) + in + if res = 0 then hd (split_lines out) + else error ("Cache IO: failed to generate hash key for file " ^ arg) + end + +fun load_cached_result cache_path (p, len1, len2) = + let + fun load line (i, xsp) = + if i < p then (i+1, xsp) + else if i < p + len1 then (i+1, apfst (cons line) xsp) + else if i < p + len2 then (i+1, apsnd (cons line) xsp) + else (i, xsp) + in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end + +fun cached' (Cache {path=cache_path, table}) make_cmd in_path = + let val key = get_hash_key in_path + in + (case Symtab.lookup (snd (Synchronized.value table)) key of + SOME pos => load_cached_result cache_path pos + | NONE => + let + val res as (out, err) = run' make_cmd in_path + val (l1, l2) = pairself length res + val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 + val lines = map (suffix "\n") (header :: out @ err) + + val _ = Synchronized.change table (fn (p, tab) => + if Symtab.defined tab key then (p, tab) + else + let val _ = File.append_list cache_path lines + in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end) + in res end) + end + +fun cached cache make_cmd = + snd o cached' cache (fn in_path => fn _ => make_cmd in_path) + +end +end