# HG changeset patch # User wenzelm # Date 1300046160 -3600 # Node ID 703ea96b13c674f2c058ece1876053ad6ac79264 # Parent fb94df4505a069f05b93278d55c0dfb0ddcea60e files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT; diff -r fb94df4505a0 -r 703ea96b13c6 NEWS --- 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. diff -r fb94df4505a0 -r 703ea96b13c6 doc-src/System/Thy/Basics.thy --- 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 diff -r fb94df4505a0 -r 703ea96b13c6 doc-src/System/Thy/document/Basics.tex --- 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}). diff -r fb94df4505a0 -r 703ea96b13c6 etc/settings --- 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) diff -r fb94df4505a0 -r 703ea96b13c6 lib/scripts/fileident --- 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 diff -r fb94df4505a0 -r 703ea96b13c6 src/Pure/Thy/thy_info.ML --- 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}; diff -r fb94df4505a0 -r 703ea96b13c6 src/Pure/Thy/thy_load.ML --- 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 = diff -r fb94df4505a0 -r 703ea96b13c6 src/Pure/pure_setup.ML --- 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 \"\")"; toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";