record heap sizes;
authorwenzelm
Sun Oct 09 16:24:54 2016 +0200 (2016-10-09)
changeset 641206c5039016321
parent 64119 8094eaa38d4b
child 64121 f2c8f6b11dcf
record heap sizes;
src/Pure/Tools/build_history.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_history.scala	Sun Oct 09 15:28:18 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_history.scala	Sun Oct 09 16:24:54 2016 +0200
     1.3 @@ -263,6 +263,8 @@
     1.4          other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
     1.5            Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
     1.6  
     1.7 +      val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
     1.8 +
     1.9        val meta_info =
    1.10          List(Build_Log.Field.build_engine -> BUILD_HISTORY,
    1.11            Build_Log.Field.build_host -> build_host,
    1.12 @@ -271,22 +273,31 @@
    1.13            Build_Log.Field.isabelle_version -> isabelle_version)
    1.14  
    1.15        val ml_statistics =
    1.16 -        Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info().
    1.17 -          finished_sessions.flatMap(session_name =>
    1.18 -            {
    1.19 -              val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
    1.20 -              if (session_log.is_file) {
    1.21 -                Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
    1.22 -                  ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
    1.23 -              }
    1.24 -              else Nil
    1.25 -            })
    1.26 +        build_info.finished_sessions.flatMap(session_name =>
    1.27 +          {
    1.28 +            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
    1.29 +            if (session_log.is_file) {
    1.30 +              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
    1.31 +                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
    1.32 +            }
    1.33 +            else Nil
    1.34 +          })
    1.35 +
    1.36 +      val heap_sizes =
    1.37 +        build_info.finished_sessions.flatMap(session_name =>
    1.38 +          {
    1.39 +            val heap = isabelle_output + Path.explode(session_name)
    1.40 +            if (heap.is_file)
    1.41 +              Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
    1.42 +            else None
    1.43 +          })
    1.44  
    1.45        Isabelle_System.mkdirs(log_path.dir)
    1.46        File.write_gzip(log_path,
    1.47 -        cat_lines(
    1.48 +        Library.terminate_lines(
    1.49            Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
    1.50 -          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))))
    1.51 +          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
    1.52 +          heap_sizes))
    1.53  
    1.54        Output.writeln(log_path.implode, stdout = true)
    1.55  
     2.1 --- a/src/Pure/Tools/build_log.scala	Sun Oct 09 15:28:18 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sun Oct 09 16:24:54 2016 +0200
     2.3 @@ -357,6 +357,7 @@
     2.4      timing: Timing,
     2.5      ml_timing: Timing,
     2.6      ml_statistics: List[Properties.T],
     2.7 +    heap_size: Option[Long],
     2.8      status: Session_Status.Value)
     2.9    {
    2.10      def finished: Boolean = status == Session_Status.FINISHED
    2.11 @@ -401,6 +402,7 @@
    2.12      val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
    2.13      val Session_Failed = new Regex("""^(\S+) FAILED""")
    2.14      val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
    2.15 +    val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
    2.16  
    2.17      var chapter = Map.empty[String, String]
    2.18      var groups = Map.empty[String, List[String]]
    2.19 @@ -411,10 +413,11 @@
    2.20      var failed = Set.empty[String]
    2.21      var cancelled = Set.empty[String]
    2.22      var ml_statistics = Map.empty[String, List[Properties.T]]
    2.23 +    var heap_sizes = Map.empty[String, Long]
    2.24  
    2.25      def all_sessions: Set[String] =
    2.26 -      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++
    2.27 -      ml_timing.keySet ++ failed ++ cancelled ++ started ++ ml_statistics.keySet
    2.28 +      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
    2.29 +      failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
    2.30  
    2.31  
    2.32      for (line <- log_file.lines) {
    2.33 @@ -450,13 +453,16 @@
    2.34            ml_timing += (name -> Timing(elapsed, cpu, gc))
    2.35            threads += (name -> t)
    2.36  
    2.37 +        case Heap(name, Value.Long(size)) =>
    2.38 +          heap_sizes += (name -> size)
    2.39 +
    2.40          case _ if line.startsWith(ML_STATISTICS_MARKER) =>
    2.41            val (name, props) =
    2.42              Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
    2.43                case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
    2.44                case _ => log_file.err("malformed ML_statistics " + quote(line))
    2.45              }
    2.46 -          ml_statistics = ml_statistics + (name -> (props :: ml_statistics.getOrElse(name, Nil)))
    2.47 +          ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
    2.48  
    2.49          case _ =>
    2.50        }
    2.51 @@ -480,6 +486,7 @@
    2.52                timing.getOrElse(name, Timing.zero),
    2.53                ml_timing.getOrElse(name, Timing.zero),
    2.54                ml_statistics.getOrElse(name, Nil).reverse,
    2.55 +              heap_sizes.get(name),
    2.56                status)
    2.57            (name -> entry)
    2.58          }):_*)