# HG changeset patch # User wenzelm # Date 1527539392 -7200 # Node ID ce59ab0adfddf614b525cf206e1f9b204ff5f005 # Parent ce7855c7f5f46125a056e8e5b8ccfe3c3bded561# Parent 119fc05f6b008c8091465e4d25102214f0a5d585 merged diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/ML/ml_console.scala --- 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 diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/PIDE/command.scala --- 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 { diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/PIDE/document.scala --- 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 } diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/PIDE/resources.scala --- 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(_)) } diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/System/isabelle_tool.scala --- 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, diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/System/progress.scala --- 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 diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/Thy/export.scala --- 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) } diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/Thy/sessions.scala --- 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 diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/Tools/build.scala --- 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 + } + } + } } diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/Tools/dump.scala --- /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) + }) +} diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/Tools/imports.scala --- 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 }) diff -r ce7855c7f5f4 -r ce59ab0adfdd src/Pure/build-jars --- 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