src/Pure/Tools/profiling.scala
author wenzelm
Mon, 24 Jul 2023 21:05:11 +0200
changeset 78450 14219730e04f
parent 78448 573cc2ab69c5
child 78452 14ceb9a51e97
permissions -rw-r--r--
more statistics;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78414
406d34a8a67a update headers;
wenzelm
parents: 78330
diff changeset
     1
/*  Title:      Pure/Tools/profiling.scala
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     2
    Author:     Makarius
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     3
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     4
Build sessions for profiling of ML heap content.
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     5
*/
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     6
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     7
package isabelle
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     8
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     9
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    10
import java.util.Locale
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    11
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    12
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    13
object Profiling {
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    14
  /* percentage: precision in permille */
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    15
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    16
  def percentage(a: Long, b: Long): Percentage =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    17
    new Percentage(if (b == 0L) 0 else ((a.toDouble / b.toDouble) * 1000.0).round.toInt)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    18
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    19
  def percentage(a: Int, b: Int): Percentage = percentage(a.toLong, b.toLong)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    20
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    21
  def percentage_space(a: Space, b: Space): Percentage = percentage(a.bytes, b.bytes)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    22
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    23
  final class Percentage private[Profiling](val permille: Int) extends AnyVal {
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    24
    def percent: Double = permille.toDouble / 10
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    25
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    26
    override def toString: String = (permille / 10).toString + "." + (permille % 10).toString + "%"
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    27
  }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    28
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    29
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    30
  /* session statistics */
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    31
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    32
  sealed case class Session_Statistics(
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    33
    theories: Int = 0,
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    34
    garbage_theories: Int = 0,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    35
    locales: Int = 0,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    36
    locale_thms: Int = 0,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    37
    global_thms: Int = 0,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    38
    sizeof_thys_id: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    39
    sizeof_thms_id: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    40
    sizeof_terms: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    41
    sizeof_types: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    42
    sizeof_spaces: Space = Space.zero)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    43
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    44
  object Statistics {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    45
    private val encode_args: XML.Encode.T[List[String]] =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    46
      (args: List[String]) =>
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    47
        { import XML.Encode._; list(string)(args) }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    48
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    49
    private val decode_result: XML.Decode.T[Session_Statistics] =
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    50
      (body: XML.Body) =>
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    51
        {
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    52
          val (a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))) = {
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    53
            import XML.Decode._
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    54
            pair(int, pair(int, pair(int, pair(int, pair(int,
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    55
              pair(long, pair(long, pair(long, pair(long, long)))))))))(body)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    56
          }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    57
          Session_Statistics(
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    58
            theories = a,
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    59
            garbage_theories = b,
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    60
            locales = c,
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    61
            locale_thms = d,
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    62
            global_thms = e,
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    63
            sizeof_thys_id = Space.bytes(f),
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    64
            sizeof_thms_id = Space.bytes(g),
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    65
            sizeof_terms = Space.bytes(h),
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    66
            sizeof_types = Space.bytes(i),
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    67
            sizeof_spaces = Space.bytes(j))
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    68
        }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    69
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    70
    def make(
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    71
      store: Store,
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    72
      session_background: Sessions.Background,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    73
      parent: Option[Statistics] = None
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    74
    ): Statistics = {
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    75
      val session_base = session_background.base
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    76
      val session_name = session_base.session_name
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    77
      val sessions_structure = session_background.sessions_structure
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    78
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    79
      val session = {
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    80
        val args = session_base.used_theories.map(p => p._1.theory)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    81
        val eval_args =
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    82
          List("--eval", "use_thy " + ML_Syntax.print_string_bytes("~~/src/Tools/Profiling"))
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    83
        Isabelle_System.with_tmp_dir("profiling") { dir =>
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    84
          val put_env = List("ISABELLE_PROFILING" -> dir.implode)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    85
          File.write(dir + Path.explode("args.yxml"), YXML.string_of_body(encode_args(args)))
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    86
          val session_heaps =
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    87
            ML_Process.session_heaps(store, session_background, logic = session_name)
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    88
          ML_Process(store.options, session_background, session_heaps, args = eval_args,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    89
            env = Isabelle_System.settings(put_env)).result().check
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    90
          decode_result(YXML.parse_body(File.read(dir + Path.explode("result.yxml"))))
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    91
        }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    92
      }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    93
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    94
      new Statistics(parent = parent, session = session_name,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    95
        theories = session.theories,
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
    96
        garbage_theories = session.garbage_theories,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    97
        locales = session.locales,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    98
        locale_thms = session.locale_thms,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
    99
        global_thms = session.global_thms,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   100
        heap_size = Space.bytes(store.the_heap(session_name).file.length),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   101
        thys_id_size = session.sizeof_thys_id,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   102
        thms_id_size = session.sizeof_thms_id,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   103
        terms_size = session.sizeof_terms,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   104
        types_size = session.sizeof_types,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   105
        spaces_size = session.sizeof_spaces)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   106
    }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   107
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   108
    val empty: Statistics = new Statistics()
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   109
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   110
    val header0: List[String] =
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   111
      List(
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   112
        "theories",
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   113
        "garbage_theories%",
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   114
        "locales",
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   115
        "locale_thms",
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   116
        "global_thms",
78329
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   117
        "locale_thms%",
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   118
        "global_thms%",
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   119
        "heap_size",
78329
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   120
        "thys_id_size%",
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   121
        "thms_id_size%",
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   122
        "terms_size%",
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   123
        "types_size%",
a041d49736f2 tuned output;
wenzelm
parents: 78328
diff changeset
   124
        "spaces_size%")
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   125
78330
1a69d3a3e3aa tuned output;
wenzelm
parents: 78329
diff changeset
   126
    def header: List[String] =
