src/Pure/Tools/dump.scala
author wenzelm
Sat Sep 08 13:22:23 2018 +0200 (9 months ago)
changeset 68946 6dd1460f6920
parent 68945 fa5d936daf1c
child 68947 ea804c814693
permissions -rw-r--r--
more accurate output;
wenzelm@68308
     1
/*  Title:      Pure/Tools/dump.scala
wenzelm@68308
     2
    Author:     Makarius
wenzelm@68308
     3
wenzelm@68348
     4
Dump cumulative PIDE session database.
wenzelm@68308
     5
*/
wenzelm@68308
     6
wenzelm@68308
     7
package isabelle
wenzelm@68308
     8
wenzelm@68308
     9
wenzelm@68308
    10
object Dump
wenzelm@68308
    11
{
wenzelm@68316
    12
  /* aspects */
wenzelm@68316
    13
wenzelm@68316
    14
  sealed case class Aspect_Args(
wenzelm@68355
    15
    options: Options,
wenzelm@68355
    16
    progress: Progress,
wenzelm@68365
    17
    deps: Sessions.Deps,
wenzelm@68355
    18
    output_dir: Path,
wenzelm@68929
    19
    snapshot: Document.Snapshot,
wenzelm@68929
    20
    node_status: Document_Status.Node_Status)
wenzelm@68319
    21
  {
wenzelm@68365
    22
    def write(file_name: Path, bytes: Bytes)
wenzelm@68319
    23
    {
wenzelm@68929
    24
      val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
wenzelm@68319
    25
      Isabelle_System.mkdirs(path.dir)
wenzelm@68319
    26
      Bytes.write(path, bytes)
wenzelm@68319
    27
    }
wenzelm@68319
    28
wenzelm@68365
    29
    def write(file_name: Path, text: String): Unit =
wenzelm@68365
    30
      write(file_name, Bytes(text))
wenzelm@68332
    31
wenzelm@68365
    32
    def write(file_name: Path, body: XML.Body): Unit =
wenzelm@68365
    33
      write(file_name, Symbol.encode(YXML.string_of_body(body)))
wenzelm@68319
    34
  }
wenzelm@68316
    35
wenzelm@68347
    36
  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
wenzelm@68347
    37
    options: List[String] = Nil)
wenzelm@68345
    38
  {
wenzelm@68345
    39
    override def toString: String = name
wenzelm@68345
    40
  }
wenzelm@68316
    41
wenzelm@68347
    42
  val known_aspects =
