--- a/NEWS Sun Mar 13 20:21:24 2011 +0100
+++ b/NEWS Sun Mar 13 20:56:00 2011 +0100
@@ -6,6 +6,10 @@
*** General ***
+* Theory loader: source files are identified by content via SHA1
+digests. Discontinued former path/modtime identification and optional
+ISABELLE_FILE_IDENT plugin scripts.
+
* Parallelization of nested Isar proofs is subject to
Goal.parallel_proofs_threshold (default 100). See also isabelle
usedir option -Q.
--- a/doc-src/System/Thy/Basics.thy Sun Mar 13 20:21:24 2011 +0100
+++ b/doc-src/System/Thy/Basics.thy Sun Mar 13 20:56:00 2011 +0100
@@ -228,13 +228,6 @@
usedir} is the basic utility for managing logic sessions (cf.\ the
@{verbatim IsaMakefile}s in the distribution).
- \item[@{setting_def ISABELLE_FILE_IDENT}] specifies a shell command
- for producing a source file identification, based on the actual
- content instead of the full physical path and date stamp (which is
- the default). A typical identification would produce a ``digest'' of
- the text, using a cryptographic hash function like SHA-1, for
- example.
-
\item[@{setting_def ISABELLE_LATEX}, @{setting_def
ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
--- a/doc-src/System/Thy/document/Basics.tex Sun Mar 13 20:21:24 2011 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Sun Mar 13 20:56:00 2011 +0100
@@ -236,13 +236,6 @@
typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the
\verb|IsaMakefile|s in the distribution).
- \item[\indexdef{}{setting}{ISABELLE\_FILE\_IDENT}\hypertarget{setting.ISABELLE-FILE-IDENT}{\hyperlink{setting.ISABELLE-FILE-IDENT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}FILE{\isaliteral{5F}{\isacharunderscore}}IDENT}}}}}] specifies a shell command
- for producing a source file identification, based on the actual
- content instead of the full physical path and date stamp (which is
- the default). A typical identification would produce a ``digest'' of
- the text, using a cryptographic hash function like SHA-1, for
- example.
-
\item[\indexdef{}{setting}{ISABELLE\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DVIPS}}}}}] refer to {\LaTeX} related tools for Isabelle
document preparation (see also \secref{sec:tool-latex}).
--- a/etc/settings Sun Mar 13 20:21:24 2011 +0100
+++ b/etc/settings Sun Mar 13 20:56:00 2011 +0100
@@ -80,13 +80,6 @@
ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
-#Source file identification (default: full name + date stamp)
-ISABELLE_FILE_IDENT=""
-#ISABELLE_FILE_IDENT="md5"
-#ISABELLE_FILE_IDENT="md5sum"
-#ISABELLE_FILE_IDENT="sha1sum"
-#ISABELLE_FILE_IDENT="openssl dgst -sha1"
-
###
### Document preparation (cf. isabelle latex/document)
--- a/lib/scripts/fileident Sun Mar 13 20:21:24 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-#
-# fileident --- produce file identification based
-
-FILE="$1"
-
-if [ -n "$ISABELLE_FILE_IDENT" -a -f "$FILE" -a -r "$FILE" ]
-then
- ID=$(cat "$FILE" | $ISABELLE_FILE_IDENT | cut -d " " -f 1) && echo -n "$ID"
-fi
--- a/src/Pure/Thy/thy_info.ML Sun Mar 13 20:21:24 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Mar 13 20:56:00 2011 +0100
@@ -65,7 +65,7 @@
(* thy database *)
type deps =
- {master: (Path.T * Thy_Load.file_ident), (*master dependencies for thy file*)
+ {master: (Path.T * SHA1.digest), (*master dependencies for thy file*)
imports: string list}; (*source specification of imports (partially qualified)*)
fun make_deps master imports : deps = {master = master, imports = imports};
--- a/src/Pure/Thy/thy_load.ML Sun Mar 13 20:21:24 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML Sun Mar 13 20:56:00 2011 +0100
@@ -7,18 +7,15 @@
signature THY_LOAD =
sig
- eqtype file_ident
- val pretty_file_ident: file_ident -> Pretty.T
- val file_ident: Path.T -> file_ident option
val set_master_path: Path.T -> unit
val get_master_path: unit -> Path.T
val master_directory: theory -> Path.T
val imports_of: theory -> string list
- val provide: Path.T * (Path.T * file_ident) -> theory -> theory
- val check_file: Path.T -> Path.T -> Path.T * file_ident
- val check_thy: Path.T -> string -> Path.T * file_ident
+ val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
+ val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
+ val check_thy: Path.T -> string -> Path.T * SHA1.digest
val deps_thy: Path.T -> string ->
- {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
+ {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
val loaded_files: theory -> Path.T list
val all_current: theory -> bool
val provide_file: Path.T -> theory -> theory
@@ -30,58 +27,13 @@
structure Thy_Load: THY_LOAD =
struct
-(* file identification *)
-
-local
- val file_ident_cache =
- Synchronized.var "file_ident_cache"
- (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
-in
-
-fun check_cache (path, time) =
- (case Symtab.lookup (Synchronized.value file_ident_cache) path of
- NONE => NONE
- | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
-
-fun update_cache (path, (time, id)) =
- Synchronized.change file_ident_cache
- (Symtab.update (path, {time_stamp = time, id = id}));
-
-end;
-
-datatype file_ident = File_Ident of string;
-
-fun pretty_file_ident (File_Ident s) = Pretty.str (quote s);
-
-fun file_ident path =
- let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in
- (case try (Time.toString o OS.FileSys.modTime) physical_path of
- NONE => NONE
- | SOME mod_time => SOME (File_Ident
- (case getenv "ISABELLE_FILE_IDENT" of
- "" => physical_path ^ ": " ^ mod_time
- | cmd =>
- (case check_cache (physical_path, mod_time) of
- SOME id => id
- | NONE =>
- let
- val (id, rc) = (*potentially slow*)
- bash_output
- ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path);
- in
- if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
- else error ("Failed to identify file " ^ Path.print path ^ " by " ^ cmd)
- end))))
- end;
-
-
(* manage source files *)
type files =
{master_dir: Path.T, (*master directory of theory source*)
imports: string list, (*source specification of imports*)
required: Path.T list, (*source path*)
- provided: (Path.T * (Path.T * file_ident)) list}; (*source path, physical path, identifier*)
+ provided: (Path.T * (Path.T * SHA1.digest)) list}; (*source path, physical path, digest*)
fun make_files (master_dir, imports, required, provided): files =
{master_dir = master_dir, imports = imports, required = required, provided = provided};
@@ -137,9 +89,9 @@
val _ = Path.is_current path andalso error "Bad file specification";
val full_path = File.full_path (Path.append dir path);
in
- (case file_ident full_path of
- NONE => NONE
- | SOME id => SOME (full_path, id))
+ if File.exists full_path
+ then SOME (full_path, SHA1.digest (File.read full_path))
+ else NONE
end;
fun check_file dir file =
--- a/src/Pure/pure_setup.ML Sun Mar 13 20:21:24 2011 +0100
+++ b/src/Pure/pure_setup.ML Sun Mar 13 20:56:00 2011 +0100
@@ -33,7 +33,6 @@
toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
-toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";