src/Pure/System/build.scala
changeset 48548 49afe0e92163
parent 48547 b3b092d0a9fe
child 48549 cc7990d6eb38
equal deleted inserted replaced
48547:b3b092d0a9fe 48548:49afe0e92163
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 import java.io.{File => JFile, BufferedInputStream, FileInputStream,
    10 import java.io.{BufferedInputStream, FileInputStream,
    11   BufferedReader, InputStreamReader, IOException}
    11   BufferedReader, InputStreamReader, IOException}
    12 import java.util.zip.GZIPInputStream
    12 import java.util.zip.GZIPInputStream
    13 
    13 
    14 import scala.collection.mutable
    14 import scala.collection.mutable
    15 import scala.annotation.tailrec
    15 import scala.annotation.tailrec
   136         rep(theories) ~
   136         rep(theories) ~
   137         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   137         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   138           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   138           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   139     }
   139     }
   140 
   140 
   141     def parse_entries(root: JFile): List[Session_Entry] =
   141     def parse_entries(root: Path): List[Session_Entry] =
   142     {
   142     {
   143       val toks = syntax.scan(File.read(root))
   143       val toks = syntax.scan(File.read(root))
   144       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
   144       parse_all(rep(session_entry), Token.reader(toks, root.implode)) match {
   145         case Success(result, _) => result
   145         case Success(result, _) => result
   146         case bad => error(bad.toString)
   146         case bad => error(bad.toString)
   147       }
   147       }
   148     }
   148     }
   149   }
   149   }
   154   private val ROOT = Path.explode("ROOT")
   154   private val ROOT = Path.explode("ROOT")
   155   private val SESSIONS = Path.explode("etc/sessions")
   155   private val SESSIONS = Path.explode("etc/sessions")
   156 
   156 
   157   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
   157   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
   158 
   158 
   159   private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
   159   private def sessions_root(options: Options, dir: Path, root: Path, queue: Session.Queue)
   160     : Session.Queue =
   160     : Session.Queue =
   161   {
   161   {
   162     (queue /: Parser.parse_entries(root))((queue1, entry) =>
   162     (queue /: Parser.parse_entries(root))((queue1, entry) =>
   163       try {
   163       try {
   164         if (entry.base_name == "") error("Bad session name")
   164         if (entry.base_name == "") error("Bad session name")
   200         queue1 + (full_name, info)
   200         queue1 + (full_name, info)
   201       }
   201       }
   202       catch {
   202       catch {
   203         case ERROR(msg) =>
   203         case ERROR(msg) =>
   204           error(msg + "\nThe error(s) above occurred in session entry " +
   204           error(msg + "\nThe error(s) above occurred in session entry " +
   205             quote(entry.base_name) + Position.str_of(Position.file(root)))
   205             quote(entry.base_name) + Position.str_of(root.position))
   206       })
   206       })
   207   }
   207   }
   208 
   208 
   209   private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
   209   private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
   210     : Session.Queue =
   210     : Session.Queue =
   211   {
   211   {
   212     val root = (dir + ROOT).file
   212     val root = dir + ROOT
   213     if (root.isFile) sessions_root(options, dir, root, queue)
   213     if (root.is_file) sessions_root(options, dir, root, queue)
   214     else if (strict) error("Bad session root file: " + quote(root.toString))
   214     else if (strict) error("Bad session root file: " + root.toString)
   215     else queue
   215     else queue
   216   }
   216   }
   217 
   217 
   218   private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
   218   private def sessions_catalog(options: Options, dir: Path, catalog: Path, queue: Session.Queue)
   219     : Session.Queue =
   219     : Session.Queue =
   220   {
   220   {
   221     val dirs =
   221     val dirs =
   222       split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
   222       split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
   223     (queue /: dirs)((queue1, dir1) =>
   223     (queue /: dirs)((queue1, dir1) =>
   224       try {
   224       try {
   225         val dir2 = dir + Path.explode(dir1)
   225         val dir2 = dir + Path.explode(dir1)
   226         if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
   226         if (dir2.is_dir) sessions_dir(options, true, dir2, queue1)
   227         else error("Bad session directory: " + dir2.toString)
   227         else error("Bad session directory: " + dir2.toString)
   228       }
   228       }
   229       catch {
   229       catch {
   230         case ERROR(msg) =>
   230         case ERROR(msg) =>
   231           error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
   231           error(msg + "\nThe error(s) above occurred in session catalog " + catalog.toString)
   232       })
   232       })
   233   }
   233   }
   234 
   234 
   235   def find_sessions(options: Options, more_dirs: List[Path],
   235   def find_sessions(options: Options, more_dirs: List[Path],
   236     all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
   236     all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
   238     var queue = Session.Queue.empty
   238     var queue = Session.Queue.empty
   239 
   239 
   240     for (dir <- Isabelle_System.components()) {
   240     for (dir <- Isabelle_System.components()) {
   241       queue = sessions_dir(options, false, dir, queue)
   241       queue = sessions_dir(options, false, dir, queue)
   242 
   242 
   243       val catalog = (dir + SESSIONS).file
   243       val catalog = dir + SESSIONS
   244       if (catalog.isFile)
   244       if (catalog.is_file) queue = sessions_catalog(options, dir, catalog, queue)
   245         queue = sessions_catalog(options, dir, catalog, queue)
       
   246     }
   245     }
   247 
   246 
   248     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
   247     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
   249 
   248 
   250     sessions.filter(name => !queue.isDefinedAt(name)) match {
   249     sessions.filter(name => !queue.isDefinedAt(name)) match {
   315       }))
   314       }))
   316 
   315 
   317 
   316 
   318   /* jobs */
   317   /* jobs */
   319 
   318 
   320   private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
   319   private class Job(dir: Path, env: Map[String, String], script: String, args: String,
   321     output: Path, do_output: Boolean)
   320     output: Path, do_output: Boolean)
   322   {
   321   {
   323     private val args_file = File.tmp_file("args")
   322     private val args_file = File.tmp_file("args")
   324     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   323     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   325     File.write(args_file, args)
   324     File.write(args_file, args)
   326 
   325 
   327     private val (thread, result) =
   326     private val (thread, result) =
   328       Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
   327       Simple_Thread.future("build") { Isabelle_System.bash_env(dir.file, env1, script) }
   329 
   328 
   330     def terminate: Unit = thread.interrupt
   329     def terminate: Unit = thread.interrupt
   331     def is_finished: Boolean = result.is_finished
   330     def is_finished: Boolean = result.is_finished
   332     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   331     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   333     def output_path: Option[Path] = if (do_output) Some(output) else None
   332     def output_path: Option[Path] = if (do_output) Some(output) else None
   335 
   334 
   336   private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
   335   private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
   337     options: Options, verbose: Boolean, browser_info: Path): Job =
   336     options: Options, verbose: Boolean, browser_info: Path): Job =
   338   {
   337   {
   339     // global browser info dir
   338     // global browser info dir
   340     if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
   339     if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   341     {
   340     {
   342       browser_info.file.mkdirs()
   341       browser_info.file.mkdirs()
   343       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   342       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   344         browser_info + Path.explode("isabelle.gif"))
   343         browser_info + Path.explode("isabelle.gif"))
   345       File.write(browser_info + Path.explode("index.html"),
   344       File.write(browser_info + Path.explode("index.html"),
   348         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   347         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   349     }
   348     }
   350 
   349 
   351     val parent = info.parent.getOrElse("")
   350     val parent = info.parent.getOrElse("")
   352 
   351 
   353     val cwd = info.dir.file
       
   354     val env =
   352     val env =
   355       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
   353       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
   356     val script =
   354     val script =
   357       if (is_pure(name)) {
   355       if (is_pure(name)) {
   358         if (do_output) "./build " + name + " \"$OUTPUT\""
   356         if (do_output) "./build " + name + " \"$OUTPUT\""
   388           pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   386           pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   389             pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   387             pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   390           (do_output, (options, (verbose, (browser_info, (parent,
   388           (do_output, (options, (verbose, (browser_info, (parent,
   391             (name, info.theories)))))))
   389             (name, info.theories)))))))
   392     }
   390     }
   393     new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
   391     new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output)
   394   }
   392   }
   395 
   393 
   396 
   394 
   397   /* log files and corresponding heaps */
   395   /* log files and corresponding heaps */
   398 
   396 
   506                 val output = output_dir + Path.basic(name)
   504                 val output = output_dir + Path.basic(name)
   507                 val do_output = build_heap || queue.is_inner(name)
   505                 val do_output = build_heap || queue.is_inner(name)
   508 
   506 
   509                 val current =
   507                 val current =
   510                 {
   508                 {
   511                   input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
   509                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   512                     case Some(dir) =>
   510                     case Some(dir) =>
   513                       check_stamps(dir, name) match {
   511                       check_stamps(dir, name) match {
   514                         case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
   512                         case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
   515                         case None => false
   513                         case None => false
   516                       }
   514                       }