src/Pure/Tools/dump.scala
author wenzelm
Mon Sep 03 20:04:51 2018 +0200 (10 months ago)
changeset 68899 b15b03c13dbb
parent 68896 e63eaae13165
child 68926 5129fcc1b6c0
permissions -rw-r--r--
more detailed progress;
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@68365
    19
    node_name: Document.Node.Name,
wenzelm@68758
    20
    node_status: Document_Status.Node_Status,
wenzelm@68365
    21
    snapshot: Document.Snapshot)
wenzelm@68319
    22
  {
wenzelm@68365
    23
    def write(file_name: Path, bytes: Bytes)
wenzelm@68319
    24
    {
wenzelm@68347
    25
      val path = output_dir + Path.basic(node_name.theory) + file_name
wenzelm@68319
    26
      Isabelle_System.mkdirs(path.dir)
wenzelm@68319
    27
      Bytes.write(path, bytes)
wenzelm@68319
    28
    }
wenzelm@68319
    29
wenzelm@68365
    30
    def write(file_name: Path, text: String): Unit =
wenzelm@68365
    31
      write(file_name, Bytes(text))
wenzelm@68332
    32
wenzelm@68365
    33
    def write(file_name: Path, body: XML.Body): Unit =
wenzelm@68365
    34
      write(file_name, Symbol.encode(YXML.string_of_body(body)))
wenzelm@68319
    35
  }
wenzelm@68316
    36
wenzelm@68347
    37
  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
wenzelm@68347
    38
    options: List[String] = Nil)
wenzelm@68345
    39
  {
wenzelm@68345
    40
    override def toString: String = name
wenzelm@68345
    41
  }
wenzelm@68316
    42
wenzelm@68347
    43
  val known_aspects =
