--- a/src/Pure/ML/ml_console.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/ML/ml_console.scala Mon May 28 22:29:52 2018 +0200
@@ -50,19 +50,13 @@
if (!more_args.isEmpty) getopts.usage()
- // build
- if (!no_build && !raw_ml_system &&
- !Build.build(options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
- {
+ // build logic
+ if (!no_build && !raw_ml_system) {
val progress = new Console_Progress()
- progress.echo("Build started for Isabelle/" + logic + " ...")
- progress.interrupt_handler {
- val res =
- Build.build(options, progress = progress, build_heap = true,
- dirs = dirs, system_mode = system_mode, sessions = List(logic))
- if (!res.ok) sys.exit(res.rc)
- }
+ val rc =
+ Build.build_logic(options, logic, build_heap = true, progress = progress,
+ dirs = dirs, system_mode = system_mode)
+ if (rc != 0) sys.exit(rc)
}
// process loop
--- a/src/Pure/PIDE/command.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/PIDE/command.scala Mon May 28 22:29:52 2018 +0200
@@ -511,7 +511,7 @@
val qualifier = resources.session_base.theory_qualifier(node_name)
val dir = node_name.master_dir
for {
- (_, known_name) <- resources.session_base.known.theories.toList
+ known_name <- resources.session_base.known.theory_names
if completed(known_name.theory_base_name)
}
yield {
--- a/src/Pure/PIDE/document.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/PIDE/document.scala Mon May 28 22:29:52 2018 +0200
@@ -137,6 +137,8 @@
sealed case class Entry(name: Node.Name, header: Node.Header)
{
+ def map(f: String => String): Entry = copy(name = name.map(f))
+
override def toString: String = name.toString
}
--- a/src/Pure/PIDE/resources.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/PIDE/resources.scala Mon May 28 22:29:52 2018 +0200
@@ -277,7 +277,7 @@
loaded_theories.all_preds(theories.map(_.theory)).
filter(session_base.loaded_theories.defined(_))
- base_theories.map(theory => session_base.known.theories(theory).path) :::
+ base_theories.map(theory => session_base.known.theories(theory).name.path) :::
base_theories.flatMap(session_base.known.loaded_files(_))
}
--- a/src/Pure/System/isabelle_tool.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/System/isabelle_tool.scala Mon May 28 22:29:52 2018 +0200
@@ -109,6 +109,7 @@
Build_Status.isabelle_tool,
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
+ Dump.isabelle_tool,
Export.isabelle_tool,
Imports.isabelle_tool,
Mkroot.isabelle_tool,
--- a/src/Pure/System/progress.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/System/progress.scala Mon May 28 22:29:52 2018 +0200
@@ -23,6 +23,7 @@
Timing.timeit(message, enabled, echo(_))(e)
def stopped: Boolean = false
+ def interrupt_handler[A](e: => A): A = e
def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
@@ -53,7 +54,8 @@
if (verbose) echo(session + ": theory " + theory)
@volatile private var is_stopped = false
- def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
+ override def interrupt_handler[A](e: => A): A =
+ POSIX_Interrupt.handler { is_stopped = true } { e }
override def stopped: Boolean =
{
if (Thread.interrupted) is_stopped = true
--- a/src/Pure/Thy/export.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/Thy/export.scala Mon May 28 22:29:52 2018 +0200
@@ -281,22 +281,16 @@
case _ => getopts.usage()
}
+ val progress = new Console_Progress()
+
/* build */
- val progress = new Console_Progress()
-
- if (!no_build &&
- !Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode,
- sessions = List(session_name)).ok)
- {
- progress.echo("Build started for Isabelle/" + session_name + " ...")
- progress.interrupt_handler {
- val res =
- Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode,
- sessions = List(session_name))
- if (!res.ok) sys.exit(res.rc)
- }
+ if (!no_build) {
+ val rc =
+ Build.build_logic(options, session_name, progress = progress,
+ dirs = dirs, system_mode = system_mode)
+ if (rc != 0) sys.exit(rc)
}
--- a/src/Pure/Thy/sessions.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Mon May 28 22:29:52 2018 +0200
@@ -41,42 +41,45 @@
def make(local_dir: Path, bases: List[Base],
sessions: List[(String, Position.T)] = Nil,
- theories: List[Document.Node.Name] = Nil,
+ theories: List[Document.Node.Entry] = Nil,
loaded_files: List[(String, List[Path])] = Nil): Known =
{
def bases_iterator(local: Boolean) =
for {
base <- bases.iterator
- (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
- } yield name
+ (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator
+ } yield entry
def local_theories_iterator =
{
val local_path = local_dir.canonical_file.toPath
- theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
+ theories.iterator.filter(entry =>
+ entry.name.path.canonical_file.toPath.startsWith(local_path))
}
val known_sessions =
(sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
val known_theories =
- (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
- case (known, name) =>
- known.get(name.theory) match {
- case Some(name1) if name != name1 =>
- error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
- case _ => known + (name.theory -> name)
+ (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
+ case (known, entry) =>
+ known.get(entry.name.theory) match {
+ case Some(entry1) if entry.name != entry1.name =>
+ error("Duplicate theory " + quote(entry.name.node) + " vs. " +
+ quote(entry1.name.node))
+ case _ => known + (entry.name.theory -> entry)
}
})
val known_theories_local =
- (Map.empty[String, Document.Node.Name] /:
+ (Map.empty[String, Document.Node.Entry] /:
(bases_iterator(true) ++ local_theories_iterator))({
- case (known, name) => known + (name.theory -> name)
+ case (known, entry) => known + (entry.name.theory -> entry)
})
val known_files =
(Map.empty[JFile, List[Document.Node.Name]] /:
(bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
- case (known, name) =>
+ case (known, entry) =>
+ val name = entry.name
val file = name.path.canonical_file
val theories1 = known.getOrElse(file, Nil)
if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
@@ -89,7 +92,8 @@
Known(
known_sessions,
- known_theories, known_theories_local,
+ known_theories,
+ known_theories_local,
known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
known_loaded_files)
}
@@ -97,8 +101,8 @@
sealed case class Known(
sessions: Map[String, Position.T] = Map.empty,
- theories: Map[String, Document.Node.Name] = Map.empty,
- theories_local: Map[String, Document.Node.Name] = Map.empty,
+ theories: Map[String, Document.Node.Entry] = Map.empty,
+ theories_local: Map[String, Document.Node.Entry] = Map.empty,
files: Map[JFile, List[Document.Node.Name]] = Map.empty,
loaded_files: Map[String, List[Path]] = Map.empty)
{
@@ -112,6 +116,16 @@
theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
+ def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
+
+ lazy val theory_graph: Graph[Document.Node.Name, Unit] =
+ {
+ val entries =
+ for ((_, entry) <- theories.toList)
+ yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp._1.theory).name))
+ Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
+ }
+
def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
{
val res = files.getOrElse(File.canonical(file), Nil).headOption
@@ -159,11 +173,11 @@
nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
def known_theory(name: String): Option[Document.Node.Name] =
- known.theories.get(name)
+ known.theories.get(name).map(_.name)
def dest_known_theories: List[(String, String)] =
- for ((theory, node_name) <- known.theories.toList)
- yield (theory, node_name.node)
+ for ((theory, entry) <- known.theories.toList)
+ yield (theory, entry.name.node)
def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
}
@@ -319,7 +333,7 @@
val known =
Known.make(info.dir, List(imports_base),
sessions = List(info.name -> info.pos),
- theories = dependencies.theories,
+ theories = dependencies.entries,
loaded_files = loaded_files)
val sources_errors =
@@ -352,7 +366,10 @@
}
})
- Deps(sessions_structure, session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
+ val all_known =
+ Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_)))
+
+ Deps(sessions_structure, session_bases, all_known)
}
@@ -679,6 +696,15 @@
new Structure(restrict(build_graph), restrict(imports_graph))
}
+ def selection_deps(sel: Selection,
+ progress: Progress = No_Progress,
+ inlined_files: Boolean = false,
+ verbose: Boolean = false): Deps =
+ {
+ Sessions.deps(selection(sel), global_theories,
+ progress = progress, inlined_files = inlined_files, verbose = verbose)
+ }
+
def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
--- a/src/Pure/Tools/build.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/Tools/build.scala Mon May 28 22:29:52 2018 +0200
@@ -822,4 +822,24 @@
sys.exit(results.rc)
})
+
+
+ /* build logic image */
+
+ def build_logic(options: Options, logic: String,
+ progress: Progress = No_Progress,
+ build_heap: Boolean = false,
+ dirs: List[Path] = Nil,
+ system_mode: Boolean = false): Int =
+ {
+ if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
+ system_mode = system_mode, sessions = List(logic)).ok) 0
+ else {
+ progress.echo("Build started for Isabelle/" + logic + " ...")
+ progress.interrupt_handler {
+ Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
+ system_mode = system_mode, sessions = List(logic)).rc
+ }
+ }
+ }
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/dump.scala Mon May 28 22:29:52 2018 +0200
@@ -0,0 +1,125 @@
+/* Title: Pure/Tools/dump.scala
+ Author: Makarius
+
+Dump build database produced by PIDE session.
+*/
+
+package isabelle
+
+
+object Dump
+{
+ def dump(options: Options, logic: String,
+ consume: Thy_Resources.Theories_Result => Unit = _ => (),
+ progress: Progress = No_Progress,
+ log: Logger = No_Logger,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
+ verbose: Boolean = false,
+ system_mode: Boolean = false,
+ selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
+ {
+ if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
+ system_mode = system_mode) != 0) error(logic + " FAILED")
+
+ val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
+
+ val deps =
+ Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
+ selection_deps(selection)
+
+ val session =
+ Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
+ include_sessions = deps.sessions_structure.imports_topological_order,
+ progress = progress, log = log)
+
+ val theories = deps.all_known.theory_graph.topological_order.map(_.theory)
+ val theories_result = session.use_theories(theories, progress = progress)
+
+ try { consume(theories_result) }
+ catch { case exn: Throwable => session.stop (); throw exn }
+
+ session.stop()
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
+ {
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var requirements = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var options = Options.init()
+ var system_mode = false
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
+
+ val getopts = Getopts("""
+Usage: isabelle dump [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -B NAME include session NAME and all descendants
+ -D DIR include session directory and select its sessions
+ -R operate on requirements of selected sessions
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -s system build mode for logic image
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Dump build database (PIDE markup etc.) based on dynamic session.""",
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l:" -> (arg => logic = arg),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "o:" -> (arg => options = options + arg),
+ "s" -> (_ => system_mode = true),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+ val sessions = getopts(args)
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ def consume(theories_result: Thy_Resources.Theories_Result)
+ {
+ // FIXME
+ for ((node, _) <- theories_result.nodes) progress.echo(node.toString)
+ }
+
+ val result =
+ dump(options, logic,
+ consume = consume _,
+ progress = progress,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ verbose = verbose,
+ 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))
+
+ progress.echo(result.timing.message_resources)
+
+ sys.exit(result.rc)
+ })
+}
--- a/src/Pure/Tools/imports.scala Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/Tools/imports.scala Mon May 28 22:29:52 2018 +0200
@@ -99,11 +99,9 @@
select_dirs: List[Path] = Nil,
verbose: Boolean = false) =
{
- val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
-
val deps =
- Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories,
- progress = progress, verbose = verbose).check_errors
+ Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
+ selection_deps(selection, progress = progress, verbose = verbose).check_errors
val root_keywords = Sessions.root_syntax.keywords
@@ -119,7 +117,7 @@
val extra_imports =
(for {
- (_, a) <- session_base.known.theories.iterator
+ a <- session_base.known.theory_names
if session_base.theory_qualifier(a) == info.name
b <- deps.all_known.get_file(a.path.file)
qualifier = session_base.theory_qualifier(b)
@@ -129,7 +127,7 @@
val loaded_imports =
deps.sessions_structure.imports_requirements(
session_base.loaded_theories.keys.map(a =>
- session_base.theory_qualifier(session_base.known.theories(a))))
+ session_base.theory_qualifier(session_base.known.theories(a).name)))
.toSet - session_name
val minimal_imports =
@@ -190,13 +188,13 @@
} yield upd
val updates_theories =
- for {
- (_, name) <- session_base.known.theories_local.toList
+ (for {
+ name <- session_base.known.theories_local.iterator.map(p => p._2.name)
if session_base.theory_qualifier(name) == info.name
(_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
upd <- update_name(session_base.overall_syntax.keywords, pos,
standard_import(session_base.theory_qualifier(name), name.master_dir, _))
- } yield upd
+ } yield upd).toList
updates_root ::: updates_theories
})
--- a/src/Pure/build-jars Sun May 27 22:57:06 2018 +0100
+++ b/src/Pure/build-jars Mon May 28 22:29:52 2018 +0200
@@ -137,6 +137,7 @@
Thy/thy_header.scala
Thy/thy_resources.scala
Thy/thy_syntax.scala
+ Tools/dump.scala
Tools/build.scala
Tools/build_docker.scala
Tools/check_keywords.scala