src/Pure/System/build.scala
changeset 48373 527e2bad7cca
parent 48370 d0fa3efec93b
child 48409 0d2114eb412a
equal deleted inserted replaced
48370:d0fa3efec93b 48373:527e2bad7cca
   196       })
   196       })
   197   }
   197   }
   198 
   198 
   199   private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
   199   private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
   200   {
   200   {
   201     val root = Isabelle_System.platform_file(dir + ROOT)
   201     val root = (dir + ROOT).file
   202     if (root.isFile) sessions_root(dir, root, queue)
   202     if (root.isFile) sessions_root(dir, root, queue)
   203     else if (strict) error("Bad session root file: " + quote(root.toString))
   203     else if (strict) error("Bad session root file: " + quote(root.toString))
   204     else queue
   204     else queue
   205   }
   205   }
   206 
   206 
   210       split_lines(Standard_System.read_file(catalog)).
   210       split_lines(Standard_System.read_file(catalog)).
   211         filterNot(line => line == "" || line.startsWith("#"))
   211         filterNot(line => line == "" || line.startsWith("#"))
   212     (queue /: dirs)((queue1, dir1) =>
   212     (queue /: dirs)((queue1, dir1) =>
   213       try {
   213       try {
   214         val dir2 = dir + Path.explode(dir1)
   214         val dir2 = dir + Path.explode(dir1)
   215         if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, queue1)
   215         if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
   216         else error("Bad session directory: " + dir2.toString)
   216         else error("Bad session directory: " + dir2.toString)
   217       }
   217       }
   218       catch {
   218       catch {
   219         case ERROR(msg) =>
   219         case ERROR(msg) =>
   220           error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
   220           error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
   226     var queue = Session.Queue.empty
   226     var queue = Session.Queue.empty
   227 
   227 
   228     for (dir <- Isabelle_System.components()) {
   228     for (dir <- Isabelle_System.components()) {
   229       queue = sessions_dir(false, dir, queue)
   229       queue = sessions_dir(false, dir, queue)
   230 
   230 
   231       val catalog = Isabelle_System.platform_file(dir + SESSIONS)
   231       val catalog = (dir + SESSIONS).file
   232       if (catalog.isFile)
   232       if (catalog.isFile)
   233         queue = sessions_catalog(dir, catalog, queue)
   233         queue = sessions_catalog(dir, catalog, queue)
   234     }
   234     }
   235 
   235 
   236     for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
   236     for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
   240 
   240 
   241 
   241 
   242 
   242 
   243   /** build **/
   243   /** build **/
   244 
   244 
       
   245   private def echo(msg: String) { java.lang.System.out.println(msg) }
       
   246   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
       
   247 
   245   private def build_job(build_images: Boolean,  // FIXME
   248   private def build_job(build_images: Boolean,  // FIXME
   246     key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
   249     key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
   247   {
   250   {
   248     val cwd = Isabelle_System.platform_file(info.dir)
   251     val cwd = info.dir.file
   249     val script =
   252     val script =
   250       if (is_pure(key.name)) "./build " + key.name
   253       if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
   251       else """echo "Bad session" >&2; exit 2"""
   254       else """echo "Bad session" >&2; exit 2"""
   252     new Isabelle_System.Bash_Job(cwd, null, script)
   255     new Isabelle_System.Bash_Job(cwd, null, script)
   253   }
   256   }
   254 
   257 
   255   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   258   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   256     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   259     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   257   {
   260   {
   258     val full_queue = find_sessions(more_dirs)
   261     val full_queue = find_sessions(more_dirs)
   259 
       
   260     val build_options = (Options.init() /: options)(_.define_simple(_))
   262     val build_options = (Options.init() /: options)(_.define_simple(_))
   261 
   263 
   262     sessions.filter(name => !full_queue.defined(name)) match {
   264     sessions.filter(name => !full_queue.defined(name)) match {
   263       case Nil =>
   265       case Nil =>
   264       case bad => error("Undefined session(s): " + commas_quote(bad))
   266       case bad => error("Undefined session(s): " + commas_quote(bad))
   266 
   268 
   267     val required_queue =
   269     val required_queue =
   268       if (all_sessions) full_queue
   270       if (all_sessions) full_queue
   269       else full_queue.required(sessions)
   271       else full_queue.required(sessions)
   270 
   272 
   271     for ((key, info) <- required_queue.topological_order) {
   273     // prepare browser info dir
   272       if (list_only) println(key.name + " in " + info.dir)
   274     if (build_options.bool("browser_info") &&
   273       else {
   275       !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
   274         val (out, err, rc) = build_job(build_images, key, info).join
   276     {
   275         java.lang.System.err.print(err)
   277       Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
   276       }
   278       Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
   277     }
   279         Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
   278 
   280       Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
   279     0
   281         Standard_System.read_file(
       
   282           Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
       
   283         Standard_System.read_file(
       
   284           Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
       
   285         Standard_System.read_file(
       
   286           Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
       
   287     }
       
   288 
       
   289     // prepare log dir
       
   290     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
       
   291     log_dir.file.mkdirs()
       
   292 
       
   293     // run jobs
       
   294     val rcs =
       
   295       for ((key, info) <- required_queue.topological_order) yield
       
   296       {
       
   297         if (list_only) { echo(key.name + " in " + info.dir); 0 }
       
   298         else {
       
   299           if (build_images) echo("Building " + key.name + "...")
       
   300           else echo("Running " + key.name + "...")
       
   301 
       
   302           val (out, err, rc) = build_job(build_images, key, info).join
       
   303           echo_n(err)
       
   304 
       
   305           val log = log_dir + Path.basic(key.name)
       
   306           if (rc == 0) {
       
   307             Standard_System.write_file(log.ext("gz").file, out, true)
       
   308           }
       
   309           else {
       
   310             Standard_System.write_file(log.file, out)
       
   311             echo(key.name + " FAILED")
       
   312             echo("(see also " + log.file + ")")
       
   313             val lines = split_lines(out)
       
   314             val tail = lines.drop(lines.length - 20 max 0)
       
   315             echo("\n" + cat_lines(tail))
       
   316           }
       
   317           rc
       
   318         }
       
   319       }
       
   320     (0 /: rcs)(_ max _)
   280   }
   321   }
   281 
   322 
   282 
   323 
   283   /* command line entry point */
   324   /* command line entry point */
   284 
   325