wenzelm@68316
    44
    List(
wenzelm@68365
    45
      Aspect("markup", "PIDE markup (YXML format)",
wenzelm@68365
    46
        { case args =>
wenzelm@68365
    47
            args.write(Path.explode("markup.yxml"),
wenzelm@68365
    48
              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
wenzelm@68365
    49
        }),
wenzelm@68319
    50
      Aspect("messages", "output messages (YXML format)",
wenzelm@68319
    51
        { case args =>
wenzelm@68365
    52
            args.write(Path.explode("messages.yxml"),
wenzelm@68365
    53
              args.snapshot.messages.iterator.map(_._1).toList)
wenzelm@68347
    54
        }),
wenzelm@68347
    55
      Aspect("latex", "generated LaTeX source",
wenzelm@68347
    56
        { case args =>
wenzelm@68365
    57
            for (entry <- args.snapshot.exports if entry.name == "document.tex")
wenzelm@68365
    58
              args.write(Path.explode(entry.name), entry.uncompressed())
wenzelm@68491
    59
        }, options = List("editor_presentation", "export_document")),
wenzelm@68347
    60
      Aspect("theory", "foundational theory content",
wenzelm@68347
    61
        { case args =>
wenzelm@68347
    62
            for {
wenzelm@68365
    63
              entry <- args.snapshot.exports
wenzelm@68347
    64
              if entry.name.startsWith(Export_Theory.export_prefix)
wenzelm@68365
    65
            } args.write(Path.explode(entry.name), entry.uncompressed())
wenzelm@68347
    66
        }, options = List("editor_presentation", "export_theory"))
wenzelm@68345
    67
    ).sortBy(_.name)
wenzelm@68316
    68
wenzelm@68316
    69
  def show_aspects: String =
wenzelm@68345
    70
    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
wenzelm@68316
    71
wenzelm@68316
    72
  def the_aspect(name: String): Aspect =
wenzelm@68316
    73
    known_aspects.find(aspect => aspect.name == name) getOrElse
wenzelm@68316
    74
      error("Unknown aspect " + quote(name))
wenzelm@68316
    75
wenzelm@68316
    76
wenzelm@68316
    77
  /* dump */
wenzelm@68316
    78
wenzelm@68316
    79
  val default_output_dir = Path.explode("dump")
wenzelm@68316
    80
wenzelm@68416
    81
  def make_options(options: Options, aspects: List[Aspect]): Options =
wenzelm@68895
    82
  {
wenzelm@68896
    83
    val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
wenzelm@68895
    84
    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
wenzelm@68895
    85
  }
wenzelm@68416
    86
wenzelm@68308
    87
  def dump(options: Options, logic: String,
wenzelm@68316
    88
    aspects: List[Aspect] = Nil,
wenzelm@68308
    89
    progress: Progress = No_Progress,
wenzelm@68308
    90
    log: Logger = No_Logger,
wenzelm@68308
    91
    dirs: List[Path] = Nil,
wenzelm@68308
    92
    select_dirs: List[Path] = Nil,
wenzelm@68316
    93
    output_dir: Path = default_output_dir,
wenzelm@68308
    94
    verbose: Boolean = false,
wenzelm@68308
    95
    system_mode: Boolean = false,
wenzelm@68308
    96
    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
wenzelm@68308
    97
  {
wenzelm@68537
    98
    if (Build.build_logic(options, logic, build_heap = true, progress = progress,
wenzelm@68743
    99
      dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
wenzelm@68308
   100
wenzelm@68416
   101
    val dump_options = make_options(options, aspects)
wenzelm@68308
   102
wenzelm@68318
   103
wenzelm@68318
   104
    /* dependencies */
wenzelm@68318
   105
wenzelm@68308
   106
    val deps =
wenzelm@68308
   107
      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
wenzelm@68308
   108
        selection_deps(selection)
wenzelm@68308
   109
wenzelm@68318
   110
    val include_sessions =
wenzelm@68318
   111
      deps.sessions_structure.imports_topological_order
wenzelm@68318
   112
wenzelm@68318
   113
    val use_theories =
wenzelm@68318
   114
      deps.sessions_structure.build_topological_order.
wenzelm@68318
   115
        flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
wenzelm@68318
   116
wenzelm@68318
   117
wenzelm@68318
   118
    /* session */
wenzelm@68318
   119
wenzelm@68308
   120
    val session =
wenzelm@68743
   121
      Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
wenzelm@68318
   122
        include_sessions = include_sessions, progress = progress, log = log)
wenzelm@68308
   123
wenzelm@68320
   124
    val theories_result = session.use_theories(use_theories, progress = progress)
wenzelm@68320
   125
    val session_result = session.stop()
wenzelm@68320
   126
wenzelm@68320
   127
wenzelm@68320
   128
    /* dump aspects */
wenzelm@68320
   129
wenzelm@68365
   130
    for ((node_name, node_status) <- theories_result.nodes) {
wenzelm@68365
   131
      val snapshot = theories_result.snapshot(node_name)
wenzelm@68365
   132
      val aspect_args =
wenzelm@68365
   133
        Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
wenzelm@68365
   134
      aspects.foreach(_.operation(aspect_args))
wenzelm@68365
   135
    }
wenzelm@68320
   136
wenzelm@68557
   137
    if (theories_result.ok) session_result
wenzelm@68557
   138
    else {
wenzelm@68557
   139
      for {
wenzelm@68557
   140
        (name, status) <- theories_result.nodes if !status.ok
wenzelm@68884
   141
        (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
wenzelm@68557
   142
      } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
wenzelm@68557
   143
wenzelm@68557
   144
      session_result.copy(rc = session_result.rc max 1)
wenzelm@68557
   145
    }
wenzelm@68308
   146
  }
wenzelm@68308
   147
wenzelm@68308
   148
wenzelm@68308
   149
  /* Isabelle tool wrapper */
wenzelm@68308
   150
wenzelm@68308
   151
  val isabelle_tool =
wenzelm@68348
   152
    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
wenzelm@68308
   153
    {
wenzelm@68345
   154
      var aspects: List[Aspect] = known_aspects
wenzelm@68308
   155
      var base_sessions: List[String] = Nil
wenzelm@68308
   156
      var select_dirs: List[Path] = Nil
wenzelm@68316
   157
      var output_dir = default_output_dir
wenzelm@68308
   158
      var requirements = false
wenzelm@68308
   159
      var exclude_session_groups: List[String] = Nil
wenzelm@68308
   160
      var all_sessions = false
wenzelm@68308
   161
      var dirs: List[Path] = Nil
wenzelm@68308
   162
      var session_groups: List[String] = Nil
wenzelm@68308
   163
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@68308
   164
      var options = Options.init()
wenzelm@68308
   165
      var system_mode = false
wenzelm@68308
   166
      var verbose = false
wenzelm@68308
   167
      var exclude_sessions: List[String] = Nil
wenzelm@68308
   168
wenzelm@68308
   169
      val getopts = Getopts("""
wenzelm@68308
   170
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
wenzelm@68308
   171
wenzelm@68308
   172
  Options are:
wenzelm@68345
   173
    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
wenzelm@68308
   174
    -B NAME      include session NAME and all descendants
wenzelm@68308
   175
    -D DIR       include session directory and select its sessions
wenzelm@68316
   176
    -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
wenzelm@68308
   177
    -R           operate on requirements of selected sessions
wenzelm@68308
   178
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@68308
   179
    -a           select all sessions
wenzelm@68308
   180
    -d DIR       include session directory
wenzelm@68308
   181
    -g NAME      select session group NAME
wenzelm@68308
   182
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@68308
   183
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@68308
   184
    -s           system build mode for logic image
wenzelm@68308
   185
    -v           verbose
wenzelm@68308
   186
    -x NAME      exclude session NAME and all descendants
wenzelm@68308
   187
wenzelm@68348
   188
  Dump cumulative PIDE session database, with the following aspects:
wenzelm@68316
   189
wenzelm@68316
   190
""" + Library.prefix_lines("    ", show_aspects) + "\n",
wenzelm@68316
   191
      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
wenzelm@68308
   192
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
wenzelm@68308
   193
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@68316
   194
      "O:" -> (arg => output_dir = Path.explode(arg)),
wenzelm@68308
   195
      "R" -> (_ => requirements = true),
wenzelm@68308
   196
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@68308
   197
      "a" -> (_ => all_sessions = true),
wenzelm@68308
   198
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@68741
   199
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@68308
   200
      "l:" -> (arg => logic = arg),
wenzelm@68308
   201
      "o:" -> (arg => options = options + arg),
wenzelm@68308
   202
      "s" -> (_ => system_mode = true),
wenzelm@68308
   203
      "v" -> (_ => verbose = true),
wenzelm@68308
   204
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@68308
   205
wenzelm@68308
   206
      val sessions = getopts(args)
wenzelm@68308
   207
wenzelm@68308
   208
      val progress = new Console_Progress(verbose = verbose)
wenzelm@68899
   209
      {
wenzelm@68899
   210
        override def theory_percentage(session: String, theory: String, percentage: Int)
wenzelm@68899
   211
        {
wenzelm@68899
   212
          if (verbose) echo(Progress.theory_message(session, theory) + ": " + percentage + "%")
wenzelm@68899
   213
        }
wenzelm@68899
   214
      }
wenzelm@68308
   215
wenzelm@68308
   216
      val result =
wenzelm@68331
   217
        progress.interrupt_handler {
wenzelm@68331
   218
          dump(options, logic,
wenzelm@68331
   219
            aspects = aspects,
wenzelm@68331
   220
            progress = progress,
wenzelm@68331
   221
            dirs = dirs,
wenzelm@68331
   222
            select_dirs = select_dirs,
wenzelm@68331
   223
            output_dir = output_dir,
wenzelm@68331
   224
            verbose = verbose,
wenzelm@68331
   225
            selection = Sessions.Selection(
wenzelm@68331
   226
              requirements = requirements,
wenzelm@68331
   227
              all_sessions = all_sessions,
wenzelm@68331
   228
              base_sessions = base_sessions,
wenzelm@68331
   229
              exclude_session_groups = exclude_session_groups,
wenzelm@68331
   230
              exclude_sessions = exclude_sessions,
wenzelm@68331
   231
              session_groups = session_groups,
wenzelm@68331
   232
              sessions = sessions))
wenzelm@68331
   233
        }
wenzelm@68308
   234
wenzelm@68308
   235
      progress.echo(result.timing.message_resources)
wenzelm@68308
   236
wenzelm@68308
   237
      sys.exit(result.rc)
wenzelm@68308
   238
    })
wenzelm@68308
   239
}