1/*  Title:      Pure/Tools/dump.scala
2    Author:     Makarius
3
4Dump cumulative PIDE session database.
5*/
6
7package isabelle
8
9import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter}
10
11
12object Dump
13{
14  /* aspects */
15
16  sealed case class Aspect_Args(
17    options: Options,
18    deps: Sessions.Deps,
19    progress: Progress,
20    output_dir: Path,
21    snapshot: Document.Snapshot,
22    status: Document_Status.Node_Status)
23  {
24    def write_path(file_name: Path): Path =
25    {
26      val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
27      Isabelle_System.mkdirs(path.dir)
28      path
29    }
30
31    def write(file_name: Path, bytes: Bytes): Unit =
32      Bytes.write(write_path(file_name), bytes)
33
34    def write(file_name: Path, text: String): Unit =
35      write(file_name, Bytes(text))
36
37    def write(file_name: Path, body: XML.Body): Unit =
38      using(File.writer(write_path(file_name).file))(
39        writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
40  }
41
42  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
43    options: List[String] = Nil)
44  {
45    override def toString: String = name
46  }
47
48  val known_aspects: List[Aspect] =
49    List(
50      Aspect("markup", "PIDE markup (YXML format)",
51        { case args =>
52            args.write(Path.explode("markup.yxml"),
53              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
54        }),
55      Aspect("messages", "output messages (YXML format)",
56        { case args =>
57            args.write(Path.explode("messages.yxml"),
58              args.snapshot.messages.iterator.map(_._1).toList)
59        }),
60      Aspect("latex", "generated LaTeX source",
61        { case args =>
62            for (entry <- args.snapshot.exports if entry.name == "document.tex")
63              args.write(Path.explode(entry.name), entry.uncompressed())
64        }, options = List("export_document")),
65      Aspect("theory", "foundational theory content",
66        { case args =>
67            for {
68              entry <- args.snapshot.exports
69              if entry.name.startsWith(Export_Theory.export_prefix)
70            } args.write(Path.explode(entry.name), entry.uncompressed())
71        }, options = List("export_theory"))
72    ).sortBy(_.name)
73
74  def show_aspects: String =
75    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
76
77  def the_aspect(name: String): Aspect =
78    known_aspects.find(aspect => aspect.name == name) getOrElse
79      error("Unknown aspect " + quote(name))
80
81
82  /* context and session */
83
84  sealed case class Args(
85    session: Headless.Session,
86    snapshot: Document.Snapshot,
87    status: Document_Status.Node_Status)
88  {
89    def print_node: String = snapshot.node_name.toString
90  }
91
92  object Context
93  {
94    def apply(
95      options: Options,
96      aspects: List[Aspect] = Nil,
97      progress: Progress = No_Progress,
98      dirs: List[Path] = Nil,
99      select_dirs: List[Path] = Nil,
100      selection: Sessions.Selection = Sessions.Selection.empty,
101      pure_base: Boolean = false,
102      skip_base: Boolean = false): Context =
103    {
104      val session_options: Options =
105      {
106        val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
107        val options1 =
108          options0 +
109            "completion_limit=0" +
110            "ML_statistics=false" +
111            "parallel_proofs=0" +
112            "editor_tracing_messages=0" +
113            "editor_presentation"
114        (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
115      }
116
117      val sessions_structure: Sessions.Structure =
118        Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs).
119          selection(selection)
120
121      {
122        val selection_size = sessions_structure.build_graph.size
123        if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
124      }
125
126      val deps: Sessions.Deps =
127        Sessions.deps(sessions_structure, progress = progress).check_errors
128
129      new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps)
130    }
131  }
132
133  class Context private(
134    val options: Options,
135    val progress: Progress,
136    val dirs: List[Path],
137    val select_dirs: List[Path],
138    val pure_base: Boolean,
139    val skip_base: Boolean,
140    val session_options: Options,
141    val deps: Sessions.Deps)
142  {
143    context =>
144
145    def session_dirs: List[Path] = dirs ::: select_dirs
146
147    def build_logic(logic: String)
148    {
149      Build.build_logic(options, logic, build_heap = true, progress = progress,
150        dirs = session_dirs, strict = true)
151    }
152
153    def sessions(
154      logic: String = default_logic,
155      log: Logger = No_Logger): List[Session] =
156    {
157      /* partitions */
158
159      def session_info(session_name: String): Sessions.Info =
160        deps.sessions_structure(session_name)
161
162      val session_graph = deps.sessions_structure.build_graph
163      val all_sessions = session_graph.topological_order
164
165      val afp_sessions =
166        (for (name <- all_sessions if session_info(name).is_afp) yield name).toSet
167
168      val afp_bulky_sessions =
169        (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList
170
171      val base_sessions =
172        session_graph.all_preds(List(logic).filter(session_graph.defined)).reverse
173
174      val proof_sessions =
175        session_graph.all_succs(
176          for (name <- all_sessions if session_info(name).record_proofs) yield name)
177
178
179      /* resulting sessions */
180
181      def make_session(
182        selected_sessions: List[String],
183        session_logic: String = logic,
184        strict: Boolean = false,
185        record_proofs: Boolean = false): List[Session] =
186      {
187        if (selected_sessions.isEmpty && !strict) Nil
188        else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
189      }
190
191      val PURE = isabelle.Thy_Header.PURE
192
193      val base =
194        if ((logic == PURE && !pure_base) || skip_base) Nil
195        else make_session(base_sessions, session_logic = PURE, strict = logic == PURE)
196
197      val main =
198        make_session(
199          session_graph.topological_order.filterNot(name =>
200            afp_sessions.contains(name) ||
201            base_sessions.contains(name) ||
202            proof_sessions.contains(name)))
203
204      val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true)
205
206      val afp =
207        if (afp_sessions.isEmpty) Nil
208        else {
209          val (part1, part2) =
210          {
211            val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions)
212            val force_partition1 = AFP.force_partition1.filter(graph.defined)
213            val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet
214            graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
215          }
216          List(part1, part2, afp_bulky_sessions).flatMap(make_session(_))
217        }
218
219      proofs ::: base ::: main ::: afp
220    }
221
222
223    /* processed theories */
224
225    private val processed_theories = Synchronized(Set.empty[String])
226
227    def process_theory(theory: String): Boolean =
228      processed_theories.change_result(processed => (!processed(theory), processed + theory))
229
230
231    /* errors */
232
233    private val errors = Synchronized(List.empty[String])
234
235    def add_errors(more_errs: List[String])
236    {
237      errors.change(errs => errs ::: more_errs)
238    }
239
240    def check_errors
241    {
242      val errs = errors.value
243      if (errs.nonEmpty) error(errs.mkString("\n\n"))
244    }
245  }
246
247  class Session private[Dump](
248    val context: Context,
249    val logic: String,
250    log: Logger,
251    selected_sessions: List[String],
252    record_proofs: Boolean)
253  {
254    /* resources */
255
256    val options: Options =
257      if (record_proofs) context.session_options + "record_proofs=2"
258      else context.session_options
259
260    private def deps = context.deps
261    private def progress = context.progress
262
263    val resources: Headless.Resources =
264      Headless.Resources.make(options, logic, progress = progress, log = log,
265        session_dirs = context.session_dirs,
266        include_sessions = deps.sessions_structure.imports_topological_order)
267
268    val used_theories: List[Document.Node.Name] =
269    {
270      for {
271        session_name <-
272          deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
273        (name, theory_options) <- deps(session_name).used_theories
274        if !resources.session_base.loaded_theory(name.theory)
275        if {
276          def warn(msg: String): Unit =
277            progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
278
279          val conditions =
280            space_explode(',', theory_options.string("condition")).
281              filter(cond => Isabelle_System.getenv(cond) == "")
282          if (conditions.nonEmpty) {
283            warn("undefined " + conditions.mkString(", "))
284            false
285          }
286          else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) {
287            warn("option skip_proofs")
288            false
289          }
290          else true
291        }
292      } yield name
293    }
294
295
296    /* process */
297
298    def process(process_theory: Args => Unit, unicode_symbols: Boolean = false)
299    {
300      val session = resources.start_session(progress = progress)
301
302
303      // asynchronous consumer
304
305      object Consumer
306      {
307        sealed case class Bad_Theory(
308          name: Document.Node.Name,
309          status: Document_Status.Node_Status,
310          errors: List[String])
311
312        private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
313
314        private val consumer =
315          Consumer_Thread.fork(name = "dump")(
316            consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
317              {
318                val (snapshot, status) = args
319                val name = snapshot.node_name
320                if (status.ok) {
321                  try {
322                    if (context.process_theory(name.theory)) {
323                      process_theory(Args(session, snapshot, status))
324                    }
325                  }
326                  catch {
327                    case exn: Throwable if !Exn.is_interrupt(exn) =>
328                      val msg = Exn.message(exn)
329                      progress.echo("FAILED to process theory " + name)
330                      progress.echo_error_message(msg)
331                      consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
332                  }
333                }
334                else {
335                  val msgs =
336                    for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
337                    yield {
338                      "Error" + Position.here(pos) + ":\n" +
339                        XML.content(Pretty.formatted(List(tree)))
340                    }
341                  progress.echo("FAILED to process theory " + name)
342                  msgs.foreach(progress.echo_error_message)
343                  consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
344                }
345                true
346              })
347
348        def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
349          consumer.send((snapshot, status))
350
351        def shutdown(): List[Bad_Theory] =
352        {
353          consumer.shutdown()
354          consumer_bad_theories.value.reverse
355        }
356      }
357
358
359      // synchronous body
360
361      try {
362        val use_theories_result =
363          session.use_theories(used_theories.map(_.theory),
364            unicode_symbols = unicode_symbols,
365            progress = progress,
366            commit = Some(Consumer.apply _))
367
368        val bad_theories = Consumer.shutdown()
369        val bad_msgs =
370          bad_theories.map(bad =>
371            Output.clean_yxml(
372              "FAILED theory " + bad.name +
373                (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
374                (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
375
376        val pending_msgs =
377          use_theories_result.nodes_pending match {
378            case Nil => Nil
379            case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString)))
380          }
381
382        context.add_errors(bad_msgs ::: pending_msgs)
383      }
384      finally { session.stop() }
385    }
386  }
387
388
389  /* dump */
390
391  val default_output_dir: Path = Path.explode("dump")
392  val default_logic: String = Thy_Header.PURE
393
394  def dump(
395    options: Options,
396    logic: String,
397    aspects: List[Aspect] = Nil,
398    progress: Progress = No_Progress,
399    log: Logger = No_Logger,
400    dirs: List[Path] = Nil,
401    select_dirs: List[Path] = Nil,
402    output_dir: Path = default_output_dir,
403    selection: Sessions.Selection = Sessions.Selection.empty)
404  {
405    val context =
406      Context(options, aspects = aspects, progress = progress, dirs = dirs,
407        select_dirs = select_dirs, selection = selection)
408
409    context.build_logic(logic)
410
411    for (session <- context.sessions(logic = logic, log = log)) {
412      session.process((args: Args) =>
413        {
414          progress.echo("Processing theory " + args.print_node + " ...")
415          val aspect_args =
416            Aspect_Args(session.options, context.deps, progress, output_dir,
417              args.snapshot, args.status)
418          aspects.foreach(_.operation(aspect_args))
419        })
420    }
421
422    context.check_errors
423  }
424
425
426  /* Isabelle tool wrapper */
427
428  val isabelle_tool =
429    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
430    {
431      var aspects: List[Aspect] = known_aspects
432      var base_sessions: List[String] = Nil
433      var select_dirs: List[Path] = Nil
434      var output_dir = default_output_dir
435      var requirements = false
436      var exclude_session_groups: List[String] = Nil
437      var all_sessions = false
438      var logic = default_logic
439      var dirs: List[Path] = Nil
440      var session_groups: List[String] = Nil
441      var options = Options.init()
442      var verbose = false
443      var exclude_sessions: List[String] = Nil
444
445      val getopts = Getopts("""
446Usage: isabelle dump [OPTIONS] [SESSIONS ...]
447
448  Options are:
449    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
450    -B NAME      include session NAME and all descendants
451    -D DIR       include session directory and select its sessions
452    -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
453    -R           operate on requirements of selected sessions
454    -X NAME      exclude sessions from group NAME and all descendants
455    -a           select all sessions
456    -b NAME      base logic image (default """ + isabelle.quote(default_logic) + """)
457    -d DIR       include session directory
458    -g NAME      select session group NAME
459    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
460    -v           verbose
461    -x NAME      exclude session NAME and all descendants
462
463  Dump cumulative PIDE session database, with the following aspects:
464
465""" + Library.prefix_lines("    ", show_aspects) + "\n",
466      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
467      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
468      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
469      "O:" -> (arg => output_dir = Path.explode(arg)),
470      "R" -> (_ => requirements = true),
471      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
472      "a" -> (_ => all_sessions = true),
473      "b:" -> (arg => logic = arg),
474      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
475      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
476      "o:" -> (arg => options = options + arg),
477      "v" -> (_ => verbose = true),
478      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
479
480      val sessions = getopts(args)
481
482      val progress = new Console_Progress(verbose = verbose)
483
484      val start_date = Date.now()
485
486      if (verbose) progress.echo("Started at " + Build_Log.print_date(start_date))
487
488      progress.interrupt_handler {
489        dump(options, logic,
490          aspects = aspects,
491          progress = progress,
492          dirs = dirs,
493          select_dirs = select_dirs,
494          output_dir = output_dir,
495          selection = Sessions.Selection(
496            requirements = requirements,
497            all_sessions = all_sessions,
498            base_sessions = base_sessions,
499            exclude_session_groups = exclude_session_groups,
500            exclude_sessions = exclude_sessions,
501            session_groups = session_groups,
502            sessions = sessions))
503      }
504
505      val end_date = Date.now()
506      val timing = end_date.time - start_date.time
507
508      if (verbose) progress.echo("\nFinished at " + Build_Log.print_date(end_date))
509      progress.echo(timing.message_hms + " elapsed time")
510    })
511}
512