--- a/src/HOL/Word/Bool_List_Representation.thy Thu Mar 24 15:56:47 2016 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Thu Mar 24 15:56:54 2016 +0100
@@ -329,13 +329,15 @@
apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+
done
-lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
- apply (unfold bl_to_bin_def)
- apply (rule xtrans(1))
- prefer 2
- apply (rule bl_to_bin_lt2p_aux)
- apply simp
- done
+lemma bl_to_bin_lt2p_drop:
+ "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
+proof (induct bs)
+ case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
+ show ?case unfolding bl_to_bin_def by simp
+qed simp
+
+lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
+ by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
lemma bl_to_bin_ge2p_aux:
"bl_to_bin_aux bs w >= w * (2 ^ length bs)"
--- a/src/Pure/General/file.scala Thu Mar 24 15:56:47 2016 +0100
+++ b/src/Pure/General/file.scala Thu Mar 24 15:56:54 2016 +0100
@@ -10,7 +10,8 @@
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
InputStreamReader, File => JFile, IOException}
-import java.nio.file.{StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
+ Files, SimpleFileVisitor, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, URLDecoder, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
@@ -238,6 +239,15 @@
}
+ /* append */
+
+ def append(file: JFile, text: CharSequence): Unit =
+ Files.write(file.toPath, UTF8.bytes(text.toString),
+ StandardOpenOption.APPEND, StandardOpenOption.CREATE)
+
+ def append(path: Path, text: CharSequence): Unit = append(path.file, text)
+
+
/* copy */
def eq(file1: JFile, file2: JFile): Boolean =
@@ -254,14 +264,4 @@
}
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
-
-
- /* approximative time stamp */
-
- def time_stamp(path: Path): Option[String] =
- {
- val file = path.file
- if (file.isFile) Some(file.length.toString + " " + file.lastModified.toString)
- else None
- }
}
--- a/src/Pure/General/sha1.ML Thu Mar 24 15:56:47 2016 +0100
+++ b/src/Pure/General/sha1.ML Thu Mar 24 15:56:54 2016 +0100
@@ -8,9 +8,9 @@
signature SHA1 =
sig
eqtype digest
- val digest: string -> digest
val rep: digest -> string
val fake: string -> digest
+ val digest: string -> digest
val test_samples: unit -> unit
end;
--- a/src/Pure/General/sha1.scala Thu Mar 24 15:56:47 2016 +0100
+++ b/src/Pure/General/sha1.scala Thu Mar 24 15:56:54 2016 +0100
@@ -36,6 +36,8 @@
new Digest(result.toString)
}
+ def fake(rep: String): Digest = new Digest(rep)
+
def digest(file: JFile): Digest =
{
val stream = new FileInputStream(file)
@@ -54,6 +56,8 @@
make_result(digest)
}
+ def digest(path: Path): Digest = digest(path.file)
+
def digest(bytes: Array[Byte]): Digest =
{
val digest = MessageDigest.getInstance("SHA")
@@ -63,9 +67,7 @@
}
def digest(bytes: Bytes): Digest = bytes.sha1_digest
-
def digest(string: String): Digest = digest(Bytes(string))
- def fake(rep: String): Digest = new Digest(rep)
+ val digest_length: Int = digest("").rep.length
}
-
--- a/src/Pure/Thy/sessions.scala Thu Mar 24 15:56:47 2016 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Mar 24 15:56:54 2016 +0100
@@ -6,6 +6,9 @@
package isabelle
+import java.nio.ByteBuffer
+import java.nio.channels.FileChannel
+import java.nio.file.StandardOpenOption
import scala.collection.SortedSet
import scala.collection.mutable
@@ -319,6 +322,54 @@
+ /** heap file with SHA1 digest **/
+
+ private val sha1_prefix = "SHA1:"
+
+ def read_heap_digest(heap: Path): Option[String] =
+ {
+ if (heap.is_file) {
+ val file = FileChannel.open(heap.file.toPath, StandardOpenOption.READ)
+ try {
+ val len = file.size
+ val n = sha1_prefix.length + SHA1.digest_length
+ if (len >= n) {
+ file.position(len - n)
+
+ val buf = ByteBuffer.allocate(n)
+ var i = 0
+ var m = 0
+ do {
+ m = file.read(buf)
+ if (m != -1) i += m
+ }
+ while (m != -1 && n > i)
+
+ if (i == n) {
+ val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
+ val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
+ if (prefix == sha1_prefix) Some(s) else None
+ }
+ else None
+ }
+ else None
+ }
+ finally { file.close }
+ }
+ else None
+ }
+
+ def write_heap_digest(heap: Path): String =
+ read_heap_digest(heap) match {
+ case None =>
+ val s = SHA1.digest(heap).rep
+ File.append(heap, sha1_prefix + s)
+ s
+ case Some(s) => s
+ }
+
+
+
/** persistent store **/
def log(name: String): Path = Path.basic("log") + Path.basic(name)
@@ -352,7 +403,7 @@
def find(name: String): Option[(Path, Option[String])] =
input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
- (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
+ (dir + log_gz(name), read_heap_digest(dir + Path.basic(name))))
def find_log(name: String): Option[Path] =
input_dirs.map(_ + log(name)).find(_.is_file)
--- a/src/Pure/Tools/build.scala Thu Mar 24 15:56:47 2016 +0100
+++ b/src/Pure/Tools/build.scala Thu Mar 24 15:56:54 2016 +0100
@@ -560,8 +560,8 @@
if (process_result.ok) {
(store.output_dir + Sessions.log(name)).file.delete
val heap_stamp =
- for (path <- job.output_path; stamp <- File.time_stamp(path))
- yield stamp
+ for (path <- job.output_path if path.is_file)
+ yield Sessions.write_heap_digest(path)
File.write_gzip(store.output_dir + Sessions.log_gz(name),
Library.terminate_lines(