--- a/NEWS Thu Oct 12 11:39:54 2017 +0200
+++ b/NEWS Thu Oct 12 15:58:18 2017 +0200
@@ -78,6 +78,9 @@
corresponding environment values into account, when determining the
up-to-date status of a session.
+* Command-line tool "isabelle imports -I" also reports actual session
+imports. This helps to minimize the session dependency graph.
+
New in Isabelle2017 (October 2017)
----------------------------------
--- a/src/Doc/System/Sessions.thy Thu Oct 12 11:39:54 2017 +0200
+++ b/src/Doc/System/Sessions.thy Thu Oct 12 15:58:18 2017 +0200
@@ -466,7 +466,7 @@
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
- -I operation: report potential session imports
+ -I operation: report session imports
-M operation: Mercurial repository check for theory files
-R operate on requirements of selected sessions
-U operation: update theory imports to use session qualifiers
@@ -495,12 +495,19 @@
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
\<^medskip>
- Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
- \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
- theory imports from other sessions may use session-qualified names. For
- example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
- \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
- \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
+ Option \<^verbatim>\<open>-I\<close> determines reports session imports:
+
+ \<^descr>[Potential session imports] are derived from old-style use of theory
+ files from other sessions via the directory structure. After declaring
+ those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
+ proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
+ example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
+ \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
+ \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
+
+ \<^descr>[Actual session imports] are derived from the session qualifiers of all
+ currently imported theories. This helps to minimize dependencies in the
+ session import structure to what is actually required.
\<^medskip>
Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
--- a/src/Pure/Tools/imports.scala Thu Oct 12 11:39:54 2017 +0200
+++ b/src/Pure/Tools/imports.scala Thu Oct 12 15:58:18 2017 +0200
@@ -30,6 +30,23 @@
}
+ /* report imports */
+
+ sealed case class Report(
+ info: Sessions.Info,
+ declared_imports: Set[String],
+ potential_imports: Option[List[String]],
+ actual_imports: Option[List[String]])
+ {
+ def print(keywords: Keyword.Keywords, result: List[String]): String =
+ {
+ def print_name(name: String): String = Token.quote_name(keywords, name)
+
+ " session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ")
+ }
+ }
+
+
/* update imports */
sealed case class Update(range: Text.Range, old_text: String, new_text: String)
@@ -91,15 +108,16 @@
val root_keywords = Sessions.root_syntax.keywords
-
if (operation_imports) {
- progress.echo("\nPotential session imports:")
- selected.flatMap(session_name =>
+ val report_imports: List[Report] = selected.map((session_name: String) =>
{
- val info = full_sessions(session_name)
- val session_resources = new Resources(deps(session_name))
+ val info = selected_sessions(session_name)
+ val session_base = deps(session_name)
+ val session_resources = new Resources(session_base)
- val declared_imports = full_sessions.imports_requirements(List(session_name)).toSet
+ val declared_imports =
+ selected_sessions.imports_requirements(List(session_name)).toSet
+
val extra_imports =
(for {
(_, a) <- session_resources.session_base.known.theories.iterator
@@ -109,12 +127,36 @@
if !declared_imports.contains(qualifier)
} yield qualifier).toSet
- if (extra_imports.isEmpty) None
- else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
- }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
- progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
- extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
+ val loaded_imports =
+ selected_sessions.imports_requirements(
+ session_base.loaded_theories.keys.map(a =>
+ session_resources.theory_qualifier(session_base.known.theories(a))))
+ .toSet - session_name
+
+ val minimal_imports =
+ loaded_imports.filter(s1 =>
+ !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
+
+ def make_result(set: Set[String]): Option[List[String]] =
+ if (set.isEmpty) None
+ else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
+
+ Report(info, declared_imports, make_result(extra_imports),
+ if (loaded_imports == declared_imports - session_name) None
+ else make_result(minimal_imports))
})
+
+ progress.echo("\nPotential session imports:")
+ for {
+ report <- report_imports.sortBy(_.declared_imports.size)
+ potential_imports <- report.potential_imports
+ } progress.echo(report.print(root_keywords, potential_imports))
+
+ progress.echo("\nActual session imports:")
+ for {
+ report <- report_imports
+ actual_imports <- report.actual_imports
+ } progress.echo(report.print(root_keywords, actual_imports))
}
if (operation_repository_files) {
@@ -133,7 +175,7 @@
val updates =
selected.flatMap(session_name =>
{
- val info = full_sessions(session_name)
+ val info = selected_sessions(session_name)
val session_base = deps(session_name)
val session_resources = new Resources(session_base)
val imports_base = session_base.get_imports
@@ -219,7 +261,7 @@
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
- -I operation: report potential session imports
+ -I operation: report session imports
-M operation: Mercurial repository check for theory files
-R operate on requirements of selected sessions
-U operation: update theory imports to use session qualifiers