merged
authorwenzelm
Wed Nov 14 22:13:57 2018 +0100 (3 weeks ago)
changeset 69306341ebf35464b
parent 69298 360bde07daf9
parent 69305 5a71b5145201
child 69307 196347d2fd2d
merged
     1.1 --- a/src/Pure/Admin/build_history.scala	Wed Nov 14 14:25:57 2018 -0500
     1.2 +++ b/src/Pure/Admin/build_history.scala	Wed Nov 14 22:13:57 2018 +0100
     1.3 @@ -114,6 +114,7 @@
     1.4      ml_statistics_step: Int = 1,
     1.5      components_base: String = "",
     1.6      fresh: Boolean = false,
     1.7 +    hostname: String = "",
     1.8      nonfree: Boolean = false,
     1.9      multicore_base: Boolean = false,
    1.10      multicore_list: List[(Int, Int)] = List(default_multicore),
    1.11 @@ -176,7 +177,7 @@
    1.12        Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
    1.13          user_home = user_home, progress = progress)
    1.14  
    1.15 -    val build_host = Isabelle_System.hostname()
    1.16 +    val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
    1.17      val build_history_date = Date.now()
    1.18      val build_group_id = build_host + ":" + build_history_date.time.ms
    1.19  
    1.20 @@ -402,6 +403,7 @@
    1.21        var afp_partition = 0
    1.22        var more_settings: List[String] = Nil
    1.23        var fresh = false
    1.24 +      var hostname = ""
    1.25        var init_settings: List[String] = Nil
    1.26        var arch_64 = false
    1.27        var nonfree = false
    1.28 @@ -428,6 +430,7 @@
    1.29      -U SIZE      maximal ML heap in MB (default: unbounded)
    1.30      -e TEXT      additional text for generated etc/settings
    1.31      -f           fresh build of Isabelle/Scala components (recommended)
    1.32 +    -h NAME      override local hostname
    1.33      -i TEXT      initial text for generated etc/settings
    1.34      -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
    1.35      -n           include nonfree components
    1.36 @@ -455,6 +458,7 @@
    1.37          "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
    1.38          "e:" -> (arg => more_settings = more_settings ::: List(arg)),
    1.39          "f" -> (_ => fresh = true),
    1.40 +        "h:" -> (arg => hostname = arg),
    1.41          "i:" -> (arg => init_settings = init_settings ::: List(arg)),
    1.42          "m:" ->
    1.43            {
    1.44 @@ -484,7 +488,7 @@
    1.45          build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
    1.46            afp_rev = afp_rev, afp_partition = afp_partition,
    1.47            isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
    1.48 -          components_base = components_base, fresh = fresh, nonfree = nonfree,
    1.49 +          components_base = components_base, fresh = fresh, hostname = hostname, nonfree = nonfree,
    1.50            multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
    1.51            heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
    1.52            max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
     2.1 --- a/src/Pure/Admin/build_log.scala	Wed Nov 14 14:25:57 2018 -0500
     2.2 +++ b/src/Pure/Admin/build_log.scala	Wed Nov 14 22:13:57 2018 +0100
     2.3 @@ -146,9 +146,6 @@
     2.4        name != "main.log"
     2.5      }
     2.6  
     2.7 -    def find_files(dirs: Iterable[Path]): List[JFile] =
     2.8 -      dirs.iterator.flatMap(dir => File.find_files(dir.file, is_log(_))).toList
     2.9 -
    2.10  
    2.11      /* date format */
    2.12  
    2.13 @@ -904,7 +901,10 @@
    2.14  
    2.15      def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
    2.16      {
    2.17 -      write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
    2.18 +      val log_files =
    2.19 +        dirs.flatMap(dir =>
    2.20 +          File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
    2.21 +      write_info(db, log_files, ml_statistics = ml_statistics)
    2.22  
    2.23        db.create_view(Data.pull_date_table())
    2.24        db.create_view(Data.pull_date_table(afp = true))
     3.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Nov 14 14:25:57 2018 -0500
     3.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Nov 14 22:13:57 2018 +0100
     3.3 @@ -350,7 +350,7 @@
     3.4                  afp_rev = afp_rev,
     3.5                  options =
     3.6                    " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
     3.7 -                  " -f " + r.options,
     3.8 +                  " -f -h " + Bash.string(r.host) + " " + r.options,
     3.9                  args = "-o timeout=10800 " + r.args)
    3.10  
    3.11              for ((log_name, bytes) <- results) {
     4.1 --- a/src/Pure/General/file.ML	Wed Nov 14 14:25:57 2018 -0500
     4.2 +++ b/src/Pure/General/file.ML	Wed Nov 14 22:13:57 2018 +0100
     4.3 @@ -15,6 +15,7 @@
     4.4    val exists: Path.T -> bool
     4.5    val rm: Path.T -> unit
     4.6    val is_dir: Path.T -> bool
     4.7 +  val is_file: Path.T -> bool
     4.8    val check_dir: Path.T -> Path.T
     4.9    val check_file: Path.T -> Path.T
    4.10    val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
    4.11 @@ -74,15 +75,16 @@
    4.12  
    4.13  val rm = OS.FileSys.remove o platform_path;
    4.14  
    4.15 -fun is_dir path =
    4.16 -  the_default false (try OS.FileSys.isDir (platform_path path));
    4.17 +fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path));
    4.18 +fun is_dir path = exists path andalso test_dir path;
    4.19 +fun is_file path = exists path andalso not (test_dir path);
    4.20  
    4.21  fun check_dir path =
    4.22 -  if exists path andalso is_dir path then path
    4.23 +  if is_dir path then path
    4.24    else error ("No such directory: " ^ Path.print (Path.expand path));
    4.25  
    4.26  fun check_file path =
    4.27 -  if exists path andalso not (is_dir path) then path
    4.28 +  if is_file path then path
    4.29    else error ("No such file: " ^ Path.print (Path.expand path));
    4.30  
    4.31  
    4.32 @@ -106,13 +108,14 @@
    4.33  
    4.34  (* directory content *)
    4.35  
    4.36 -fun fold_dir f path a = open_dir (fn stream =>
    4.37 -  let
    4.38 -    fun read x =
    4.39 -      (case OS.FileSys.readDir stream of
    4.40 -        NONE => x
    4.41 -      | SOME entry => read (f entry x));
    4.42 -  in read a end) path;
    4.43 +fun fold_dir f path a =
    4.44 +  check_dir path |> open_dir (fn stream =>
    4.45 +    let
    4.46 +      fun read x =
    4.47 +        (case OS.FileSys.readDir stream of
    4.48 +          NONE => x
    4.49 +        | SOME entry => read (f entry x));
    4.50 +    in read a end);
    4.51  
    4.52  fun read_dir path = rev (fold_dir cons path []);
    4.53  
     5.1 --- a/src/Pure/General/file.scala	Wed Nov 14 14:25:57 2018 -0500
     5.2 +++ b/src/Pure/General/file.scala	Wed Nov 14 22:13:57 2018 +0100
     5.3 @@ -141,7 +141,7 @@
     5.4  
     5.5    def read_dir(dir: Path): List[String] =
     5.6    {
     5.7 -    if (!dir.is_dir) error("Bad directory: " + dir.toString)
     5.8 +    if (!dir.is_dir) error("No such directory: " + dir.toString)
     5.9      val files = dir.file.listFiles
    5.10      if (files == null) Nil
    5.11      else files.toList.map(_.getName)
    5.12 @@ -151,7 +151,7 @@
    5.13      start: JFile,
    5.14      pred: JFile => Boolean = _ => true,
    5.15      include_dirs: Boolean = false,
    5.16 -    follow_links: Boolean = true): List[JFile] =
    5.17 +    follow_links: Boolean = false): List[JFile] =
    5.18    {
    5.19      val result = new mutable.ListBuffer[JFile]
    5.20      def check(file: JFile) { if (pred(file)) result += file }
    5.21 @@ -170,7 +170,8 @@
    5.22            }
    5.23            override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
    5.24            {
    5.25 -            check(path.toFile)
    5.26 +            val file = path.toFile
    5.27 +            if (include_dirs || !file.isDirectory) check(file)
    5.28              FileVisitResult.CONTINUE
    5.29            }
    5.30          }
     6.1 --- a/src/Pure/General/http.scala	Wed Nov 14 14:25:57 2018 -0500
     6.2 +++ b/src/Pure/General/http.scala	Wed Nov 14 22:13:57 2018 +0100
     6.3 @@ -45,13 +45,18 @@
     6.4      def request_uri: URI = http_exchange.getRequestURI
     6.5  
     6.6      def read_request(): Bytes =
     6.7 -      using(http_exchange.getRequestBody)(Bytes.read_stream(_))
     6.8 +    {
     6.9 +      val stream = http_exchange.getRequestBody
    6.10 +      try { Bytes.read_stream(stream) } finally { stream.close }
    6.11 +    }
    6.12  
    6.13      def write_response(code: Int, response: Response)
    6.14      {
    6.15        http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
    6.16        http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
    6.17 -      using(http_exchange.getResponseBody)(response.bytes.write_stream(_))
    6.18 +
    6.19 +      val stream = http_exchange.getResponseBody
    6.20 +      try { response.bytes.write_stream(stream) } finally { stream.close }
    6.21      }
    6.22    }
    6.23  
     7.1 --- a/src/Pure/General/ssh.scala	Wed Nov 14 14:25:57 2018 -0500
     7.2 +++ b/src/Pure/General/ssh.scala	Wed Nov 14 22:13:57 2018 +0100
     7.3 @@ -201,10 +201,9 @@
     7.4  
     7.5    type Attrs = SftpATTRS
     7.6  
     7.7 -  sealed case class Dir_Entry(name: Path, attrs: Attrs)
     7.8 +  sealed case class Dir_Entry(name: String, is_dir: Boolean)
     7.9    {
    7.10 -    def is_file: Boolean = attrs.isReg
    7.11 -    def is_dir: Boolean = attrs.isDir
    7.12 +    def is_file: Boolean = !is_dir
    7.13    }
    7.14  
    7.15  
    7.16 @@ -341,12 +340,19 @@
    7.17      def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
    7.18      def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
    7.19  
    7.20 -    def stat(path: Path): Option[Dir_Entry] =
    7.21 -      try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
    7.22 -      catch { case _: SftpException => None }
    7.23 +    private def test_entry(path: Path, as_dir: Boolean): Boolean =
    7.24 +      try {
    7.25 +        val is_dir = sftp.stat(remote_path(path)).isDir
    7.26 +        if (as_dir) is_dir else !is_dir
    7.27 +      }
    7.28 +      catch { case _: SftpException => false }
    7.29  
    7.30 -    override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
    7.31 -    override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
    7.32 +    override def is_dir(path: Path): Boolean = test_entry(path, true)
    7.33 +    override def is_file(path: Path): Boolean = test_entry(path, false)
    7.34 +
    7.35 +    def is_link(path: Path): Boolean =
    7.36 +      try { sftp.lstat(remote_path(path)).isLink }
    7.37 +      catch { case _: SftpException => false }
    7.38  
    7.39      override def mkdirs(path: Path): Unit =
    7.40        if (!is_dir(path)) {
    7.41 @@ -357,27 +363,49 @@
    7.42  
    7.43      def read_dir(path: Path): List[Dir_Entry] =
    7.44      {
    7.45 -      val dir = sftp.ls(remote_path(path))
    7.46 +      if (!is_dir(path)) error("No such directory: " + path.toString)
    7.47 +
    7.48 +      val dir_name = remote_path(path)
    7.49 +      val dir = sftp.ls(dir_name)
    7.50        (for {
    7.51          i <- (0 until dir.size).iterator
    7.52          a = dir.get(i).asInstanceOf[AnyRef]
    7.53          name = Untyped.get[String](a, "filename")
    7.54          attrs = Untyped.get[Attrs](a, "attrs")
    7.55          if name != "." && name != ".."
    7.56 -      } yield Dir_Entry(Path.basic(name), attrs)).toList
    7.57 +      }
    7.58 +      yield {
    7.59 +        Dir_Entry(name,
    7.60 +          if (attrs.isLink) {
    7.61 +            try { sftp.stat(dir_name + "/" + name).isDir }
    7.62 +            catch { case _: SftpException => false }
    7.63 +          }
    7.64 +          else attrs.isDir)
    7.65 +      }).toList
    7.66      }
    7.67  
    7.68 -    def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
    7.69 +    def find_files(
    7.70 +      start: Path,
    7.71 +      pred: Path => Boolean = _ => true,
    7.72 +      include_dirs: Boolean = false,
    7.73 +      follow_links: Boolean = false): List[Path] =
    7.74      {
    7.75 -      def find(dir: Path): List[Dir_Entry] =
    7.76 -        read_dir(dir).flatMap(entry =>
    7.77 -          {
    7.78 -            val file = dir + entry.name
    7.79 -            if (entry.is_dir) find(file)
    7.80 -            else if (pred(entry)) List(entry.copy(name = file))
    7.81 -            else Nil
    7.82 -          })
    7.83 -      find(root)
    7.84 +      val result = new mutable.ListBuffer[Path]
    7.85 +      def check(path: Path) { if (pred(path)) result += path }
    7.86 +
    7.87 +      def find(dir: Path)
    7.88 +      {
    7.89 +        if (include_dirs) check(dir)
    7.90 +        if (follow_links || !is_link(dir)) {
    7.91 +          for (entry <- read_dir(dir)) {
    7.92 +            val path = dir + Path.basic(entry.name)
    7.93 +            if (entry.is_file) check(path) else find(path)
    7.94 +          }
    7.95 +        }
    7.96 +      }
    7.97 +      if (is_file(start)) check(start) else find(start)
    7.98 +
    7.99 +      result.toList
   7.100      }
   7.101  
   7.102      def open_input(path: Path): InputStream = sftp.get(remote_path(path))
   7.103 @@ -440,8 +468,8 @@
   7.104  
   7.105      def expand_path(path: Path): Path = path.expand
   7.106      def bash_path(path: Path): String = File.bash_path(path)
   7.107 +    def is_dir(path: Path): Boolean = path.is_dir
   7.108      def is_file(path: Path): Boolean = path.is_file
   7.109 -    def is_dir(path: Path): Boolean = path.is_dir
   7.110      def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
   7.111  
   7.112      def execute(command: String,