1a69d3a3e3aa tuned output;
wenzelm
parents: 78329
diff changeset
   127
      "session" :: header0.flatMap(a => List(a, "\u2211" + a))
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   128
  }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   129
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   130
  final class Statistics private(
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   131
    val parent: Option[Statistics] = None,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   132
    val session: String = "",
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   133
    val theories: Int = 0,
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   134
    val garbage_theories: Int = 0,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   135
    val locales: Int = 0,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   136
    val locale_thms: Int = 0,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   137
    val global_thms: Int = 0,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   138
    val heap_size: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   139
    val thys_id_size: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   140
    val thms_id_size: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   141
    val terms_size: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   142
    val types_size: Space = Space.zero,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   143
    val spaces_size: Space = Space.zero
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   144
  ) {
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   145
    def garbage_theories_percentage: Percentage =
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   146
      percentage(garbage_theories, theories + garbage_theories)
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   147
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   148
    private def size_percentage(space: Space): Percentage =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   149
      percentage_space(space, heap_size)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   150
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   151
    private def thms_percentage(thms: Int): Percentage =
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   152
      percentage(thms, locale_thms + global_thms)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   153
78330
1a69d3a3e3aa tuned output;
wenzelm
parents: 78329
diff changeset
   154
    val fields0: List[Any] =
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   155
      List(
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   156
        theories,
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   157
        garbage_theories_percentage.toString,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   158
        locales,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   159
        locale_thms,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   160
        global_thms,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   161
        thms_percentage(locale_thms).toString,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   162
        thms_percentage(global_thms).toString,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   163
        heap_size.print,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   164
        size_percentage(thys_id_size).toString,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   165
        size_percentage(thms_id_size).toString,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   166
        size_percentage(terms_size).toString,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   167
        size_percentage(types_size).toString,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   168
        size_percentage(spaces_size).toString)
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   169
78330
1a69d3a3e3aa tuned output;
wenzelm
parents: 78329
diff changeset
   170
    def fields: List[Any] =
1a69d3a3e3aa tuned output;
wenzelm
parents: 78329
diff changeset
   171
      session :: fields0.zipWithIndex.flatMap({ case (a, i) => List(a, cumulative.fields0(i)) })
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   172
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   173
    lazy val cumulative: Statistics =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   174
      parent match {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   175
        case None => this
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   176
        case Some(other) =>
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   177
          new Statistics(parent = None,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   178
            session = session,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   179
            theories = other.cumulative.theories + theories,
78450
14219730e04f more statistics;
wenzelm
parents: 78448
diff changeset
   180
            garbage_theories = other.cumulative.garbage_theories + garbage_theories,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   181
            locales = other.cumulative.locales + locales,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   182
            locale_thms = other.cumulative.locale_thms + locale_thms,
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   183
            global_thms = other.cumulative.global_thms + global_thms,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   184
            heap_size = other.cumulative.heap_size + heap_size,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   185
            thys_id_size = other.cumulative.thys_id_size + thys_id_size,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   186
            thms_id_size = other.cumulative.thms_id_size + thms_id_size,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   187
            terms_size = other.cumulative.terms_size + terms_size,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   188
            types_size = other.cumulative.types_size + types_size,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   189
            spaces_size = other.cumulative.spaces_size + spaces_size)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   190
      }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   191
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   192
    override def toString: String = "Statistics(" + session + ")"
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   193
  }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   194
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   195
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   196
  /* profiling results */
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   197
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   198
  sealed case class Results(build_results: Build.Results, sessions: List[Statistics]) {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   199
    def output(
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   200
      output_dir: Path = default_output_dir,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   201
      progress: Progress = new Progress
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   202
    ): Unit = {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   203
      progress.echo("Output directory " + output_dir.absolute)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   204
      Isabelle_System.make_directory(output_dir)
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   205
      val csv_records = for (session <- sessions) yield CSV.Record(session.fields:_*)
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   206
      CSV.File("sessions", Statistics.header, csv_records).write(output_dir)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   207
    }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   208
  }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   209
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   210
  def profiling(
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   211
    options: Options,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   212
    selection: Sessions.Selection = Sessions.Selection.empty,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   213
    progress: Progress = new Progress,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   214
    dirs: List[Path] = Nil,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   215
    select_dirs: List[Path] = Nil,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   216
    numa_shuffling: Boolean = false,
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   217
    max_jobs: Int = 1
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   218
  ): Results = {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   219
    /* sessions structure */
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   220
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   221
    val sessions_dirs = dirs ::: select_dirs
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   222
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   223
    val sessions_structure =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   224
      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   225
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   226
    val selected_sessions = sessions_structure.imports_selection(selection)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   227
    val cumulative_sessions = sessions_structure.build_requirements(selected_sessions)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   228
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   229
    val sessions_selection = Sessions.Selection(sessions = selected_sessions)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   230
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   231
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   232
    /* build session */
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   233
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   234
    val store = Store(options)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   235
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   236
    def build(
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   237
      selection: Sessions.Selection,
78448
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   238
      build_options: Options = options,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   239
      build_heap: Boolean = false,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   240
      clean_build: Boolean = false
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   241
    ): Build.Results = {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   242
      val results =
78448
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   243
        Build.build(build_options, progress = progress,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   244
          selection = selection, build_heap = build_heap, clean_build = clean_build,
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   245
          dirs = sessions_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   246
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   247
      if (results.ok) results else error("Build failed")
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   248
    }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   249
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   250
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   251
    /* session builds and profiling */
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   252
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   253
    progress.echo("Build session requirements:")
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   254
    build(sessions_selection.copy(requirements = true), build_heap = true)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   255
    progress.echo("DONE")
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   256
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   257
    progress.echo("Build sessions:")
78448
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   258
    val build_results =
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   259
      build(sessions_selection,
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   260
        build_options = options + "context_theory_tracing",
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   261
        build_heap = true,
573cc2ab69c5 more thorough context tracing;
wenzelm
parents: 78414
diff changeset
   262
        clean_build = true)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   263
    progress.echo("DONE")
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   264
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   265
    val sessions = {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   266
      var seen = Map.empty[String, Statistics]
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   267
      for (session_name <- cumulative_sessions)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   268
      yield {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   269
        progress.echo("Profiling " + session_name + " ...")
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   270
        val parent =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   271
          for {
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   272
            info <- sessions_structure.get(session_name)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   273
            parent_name <- info.parent
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   274
            parent_stats <- seen.get(parent_name)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   275
          } yield parent_stats
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   276
        val stats =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   277
          Statistics.make(store,
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   278
            build_results.deps.background(session_name),
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   279
            parent = parent)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   280
        seen += (session_name -> stats)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   281
        stats
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   282
      }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   283
    }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   284
    progress.echo("DONE")
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   285
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   286
    Results(build_results, sessions)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   287
  }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   288
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   289
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   290
  /* Isabelle tool wrapper */
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   291
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   292
  val default_output_dir: Path = Path.explode("profiling")
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   293
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   294
  val isabelle_tool =
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   295
    Isabelle_Tool("profiling", "build sessions for profiling of ML heap content",
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   296
      Scala_Project.here, { args =>
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   297
        var base_sessions: List[String] = Nil
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   298
        var select_dirs: List[Path] = Nil
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   299
        var numa_shuffling = false
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   300
        var output_dir = default_output_dir
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   301
        var exclude_session_groups: List[String] = Nil
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   302
        var all_sessions = false
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   303
        var dirs: List[Path] = Nil
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   304
        var session_groups: List[String] = Nil
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   305
        var max_jobs = 1
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   306
        var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   307
        var verbose = false
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   308
        var exclude_sessions: List[String] = Nil
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   309
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   310
        val getopts = Getopts("""
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   311
Usage: isabelle profiling [OPTIONS] [SESSIONS ...]
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   312
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   313
  Options are:
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   314
    -B NAME      include session NAME and all descendants
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   315
    -D DIR       include session directory and select its sessions
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   316
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   317
    -O DIR       output directory (default: """ + default_output_dir + """)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   318
    -X NAME      exclude sessions from group NAME and all descendants
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   319
    -a           select all sessions
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   320
    -d DIR       include session directory
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   321
    -g NAME      select session group NAME
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   322
    -j INT       maximum number of parallel jobs (default 1)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   323
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   324
    -v           verbose
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   325
    -x NAME      exclude session NAME and all descendants
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   326
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   327
  Build specified sessions, with options similar to "isabelle build" and
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   328
  implicit modifications for profiling of ML heap content.""",
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   329
          "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   330
          "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   331
          "N" -> (_ => numa_shuffling = true),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   332
          "O:" -> (arg => output_dir = Path.explode(arg)),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   333
          "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   334
          "a" -> (_ => all_sessions = true),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   335
          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   336
          "g:" -> (arg => session_groups = session_groups ::: List(arg)),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   337
          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   338
          "o:" -> (arg => options = options + arg),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   339
          "v" -> (_ => verbose = true),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   340
          "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   341
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   342
        val sessions = getopts(args)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   343
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   344
        val progress = new Console_Progress(verbose = verbose)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   345
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   346
        val results =
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   347
          progress.interrupt_handler {
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   348
            profiling(options,
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   349
              selection = Sessions.Selection(
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   350
                all_sessions = all_sessions,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   351
                base_sessions = base_sessions,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   352
                exclude_session_groups = exclude_session_groups,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   353
                exclude_sessions = exclude_sessions,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   354
                session_groups = session_groups,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   355
                sessions = sessions),
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   356
              progress = progress,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   357
              dirs = dirs,
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   358
              select_dirs = select_dirs,
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
   359
              numa_shuffling = Host.numa_check(progress, numa_shuffling),
78328
007b04dc6f96 clarified session_statistics: removed somewhat pointless per-theory statistics;
wenzelm
parents: 78315
diff changeset
   360
              max_jobs = max_jobs)
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   361
          }
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   362
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   363
        results.output(output_dir = output_dir.absolute, progress = progress)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   364
      })
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
   365
}