src/Pure/System/build.scala
changeset 48639 675988e64bf9
parent 48626 ef374008cb7c
child 48649 bf9bff84a61d
equal deleted inserted replaced
48638:22d65e375c01 48639:675988e64bf9
   328 
   328 
   329 
   329 
   330   /* jobs */
   330   /* jobs */
   331 
   331 
   332   private class Job(dir: Path, env: Map[String, String], script: String, args: String,
   332   private class Job(dir: Path, env: Map[String, String], script: String, args: String,
   333     output: Path, do_output: Boolean)
   333     val parent_heap: String, output: Path, do_output: Boolean)
   334   {
   334   {
   335     private val args_file = File.tmp_file("args")
   335     private val args_file = File.tmp_file("args")
   336     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   336     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
   337     File.write(args_file, args)
   337     File.write(args_file, args)
   338 
   338 
   343     def is_finished: Boolean = result.is_finished
   343     def is_finished: Boolean = result.is_finished
   344     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   344     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   345     def output_path: Option[Path] = if (do_output) Some(output) else None
   345     def output_path: Option[Path] = if (do_output) Some(output) else None
   346   }
   346   }
   347 
   347 
   348   private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
   348   private def start_job(name: String, info: Session.Info, parent_heap: String,
   349     options: Options, verbose: Boolean, browser_info: Path): Job =
   349     output: Path, do_output: Boolean, options: Options, verbose: Boolean, browser_info: Path): Job =
   350   {
   350   {
   351     // global browser info dir
   351     // global browser info dir
   352     if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   352     if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   353     {
   353     {
   354       browser_info.file.mkdirs()
   354       browser_info.file.mkdirs()
   399           pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   399           pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   400             pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   400             pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   401           (do_output, (options, (verbose, (browser_info, (parent,
   401           (do_output, (options, (verbose, (browser_info, (parent,
   402             (name, info.theories)))))))
   402             (name, info.theories)))))))
   403     }
   403     }
   404     new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output)
   404     new Job(info.dir, env, script, YXML.string_of_body(args_xml), parent_heap, output, do_output)
   405   }
   405   }
   406 
   406 
   407 
   407 
   408   /* log files and corresponding heaps */
   408   /* log files and corresponding heaps */
   409 
   409 
   412   private def log_gz(name: String): Path = log(name).ext("gz")
   412   private def log_gz(name: String): Path = log(name).ext("gz")
   413 
   413 
   414   private def sources_stamp(digests: List[SHA1.Digest]): String =
   414   private def sources_stamp(digests: List[SHA1.Digest]): String =
   415     digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   415     digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   416 
   416 
   417   private def heap_stamp(output: Option[Path]): String =
   417   private val no_heap: String = "heap: -"
       
   418 
       
   419   private def heap_stamp(heap: Option[Path]): String =
   418   {
   420   {
   419     "heap: " +
   421     "heap: " +
   420       (output match {
   422       (heap match {
   421         case Some(path) =>
   423         case Some(path) =>
   422           val file = path.file
   424           val file = path.file
   423           if (file.isFile) file.length.toString + " " + file.lastModified.toString
   425           if (file.isFile) file.length.toString + " " + file.lastModified.toString
   424           else "-"
   426           else "-"
   425         case None => "-"
   427         case None => "-"
   426       })
   428       })
   427   }
   429   }
   428 
   430 
   429   private def check_stamps(dir: Path, name: String): Option[(String, Boolean)] =
   431   private def read_stamps(path: Path): Option[(String, String, String)] =
   430   {
   432     if (path.is_file) {
   431     val file = (dir + log_gz(name)).file
   433       val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
   432     if (file.isFile) {
       
   433       val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(file)))
       
   434       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   434       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   435       val (s, h) = try { (reader.readLine, reader.readLine) } finally { reader.close }
   435       val (s, h1, h2) =
   436       if (s != null && s.startsWith("sources: ") && h != null && h.startsWith("heap: ") &&
   436         try { (reader.readLine, reader.readLine, reader.readLine) }
   437           h == heap_stamp(Some(dir + Path.basic(name)))) Some((s, h != "heap: -"))
   437         finally { reader.close }
       
   438       if (s != null && s.startsWith("sources: ") &&
       
   439           h1 != null && h1.startsWith("heap: ") &&
       
   440           h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
   438       else None
   441       else None
   439     }
   442     }
   440     else None
   443     else None
   441   }
       
   442 
   444 
   443 
   445 
   444   /* build */
   446   /* build */
   445 
   447 
   446   def build(
   448   def build(
   487         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   489         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   488       }
   490       }
   489     }
   491     }
   490 
   492 
   491     // scheduler loop
   493     // scheduler loop
       
   494     case class Result(current: Boolean, heap: String, rc: Int)
       
   495 
   492     @tailrec def loop(
   496     @tailrec def loop(
   493       pending: Session.Queue,
   497       pending: Session.Queue,
   494       running: Map[String, Job],
   498       running: Map[String, Job],
   495       results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] =
   499       results: Map[String, Result]): Map[String, Result] =
   496     {
   500     {
   497       if (pending.is_empty) results
   501       if (pending.is_empty) results
   498       else
   502       else
   499         running.find({ case (_, job) => job.is_finished }) match {
   503         running.find({ case (_, job) => job.is_finished }) match {
   500           case Some((name, job)) =>
   504           case Some((name, job)) =>
   501             // finish job
   505             // finish job
   502 
   506 
   503             val (out, err, rc) = job.join
   507             val (out, err, rc) = job.join
   504             echo(Library.trim_line(err))
   508             echo(Library.trim_line(err))
   505 
   509 
   506             if (rc == 0) {
   510             val heap =
   507               val sources = make_stamp(name)
   511               if (rc == 0) {
   508               val heap = heap_stamp(job.output_path)
   512                 (output_dir + log(name)).file.delete
   509               (output_dir + log(name)).file.delete
   513 
   510               File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
   514                 val sources = make_stamp(name)
   511             }
   515                 val heap = heap_stamp(job.output_path)
   512             else {
   516                 File.write_gzip(output_dir + log_gz(name),
   513               (output_dir + log_gz(name)).file.delete
   517                   sources + "\n" + job.parent_heap + "\n" + heap + "\n" + out)
   514               File.write(output_dir + log(name), out)
   518 
   515               echo(name + " FAILED")
   519                 heap
   516               echo("(see also " + (output_dir + log(name)).file.toString + ")")
   520               }
   517               val lines = split_lines(out)
   521               else {
   518               val tail = lines.drop(lines.length - 20 max 0)
   522                 (output_dir + Path.basic(name)).file.delete
   519               echo("\n" + cat_lines(tail))
   523                 (output_dir + log_gz(name)).file.delete
   520             }
   524 
   521             loop(pending - name, running - name, results + (name -> (false, rc)))
   525                 File.write(output_dir + log(name), out)
       
   526                 echo(name + " FAILED")
       
   527                 echo("(see also " + (output_dir + log(name)).file.toString + ")")
       
   528                 val lines = split_lines(out)
       
   529                 val tail = lines.drop(lines.length - 20 max 0)
       
   530                 echo("\n" + cat_lines(tail))
       
   531 
       
   532                 no_heap
       
   533               }
       
   534             loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   522 
   535 
   523           case None if (running.size < (max_jobs max 1)) =>
   536           case None if (running.size < (max_jobs max 1)) =>
   524             // check/start next job
   537             // check/start next job
   525             pending.dequeue(running.isDefinedAt(_)) match {
   538             pending.dequeue(running.isDefinedAt(_)) match {
   526               case Some((name, info)) =>
   539               case Some((name, info)) =>
   527                 val parent_result = info.parent.map(results(_))
   540                 val parent_result =
   528                 val parent_current = parent_result.forall(_._1)
   541                   info.parent match {
   529                 val parent_ok = parent_result.forall(_._2 == 0)
   542                     case None => Result(true, no_heap, 0)
   530 
   543                     case Some(parent) => results(parent)
       
   544                   }
   531                 val output = output_dir + Path.basic(name)
   545                 val output = output_dir + Path.basic(name)
   532                 val do_output = build_heap || queue.is_inner(name)
   546                 val do_output = build_heap || queue.is_inner(name)
   533 
   547 
   534                 val current =
   548                 val (current, heap) =
   535                 {
   549                 {
   536                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   550                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   537                     case Some(dir) =>
   551                     case Some(dir) =>
   538                       check_stamps(dir, name) match {
   552                       read_stamps(dir + log_gz(name)) match {
   539                         case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
   553                         case Some((s, h1, h2)) =>
   540                         case None => false
   554                           val heap = heap_stamp(Some(dir + Path.basic(name)))
       
   555                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
       
   556                             !(do_output && heap == no_heap), heap)
       
   557                         case None => (false, no_heap)
   541                       }
   558                       }
   542                     case None => false
   559                     case None => (false, no_heap)
   543                   }
   560                   }
   544                 }
   561                 }
   545                 val all_current = current && parent_current
   562                 val all_current = current && parent_result.current
   546 
   563 
   547                 if (all_current)
   564                 if (all_current)
   548                   loop(pending - name, running, results + (name -> (true, 0)))
   565                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   549                 else if (no_build)
   566                 else if (no_build)
   550                   loop(pending - name, running, results + (name -> (false, 1)))
   567                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   551                 else if (parent_ok) {
   568                 else if (parent_result.rc == 0) {
   552                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   569                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   553                   val job =
   570                   val job =
   554                     start_job(name, info, output, do_output, info.options, verbose, browser_info)
   571                     start_job(name, info, parent_result.heap, output, do_output,
       
   572                       info.options, verbose, browser_info)
   555                   loop(pending, running + (name -> job), results)
   573                   loop(pending, running + (name -> job), results)
   556                 }
   574                 }
   557                 else {
   575                 else {
   558                   echo(name + " CANCELLED")
   576                   echo(name + " CANCELLED")
   559                   loop(pending - name, running, results + (name -> (false, 1)))
   577                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   560                 }
   578                 }
   561               case None => sleep(); loop(pending, running, results)
   579               case None => sleep(); loop(pending, running, results)
   562             }
   580             }
   563           case None => sleep(); loop(pending, running, results)
   581           case None => sleep(); loop(pending, running, results)
   564         }
   582         }
   569         echo("### Nothing to build")
   587         echo("### Nothing to build")
   570         Map.empty
   588         Map.empty
   571       }
   589       }
   572       else loop(queue, Map.empty, Map.empty)
   590       else loop(queue, Map.empty, Map.empty)
   573 
   591 
   574     val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 })
   592     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   575     if (rc != 0 && (verbose || !no_build)) {
   593     if (rc != 0 && (verbose || !no_build)) {
   576       val unfinished =
   594       val unfinished =
   577         (for ((name, (_, r)) <- results.iterator if r != 0) yield name).toList.sorted
   595         (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
   578       echo("Unfinished session(s): " + commas(unfinished))
   596       echo("Unfinished session(s): " + commas(unfinished))
   579     }
   597     }
   580     rc
   598     rc
   581   }
   599   }
   582 
   600