/* Title: Pure/Tools/dump.scala
Author: Makarius
Dump cumulative PIDE session database.
*/
package isabelle
import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter}
object Dump
{
/* aspects */
sealed case class Aspect_Args(
options: Options,
deps: Sessions.Deps,
progress: Progress,
output_dir: Path,
snapshot: Document.Snapshot,
status: Document_Status.Node_Status)
{
def write_path(file_name: Path): Path =
{
val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
Isabelle_System.make_directory(path.dir)
path
}
def write(file_name: Path, bytes: Bytes): Unit =
Bytes.write(write_path(file_name), bytes)
def write(file_name: Path, text: String): Unit =
write(file_name, Bytes(text))
def write(file_name: Path, body: XML.Body): Unit =
using(File.writer(write_path(file_name).file))(
writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
}
sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
options: List[String] = Nil)
{
override def toString: String = name
}
val known_aspects: List[Aspect] =
List(
Aspect("markup", "PIDE markup (YXML format)",
args => args.write(Path.explode(Export.MARKUP), args.snapshot.xml_markup())),
Aspect("messages", "output messages (YXML format)",
args => args.write(Path.explode(Export.MESSAGES), args.snapshot.messages.map(_._1))),
Aspect("latex", "generated LaTeX source",
args =>
for {
entry <- args.snapshot.exports
if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
} args.write(Path.explode(entry.name), entry.uncompressed)),
Aspect("theory", "foundational theory content",
args =>
for {
entry <- args.snapshot.exports
if entry.name_has_prefix(Export.THEORY_PREFIX)
} args.write(Path.explode(entry.name), entry.uncompressed),
options = List("export_theory"))
).sortBy(_.name)
def show_aspects: String =
cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
def the_aspect(name: String): Aspect =
known_aspects.find(aspect => aspect.name == name) getOrElse
error("Unknown aspect " + quote(name))
/* context and session */
sealed case class Args(
session: Headless.Session,
snapshot: Document.Snapshot,
status: Document_Status.Node_Status)
{
def print_node: String = snapshot.node_name.toString
}
object Context
{
def apply(
options: Options,
aspects: List[Aspect] = Nil,
progress: Progress = new Progress,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty,
pure_base: Boolean = false,
skip_base: Boolean = false): Context =
{
val session_options: Options =
{
val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
val options1 =
options0 +
"parallel_proofs=0" +
"completion_limit=0" +
"editor_tracing_messages=0" +
"editor_presentation"
(options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
}
val sessions_structure: Sessions.Structure =
Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs).
selection(selection)
{
val selection_size = sessions_structure.build_graph.size
if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
}
val deps: Sessions.Deps =
Sessions.deps(sessions_structure, progress = progress).check_errors
new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps)
}
}
class Context private(
val options: Options,
val progress: Progress,
val dirs: List[Path],
val select_dirs: List[Path],
val pure_base: Boolean,
val skip_base: Boolean,
val session_options: Options,
val deps: Sessions.Deps)
{
context =>
def session_dirs: List[Path] = dirs ::: select_dirs
def build_logic(logic: String)
{
Build.build_logic(options, logic, build_heap = true, progress = progress,
dirs = session_dirs, strict = true)
}
def sessions(
logic: String = default_logic,
log: Logger = No_Logger): List[Session] =
{
/* partitions */
def session_info(session_name: String): Sessions.Info =
deps.sessions_structure(session_name)
val session_graph = deps.sessions_structure.build_graph
val all_sessions = session_graph.topological_order
val afp_sessions =
(for (name <- all_sessions if session_info(name).is_afp) yield name).toSet
val afp_bulky_sessions =
(for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList
val base_sessions =
session_graph.all_preds_rev(List(logic).filter(session_graph.defined))
val proof_sessions =
session_graph.all_succs(
for (name <- all_sessions if session_info(name).record_proofs) yield name)
/* resulting sessions */
def make_session(
selected_sessions: List[String],
session_logic: String = logic,
strict: Boolean = false,
record_proofs: Boolean = false): List[Session] =
{
if (selected_sessions.isEmpty && !strict) Nil
else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
}
val PURE = isabelle.Thy_Header.PURE
val base =
if ((logic == PURE && !pure_base) || skip_base) Nil
else make_session(base_sessions, session_logic = PURE, strict = logic == PURE)
val main =
make_session(
session_graph.topological_order.filterNot(name =>
afp_sessions.contains(name) ||
base_sessions.contains(name) ||
proof_sessions.contains(name)))
val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true)
val afp =
if (afp_sessions.isEmpty) Nil
else {
val (part1, part2) =
{
val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions)
val force_partition1 = AFP.force_partition1.filter(graph.defined)
val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet
graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
}
List(part1, part2, afp_bulky_sessions).flatMap(make_session(_))
}
proofs ::: base ::: main ::: afp
}
/* processed theories */
private val processed_theories = Synchronized(Set.empty[String])
def process_theory(theory: String): Boolean =
processed_theories.change_result(processed => (!processed(theory), processed + theory))
/* errors */
private val errors = Synchronized(List.empty[String])
def add_errors(more_errs: List[String])
{
errors.change(errs => errs ::: more_errs)
}
def check_errors
{
val errs = errors.value
if (errs.nonEmpty) error(errs.mkString("\n\n"))
}
}
class Session private[Dump](
val context: Context,
val logic: String,
log: Logger,
selected_sessions: List[String],
record_proofs: Boolean)
{
/* resources */
val options: Options =
if (record_proofs) context.session_options + "record_proofs=2"
else context.session_options
private def deps = context.deps
private def progress = context.progress
val resources: Headless.Resources =
Headless.Resources.make(options, logic, progress = progress, log = log,
session_dirs = context.session_dirs,
include_sessions = deps.sessions_structure.imports_topological_order)
val used_theories: List[Document.Node.Name] =
{
for {
session_name <-
deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
(name, theory_options) <- deps(session_name).used_theories
if !resources.session_base.loaded_theory(name.theory)
if {
def warn(msg: String): Unit =
progress.echo_warning("Skipping theory " + name + " (" + msg + ")")
val conditions =
space_explode(',', theory_options.string("condition")).
filter(cond => Isabelle_System.getenv(cond) == "")
if (conditions.nonEmpty) {
warn("undefined " + conditions.mkString(", "))
false
}
else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) {
warn("option skip_proofs")
false
}
else true
}
} yield name
}
/* process */
def process(process_theory: Args => Unit, unicode_symbols: Boolean = false)
{
val session = resources.start_session(progress = progress)
// asynchronous consumer
object Consumer
{
sealed case class Bad_Theory(
name: Document.Node.Name,
status: Document_Status.Node_Status,
errors: List[String])
private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
private val consumer =
Consumer_Thread.fork(name = "dump")(
consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
{
val (snapshot, status) = args
val name = snapshot.node_name
if (status.ok) {
try {
if (context.process_theory(name.theory)) {
process_theory(Args(session, snapshot, status))
}
}
catch {
case exn: Throwable if !Exn.is_interrupt(exn) =>
val msg = Exn.message(exn)
progress.echo("FAILED to process theory " + name)
progress.echo_error_message(msg)
consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
}
}
else {
val msgs =
for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
yield {
"Error" + Position.here(pos) + ":\n" +
XML.content(Pretty.formatted(List(tree)))
}
progress.echo("FAILED to process theory " + name)
msgs.foreach(progress.echo_error_message)
consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
}
true
})
def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
consumer.send((snapshot, status))
def shutdown(): List[Bad_Theory] =
{
consumer.shutdown()
consumer_bad_theories.value.reverse
}
}
// synchronous body
try {
val use_theories_result =
session.use_theories(used_theories.map(_.theory),
unicode_symbols = unicode_symbols,
progress = progress,
commit = Some(Consumer.apply))
val bad_theories = Consumer.shutdown()
val bad_msgs =
bad_theories.map(bad =>
Output.clean_yxml(
"FAILED theory " + bad.name +
(if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
(if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
val pending_msgs =
use_theories_result.nodes_pending match {
case Nil => Nil
case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString)))
}
context.add_errors(bad_msgs ::: pending_msgs)
}
finally { session.stop() }
}
}
/* dump */
val default_output_dir: Path = Path.explode("dump")
val default_logic: String = Thy_Header.PURE
def dump(
options: Options,
logic: String,
aspects: List[Aspect] = Nil,
progress: Progress = new Progress,
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
selection: Sessions.Selection = Sessions.Selection.empty)
{
val context =
Context(options, aspects = aspects, progress = progress, dirs = dirs,
select_dirs = select_dirs, selection = selection)
context.build_logic(logic)
for (session <- context.sessions(logic = logic, log = log)) {
session.process((args: Args) =>
{
progress.echo("Processing theory " + args.print_node + " ...")
val aspect_args =
Aspect_Args(session.options, context.deps, progress, output_dir,
args.snapshot, args.status)
aspects.foreach(_.operation(aspect_args))
})
}
context.check_errors
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here, args =>
{
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var output_dir = default_output_dir
var requirements = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var logic = default_logic
var dirs: List[Path] = Nil
var session_groups: List[String] = Nil
var options = Options.init()
var verbose = false
var exclude_sessions: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
Options are:
-A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: """ + default_output_dir + """)
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b NAME base logic image (default """ + isabelle.quote(default_logic) + """)
-d DIR include session directory
-g NAME select session group NAME
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
Dump cumulative PIDE session database, with the following aspects:
""" + Library.prefix_lines(" ", show_aspects) + "\n",
"A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)),
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"O:" -> (arg => output_dir = Path.explode(arg)),
"R" -> (_ => requirements = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
"b:" -> (arg => logic = arg),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
val sessions = getopts(args)
val progress = new Console_Progress(verbose = verbose)
val start_date = Date.now()
progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
progress.interrupt_handler {
dump(options, logic,
aspects = aspects,
progress = progress,
dirs = dirs,
select_dirs = select_dirs,
output_dir = output_dir,
selection = Sessions.Selection(
requirements = requirements,
all_sessions = all_sessions,
base_sessions = base_sessions,
exclude_session_groups = exclude_session_groups,
exclude_sessions = exclude_sessions,
session_groups = session_groups,
sessions = sessions))
}
val end_date = Date.now()
val timing = end_date.time - start_date.time
progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
progress.echo(timing.message_hms + " elapsed time")
})
}