--- a/src/Pure/Admin/build_history.scala Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/Admin/build_history.scala Wed Nov 14 22:13:57 2018 +0100
@@ -114,6 +114,7 @@
ml_statistics_step: Int = 1,
components_base: String = "",
fresh: Boolean = false,
+ hostname: String = "",
nonfree: Boolean = false,
multicore_base: Boolean = false,
multicore_list: List[(Int, Int)] = List(default_multicore),
@@ -176,7 +177,7 @@
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = progress)
- val build_host = Isabelle_System.hostname()
+ val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
val build_history_date = Date.now()
val build_group_id = build_host + ":" + build_history_date.time.ms
@@ -402,6 +403,7 @@
var afp_partition = 0
var more_settings: List[String] = Nil
var fresh = false
+ var hostname = ""
var init_settings: List[String] = Nil
var arch_64 = false
var nonfree = false
@@ -428,6 +430,7 @@
-U SIZE maximal ML heap in MB (default: unbounded)
-e TEXT additional text for generated etc/settings
-f fresh build of Isabelle/Scala components (recommended)
+ -h NAME override local hostname
-i TEXT initial text for generated etc/settings
-m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-n include nonfree components
@@ -455,6 +458,7 @@
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
"e:" -> (arg => more_settings = more_settings ::: List(arg)),
"f" -> (_ => fresh = true),
+ "h:" -> (arg => hostname = arg),
"i:" -> (arg => init_settings = init_settings ::: List(arg)),
"m:" ->
{
@@ -484,7 +488,7 @@
build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
afp_rev = afp_rev, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
- components_base = components_base, fresh = fresh, nonfree = nonfree,
+ components_base = components_base, fresh = fresh, hostname = hostname, nonfree = nonfree,
multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
--- a/src/Pure/Admin/build_log.scala Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/Admin/build_log.scala Wed Nov 14 22:13:57 2018 +0100
@@ -146,9 +146,6 @@
name != "main.log"
}
- def find_files(dirs: Iterable[Path]): List[JFile] =
- dirs.iterator.flatMap(dir => File.find_files(dir.file, is_log(_))).toList
-
/* date format */
@@ -904,7 +901,10 @@
def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
{
- write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
+ val log_files =
+ dirs.flatMap(dir =>
+ File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
+ write_info(db, log_files, ml_statistics = ml_statistics)
db.create_view(Data.pull_date_table())
db.create_view(Data.pull_date_table(afp = true))
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Nov 14 22:13:57 2018 +0100
@@ -350,7 +350,7 @@
afp_rev = afp_rev,
options =
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
- " -f " + r.options,
+ " -f -h " + Bash.string(r.host) + " " + r.options,
args = "-o timeout=10800 " + r.args)
for ((log_name, bytes) <- results) {
--- a/src/Pure/General/file.ML Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/General/file.ML Wed Nov 14 22:13:57 2018 +0100
@@ -15,6 +15,7 @@
val exists: Path.T -> bool
val rm: Path.T -> unit
val is_dir: Path.T -> bool
+ val is_file: Path.T -> bool
val check_dir: Path.T -> Path.T
val check_file: Path.T -> Path.T
val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
@@ -74,15 +75,16 @@
val rm = OS.FileSys.remove o platform_path;
-fun is_dir path =
- the_default false (try OS.FileSys.isDir (platform_path path));
+fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path));
+fun is_dir path = exists path andalso test_dir path;
+fun is_file path = exists path andalso not (test_dir path);
fun check_dir path =
- if exists path andalso is_dir path then path
+ if is_dir path then path
else error ("No such directory: " ^ Path.print (Path.expand path));
fun check_file path =
- if exists path andalso not (is_dir path) then path
+ if is_file path then path
else error ("No such file: " ^ Path.print (Path.expand path));
@@ -106,13 +108,14 @@
(* directory content *)
-fun fold_dir f path a = open_dir (fn stream =>
- let
- fun read x =
- (case OS.FileSys.readDir stream of
- NONE => x
- | SOME entry => read (f entry x));
- in read a end) path;
+fun fold_dir f path a =
+ check_dir path |> open_dir (fn stream =>
+ let
+ fun read x =
+ (case OS.FileSys.readDir stream of
+ NONE => x
+ | SOME entry => read (f entry x));
+ in read a end);
fun read_dir path = rev (fold_dir cons path []);
--- a/src/Pure/General/file.scala Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/General/file.scala Wed Nov 14 22:13:57 2018 +0100
@@ -141,7 +141,7 @@
def read_dir(dir: Path): List[String] =
{
- if (!dir.is_dir) error("Bad directory: " + dir.toString)
+ if (!dir.is_dir) error("No such directory: " + dir.toString)
val files = dir.file.listFiles
if (files == null) Nil
else files.toList.map(_.getName)
@@ -151,7 +151,7 @@
start: JFile,
pred: JFile => Boolean = _ => true,
include_dirs: Boolean = false,
- follow_links: Boolean = true): List[JFile] =
+ follow_links: Boolean = false): List[JFile] =
{
val result = new mutable.ListBuffer[JFile]
def check(file: JFile) { if (pred(file)) result += file }
@@ -170,7 +170,8 @@
}
override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
- check(path.toFile)
+ val file = path.toFile
+ if (include_dirs || !file.isDirectory) check(file)
FileVisitResult.CONTINUE
}
}
--- a/src/Pure/General/http.scala Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/General/http.scala Wed Nov 14 22:13:57 2018 +0100
@@ -45,13 +45,18 @@
def request_uri: URI = http_exchange.getRequestURI
def read_request(): Bytes =
- using(http_exchange.getRequestBody)(Bytes.read_stream(_))
+ {
+ val stream = http_exchange.getRequestBody
+ try { Bytes.read_stream(stream) } finally { stream.close }
+ }
def write_response(code: Int, response: Response)
{
http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
- using(http_exchange.getResponseBody)(response.bytes.write_stream(_))
+
+ val stream = http_exchange.getResponseBody
+ try { response.bytes.write_stream(stream) } finally { stream.close }
}
}
--- a/src/Pure/General/ssh.scala Wed Nov 14 14:25:57 2018 -0500
+++ b/src/Pure/General/ssh.scala Wed Nov 14 22:13:57 2018 +0100
@@ -201,10 +201,9 @@
type Attrs = SftpATTRS
- sealed case class Dir_Entry(name: Path, attrs: Attrs)
+ sealed case class Dir_Entry(name: String, is_dir: Boolean)
{
- def is_file: Boolean = attrs.isReg
- def is_dir: Boolean = attrs.isDir
+ def is_file: Boolean = !is_dir
}
@@ -341,12 +340,19 @@
def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
- def stat(path: Path): Option[Dir_Entry] =
- try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
- catch { case _: SftpException => None }
+ private def test_entry(path: Path, as_dir: Boolean): Boolean =
+ try {
+ val is_dir = sftp.stat(remote_path(path)).isDir
+ if (as_dir) is_dir else !is_dir
+ }
+ catch { case _: SftpException => false }
- override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
- override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
+ override def is_dir(path: Path): Boolean = test_entry(path, true)
+ override def is_file(path: Path): Boolean = test_entry(path, false)
+
+ def is_link(path: Path): Boolean =
+ try { sftp.lstat(remote_path(path)).isLink }
+ catch { case _: SftpException => false }
override def mkdirs(path: Path): Unit =
if (!is_dir(path)) {
@@ -357,27 +363,49 @@
def read_dir(path: Path): List[Dir_Entry] =
{
- val dir = sftp.ls(remote_path(path))
+ if (!is_dir(path)) error("No such directory: " + path.toString)
+
+ val dir_name = remote_path(path)
+ val dir = sftp.ls(dir_name)
(for {
i <- (0 until dir.size).iterator
a = dir.get(i).asInstanceOf[AnyRef]
name = Untyped.get[String](a, "filename")
attrs = Untyped.get[Attrs](a, "attrs")
if name != "." && name != ".."
- } yield Dir_Entry(Path.basic(name), attrs)).toList
+ }
+ yield {
+ Dir_Entry(name,
+ if (attrs.isLink) {
+ try { sftp.stat(dir_name + "/" + name).isDir }
+ catch { case _: SftpException => false }
+ }
+ else attrs.isDir)
+ }).toList
}
- def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
+ def find_files(
+ start: Path,
+ pred: Path => Boolean = _ => true,
+ include_dirs: Boolean = false,
+ follow_links: Boolean = false): List[Path] =
{
- def find(dir: Path): List[Dir_Entry] =
- read_dir(dir).flatMap(entry =>
- {
- val file = dir + entry.name
- if (entry.is_dir) find(file)
- else if (pred(entry)) List(entry.copy(name = file))
- else Nil
- })
- find(root)
+ val result = new mutable.ListBuffer[Path]
+ def check(path: Path) { if (pred(path)) result += path }
+
+ def find(dir: Path)
+ {
+ if (include_dirs) check(dir)
+ if (follow_links || !is_link(dir)) {
+ for (entry <- read_dir(dir)) {
+ val path = dir + Path.basic(entry.name)
+ if (entry.is_file) check(path) else find(path)
+ }
+ }
+ }
+ if (is_file(start)) check(start) else find(start)
+
+ result.toList
}
def open_input(path: Path): InputStream = sftp.get(remote_path(path))
@@ -440,8 +468,8 @@
def expand_path(path: Path): Path = path.expand
def bash_path(path: Path): String = File.bash_path(path)
+ def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
- def is_dir(path: Path): Boolean = path.is_dir
def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
def execute(command: String,