wenzelm@68316
    43
    List(
wenzelm@68365
    44
      Aspect("markup", "PIDE markup (YXML format)",
wenzelm@68365
    45
        { case args =>
wenzelm@68365
    46
            args.write(Path.explode("markup.yxml"),
wenzelm@68365
    47
              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
wenzelm@68365
    48
        }),
wenzelm@68319
    49
      Aspect("messages", "output messages (YXML format)",
wenzelm@68319
    50
        { case args =>
wenzelm@68365
    51
            args.write(Path.explode("messages.yxml"),
wenzelm@68365
    52
              args.snapshot.messages.iterator.map(_._1).toList)
wenzelm@68347
    53
        }),
wenzelm@68347
    54
      Aspect("latex", "generated LaTeX source",
wenzelm@68347
    55
        { case args =>
wenzelm@68365
    56
            for (entry <- args.snapshot.exports if entry.name == "document.tex")
wenzelm@68365
    57
              args.write(Path.explode(entry.name), entry.uncompressed())
wenzelm@68491
    58
        }, options = List("editor_presentation", "export_document")),
wenzelm@68347
    59
      Aspect("theory", "foundational theory content",
wenzelm@68347
    60
        { case args =>
wenzelm@68347
    61
            for {
wenzelm@68365
    62
              entry <- args.snapshot.exports
wenzelm@68347
    63
              if entry.name.startsWith(Export_Theory.export_prefix)
wenzelm@68365
    64
            } args.write(Path.explode(entry.name), entry.uncompressed())
wenzelm@68347
    65
        }, options = List("editor_presentation", "export_theory"))
wenzelm@68345
    66
    ).sortBy(_.name)
wenzelm@68316
    67
wenzelm@68316
    68
  def show_aspects: String =
wenzelm@68345
    69
    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
wenzelm@68316
    70
wenzelm@68316
    71
  def the_aspect(name: String): Aspect =
wenzelm@68316
    72
    known_aspects.find(aspect => aspect.name == name) getOrElse
wenzelm@68316
    73
      error("Unknown aspect " + quote(name))
wenzelm@68316
    74
wenzelm@68316
    75
wenzelm@68316
    76
  /* dump */
wenzelm@68316
    77
wenzelm@68945
    78
  val default_output_dir: Path = Path.explode("dump")
wenzelm@68945
    79
  val default_commit_clean_delay: Time = Time.seconds(-1.0)
wenzelm@68945
    80
  val default_watchdog_timeout: Time = Time.seconds(600.0)
wenzelm@68316
    81
wenzelm@68416
    82
  def make_options(options: Options, aspects: List[Aspect]): Options =
wenzelm@68895
    83
  {
wenzelm@68896
    84
    val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
wenzelm@68895
    85
    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
wenzelm@68895
    86
  }
wenzelm@68416
    87
wenzelm@68308
    88
  def dump(options: Options, logic: String,
wenzelm@68316
    89
    aspects: List[Aspect] = Nil,
wenzelm@68308
    90
    progress: Progress = No_Progress,
wenzelm@68308
    91
    log: Logger = No_Logger,
wenzelm@68308
    92
    dirs: List[Path] = Nil,
wenzelm@68308
    93
    select_dirs: List[Path] = Nil,
wenzelm@68316
    94
    output_dir: Path = default_output_dir,
wenzelm@68308
    95
    verbose: Boolean = false,
wenzelm@68936
    96
    commit_clean_delay: Time = default_commit_clean_delay,
wenzelm@68945
    97
    watchdog_timeout: Time = default_watchdog_timeout,
wenzelm@68308
    98
    system_mode: Boolean = false,
wenzelm@68308
    99
    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
wenzelm@68308
   100
  {
wenzelm@68537
   101
    if (Build.build_logic(options, logic, build_heap = true, progress = progress,
wenzelm@68743
   102
      dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
wenzelm@68308
   103
wenzelm@68416
   104
    val dump_options = make_options(options, aspects)
wenzelm@68308
   105
wenzelm@68318
   106
wenzelm@68318
   107
    /* dependencies */
wenzelm@68318
   108
wenzelm@68308
   109
    val deps =
wenzelm@68308
   110
      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
wenzelm@68308
   111
        selection_deps(selection)
wenzelm@68308
   112
wenzelm@68318
   113
    val include_sessions =
wenzelm@68318
   114
      deps.sessions_structure.imports_topological_order
wenzelm@68318
   115
wenzelm@68318
   116
    val use_theories =
wenzelm@68318
   117
      deps.sessions_structure.build_topological_order.
wenzelm@68318
   118
        flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
wenzelm@68318
   119
wenzelm@68318
   120
wenzelm@68926
   121
    /* dump aspects asynchronously */
wenzelm@68926
   122
wenzelm@68926
   123
    object Consumer
wenzelm@68926
   124
    {
wenzelm@68930
   125
      private val consumer_ok = Synchronized(true)
wenzelm@68926
   126
wenzelm@68926
   127
      private val consumer =
wenzelm@68926
   128
        Consumer_Thread.fork(name = "dump")(
wenzelm@68926
   129
          consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
wenzelm@68926
   130
            {
wenzelm@68926
   131
              val (snapshot, node_status) = args
wenzelm@68926
   132
              if (node_status.ok) {
wenzelm@68926
   133
                val aspect_args =
wenzelm@68929
   134
                  Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
wenzelm@68926
   135
                aspects.foreach(_.operation(aspect_args))
wenzelm@68926
   136
              }
wenzelm@68930
   137
              else {
wenzelm@68930
   138
                consumer_ok.change(_ => false)
wenzelm@68930
   139
                for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
wenzelm@68930
   140
                  val msg = XML.content(Pretty.formatted(List(tree)))
wenzelm@68930
   141
                  progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg)
wenzelm@68930
   142
                }
wenzelm@68926
   143
              }
wenzelm@68926
   144
              true
wenzelm@68926
   145
            })
wenzelm@68926
   146
wenzelm@68926
   147
      def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
wenzelm@68926
   148
        consumer.send((snapshot, node_status))
wenzelm@68926
   149
wenzelm@68930
   150
      def shutdown(): Boolean =
wenzelm@68926
   151
      {
wenzelm@68926
   152
        consumer.shutdown()
wenzelm@68930
   153
        consumer_ok.value
wenzelm@68926
   154
      }
wenzelm@68926
   155
    }
wenzelm@68926
   156
wenzelm@68926
   157
wenzelm@68318
   158
    /* session */
wenzelm@68318
   159
wenzelm@68308
   160
    val session =
wenzelm@68743
   161
      Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
wenzelm@68318
   162
        include_sessions = include_sessions, progress = progress, log = log)
wenzelm@68308
   163
wenzelm@68926
   164
    val theories_result =
wenzelm@68936
   165
      session.use_theories(use_theories,
wenzelm@68936
   166
        progress = progress,
wenzelm@68936
   167
        commit = Some(Consumer.apply _),
wenzelm@68945
   168
        commit_clean_delay = commit_clean_delay,
wenzelm@68945
   169
        watchdog_timeout = watchdog_timeout)
wenzelm@68926
   170
wenzelm@68320
   171
    val session_result = session.stop()
wenzelm@68320
   172
wenzelm@68930
   173
    val consumer_ok = Consumer.shutdown()
wenzelm@68320
   174
wenzelm@68930
   175
    if (theories_result.ok && consumer_ok) session_result
wenzelm@68930
   176
    else session_result.error_rc
wenzelm@68308
   177
  }
wenzelm@68308
   178
wenzelm@68308
   179
wenzelm@68308
   180
  /* Isabelle tool wrapper */
wenzelm@68308
   181
wenzelm@68308
   182
  val isabelle_tool =
wenzelm@68348
   183
    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
wenzelm@68308
   184
    {
wenzelm@68345
   185
      var aspects: List[Aspect] = known_aspects
wenzelm@68308
   186
      var base_sessions: List[String] = Nil
wenzelm@68936
   187
      var commit_clean_delay = default_commit_clean_delay
wenzelm@68308
   188
      var select_dirs: List[Path] = Nil
wenzelm@68316
   189
      var output_dir = default_output_dir
wenzelm@68308
   190
      var requirements = false
wenzelm@68945
   191
      var watchdog_timeout = default_watchdog_timeout
wenzelm@68308
   192
      var exclude_session_groups: List[String] = Nil
wenzelm@68308
   193
      var all_sessions = false
wenzelm@68308
   194
      var dirs: List[Path] = Nil
wenzelm@68308
   195
      var session_groups: List[String] = Nil
wenzelm@68308
   196
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@68308
   197
      var options = Options.init()
wenzelm@68308
   198
      var system_mode = false
wenzelm@68308
   199
      var verbose = false
wenzelm@68308
   200
      var exclude_sessions: List[String] = Nil
wenzelm@68308
   201
wenzelm@68308
   202
      val getopts = Getopts("""
wenzelm@68308
   203
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
wenzelm@68308
   204
wenzelm@68308
   205
  Options are:
wenzelm@68345
   206
    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
wenzelm@68308
   207
    -B NAME      include session NAME and all descendants
wenzelm@68936
   208
    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
wenzelm@68946
   209
      Value.Seconds(default_commit_clean_delay) + """)
wenzelm@68308
   210
    -D DIR       include session directory and select its sessions
wenzelm@68316
   211
    -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
wenzelm@68308
   212
    -R           operate on requirements of selected sessions
wenzelm@68946
   213
    -W SECONDS   delay for cleaning of already dumped theories (unlimited for 0, default: """ +
wenzelm@68946
   214
      Value.Seconds(default_watchdog_timeout) + """)
wenzelm@68308
   215
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@68308
   216
    -a           select all sessions
wenzelm@68308
   217
    -d DIR       include session directory
wenzelm@68308
   218
    -g NAME      select session group NAME
wenzelm@68308
   219
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@68308
   220
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@68308
   221
    -s           system build mode for logic image
wenzelm@68308
   222
    -v           verbose
wenzelm@68308
   223
    -x NAME      exclude session NAME and all descendants
wenzelm@68308
   224
wenzelm@68348
   225
  Dump cumulative PIDE session database, with the following aspects:
wenzelm@68316
   226
wenzelm@68316
   227
""" + Library.prefix_lines("    ", show_aspects) + "\n",
wenzelm@68316
   228
      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
wenzelm@68308
   229
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
wenzelm@68944
   230
      "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
wenzelm@68308
   231
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@68316
   232
      "O:" -> (arg => output_dir = Path.explode(arg)),
wenzelm@68308
   233
      "R" -> (_ => requirements = true),
wenzelm@68945
   234
      "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
wenzelm@68308
   235
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@68308
   236
      "a" -> (_ => all_sessions = true),
wenzelm@68308
   237
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@68741
   238
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@68308
   239
      "l:" -> (arg => logic = arg),
wenzelm@68308
   240
      "o:" -> (arg => options = options + arg),
wenzelm@68308
   241
      "s" -> (_ => system_mode = true),
wenzelm@68308
   242
      "v" -> (_ => verbose = true),
wenzelm@68308
   243
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@68308
   244
wenzelm@68308
   245
      val sessions = getopts(args)
wenzelm@68308
   246
wenzelm@68941
   247
      val progress = new Console_Progress()
wenzelm@68899
   248
      {
wenzelm@68899
   249
        override def theory_percentage(session: String, theory: String, percentage: Int)
wenzelm@68899
   250
        {
wenzelm@68899
   251
          if (verbose) echo(Progress.theory_message(session, theory) + ": " + percentage + "%")
wenzelm@68899
   252
        }
wenzelm@68899
   253
      }
wenzelm@68308
   254
wenzelm@68308
   255
      val result =
wenzelm@68331
   256
        progress.interrupt_handler {
wenzelm@68331
   257
          dump(options, logic,
wenzelm@68331
   258
            aspects = aspects,
wenzelm@68331
   259
            progress = progress,
wenzelm@68331
   260
            dirs = dirs,
wenzelm@68331
   261
            select_dirs = select_dirs,
wenzelm@68331
   262
            output_dir = output_dir,
wenzelm@68936
   263
            commit_clean_delay = commit_clean_delay,
wenzelm@68945
   264
            watchdog_timeout = watchdog_timeout,
wenzelm@68331
   265
            verbose = verbose,
wenzelm@68331
   266
            selection = Sessions.Selection(
wenzelm@68331
   267
              requirements = requirements,
wenzelm@68331
   268
              all_sessions = all_sessions,
wenzelm@68331
   269
              base_sessions = base_sessions,
wenzelm@68331
   270
              exclude_session_groups = exclude_session_groups,
wenzelm@68331
   271
              exclude_sessions = exclude_sessions,
wenzelm@68331
   272
              session_groups = session_groups,
wenzelm@68331
   273
              sessions = sessions))
wenzelm@68331
   274
        }
wenzelm@68308
   275
wenzelm@68308
   276
      progress.echo(result.timing.message_resources)
wenzelm@68308
   277
wenzelm@68308
   278
      sys.exit(result.rc)
wenzelm@68308
   279
    })
wenzelm@68308
   280
}