more informative Imports.Report with actual session imports (minimized);
authorwenzelm
Thu Oct 12 15:58:18 2017 +0200 (20 months ago)
changeset 66851c75769065548
parent 66850 a91b6d80c911
child 66852 d20a668b394e
more informative Imports.Report with actual session imports (minimized);
NEWS
src/Doc/System/Sessions.thy
src/Pure/Tools/imports.scala
     1.1 --- a/NEWS	Thu Oct 12 11:39:54 2017 +0200
     1.2 +++ b/NEWS	Thu Oct 12 15:58:18 2017 +0200
     1.3 @@ -78,6 +78,9 @@
     1.4  corresponding environment values into account, when determining the
     1.5  up-to-date status of a session.
     1.6  
     1.7 +* Command-line tool "isabelle imports -I" also reports actual session
     1.8 +imports. This helps to minimize the session dependency graph.
     1.9 +
    1.10  
    1.11  New in Isabelle2017 (October 2017)
    1.12  ----------------------------------
     2.1 --- a/src/Doc/System/Sessions.thy	Thu Oct 12 11:39:54 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Thu Oct 12 15:58:18 2017 +0200
     2.3 @@ -466,7 +466,7 @@
     2.4    Options are:
     2.5      -B NAME      include session NAME and all descendants
     2.6      -D DIR       include session directory and select its sessions
     2.7 -    -I           operation: report potential session imports
     2.8 +    -I           operation: report session imports
     2.9      -M           operation: Mercurial repository check for theory files
    2.10      -R           operate on requirements of selected sessions
    2.11      -U           operation: update theory imports to use session qualifiers
    2.12 @@ -495,12 +495,19 @@
    2.13    Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
    2.14  
    2.15    \<^medskip>
    2.16 -  Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
    2.17 -  \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
    2.18 -  theory imports from other sessions may use session-qualified names. For
    2.19 -  example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
    2.20 -  \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
    2.21 -  \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
    2.22 +  Option \<^verbatim>\<open>-I\<close> determines reports session imports:
    2.23 +
    2.24 +    \<^descr>[Potential session imports] are derived from old-style use of theory
    2.25 +    files from other sessions via the directory structure. After declaring
    2.26 +    those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
    2.27 +    proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
    2.28 +    example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
    2.29 +    \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
    2.30 +    \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
    2.31 +
    2.32 +    \<^descr>[Actual session imports] are derived from the session qualifiers of all
    2.33 +    currently imported theories. This helps to minimize dependencies in the
    2.34 +    session import structure to what is actually required.
    2.35  
    2.36    \<^medskip>
    2.37    Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
     3.1 --- a/src/Pure/Tools/imports.scala	Thu Oct 12 11:39:54 2017 +0200
     3.2 +++ b/src/Pure/Tools/imports.scala	Thu Oct 12 15:58:18 2017 +0200
     3.3 @@ -30,6 +30,23 @@
     3.4      }
     3.5  
     3.6  
     3.7 +  /* report imports */
     3.8 +
     3.9 +  sealed case class Report(
    3.10 +    info: Sessions.Info,
    3.11 +    declared_imports: Set[String],
    3.12 +    potential_imports: Option[List[String]],
    3.13 +    actual_imports: Option[List[String]])
    3.14 +  {
    3.15 +    def print(keywords: Keyword.Keywords, result: List[String]): String =
    3.16 +    {
    3.17 +      def print_name(name: String): String = Token.quote_name(keywords, name)
    3.18 +
    3.19 +      "  session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ")
    3.20 +    }
    3.21 +  }
    3.22 +
    3.23 +
    3.24    /* update imports */
    3.25  
    3.26    sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    3.27 @@ -91,15 +108,16 @@
    3.28  
    3.29      val root_keywords = Sessions.root_syntax.keywords
    3.30  
    3.31 -
    3.32      if (operation_imports) {
    3.33 -      progress.echo("\nPotential session imports:")
    3.34 -      selected.flatMap(session_name =>
    3.35 +      val report_imports: List[Report] = selected.map((session_name: String) =>
    3.36        {
    3.37 -        val info = full_sessions(session_name)
    3.38 -        val session_resources = new Resources(deps(session_name))
    3.39 +        val info = selected_sessions(session_name)
    3.40 +        val session_base = deps(session_name)
    3.41 +        val session_resources = new Resources(session_base)
    3.42  
    3.43 -        val declared_imports = full_sessions.imports_requirements(List(session_name)).toSet
    3.44 +        val declared_imports =
    3.45 +          selected_sessions.imports_requirements(List(session_name)).toSet
    3.46 +
    3.47          val extra_imports =
    3.48            (for {
    3.49              (_, a) <- session_resources.session_base.known.theories.iterator
    3.50 @@ -109,12 +127,36 @@
    3.51              if !declared_imports.contains(qualifier)
    3.52            } yield qualifier).toSet
    3.53  
    3.54 -        if (extra_imports.isEmpty) None
    3.55 -        else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
    3.56 -      }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
    3.57 -        progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    3.58 -          extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
    3.59 +        val loaded_imports =
    3.60 +          selected_sessions.imports_requirements(
    3.61 +            session_base.loaded_theories.keys.map(a =>
    3.62 +              session_resources.theory_qualifier(session_base.known.theories(a))))
    3.63 +          .toSet - session_name
    3.64 +
    3.65 +        val minimal_imports =
    3.66 +          loaded_imports.filter(s1 =>
    3.67 +            !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    3.68 +
    3.69 +        def make_result(set: Set[String]): Option[List[String]] =
    3.70 +          if (set.isEmpty) None
    3.71 +          else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
    3.72 +
    3.73 +        Report(info, declared_imports, make_result(extra_imports),
    3.74 +          if (loaded_imports == declared_imports - session_name) None
    3.75 +          else make_result(minimal_imports))
    3.76        })
    3.77 +
    3.78 +      progress.echo("\nPotential session imports:")
    3.79 +      for {
    3.80 +        report <- report_imports.sortBy(_.declared_imports.size)
    3.81 +        potential_imports <- report.potential_imports
    3.82 +      } progress.echo(report.print(root_keywords, potential_imports))
    3.83 +
    3.84 +      progress.echo("\nActual session imports:")
    3.85 +      for {
    3.86 +        report <- report_imports
    3.87 +        actual_imports <- report.actual_imports
    3.88 +      } progress.echo(report.print(root_keywords, actual_imports))
    3.89      }
    3.90  
    3.91      if (operation_repository_files) {
    3.92 @@ -133,7 +175,7 @@
    3.93        val updates =
    3.94          selected.flatMap(session_name =>
    3.95          {
    3.96 -          val info = full_sessions(session_name)
    3.97 +          val info = selected_sessions(session_name)
    3.98            val session_base = deps(session_name)
    3.99            val session_resources = new Resources(session_base)
   3.100            val imports_base = session_base.get_imports
   3.101 @@ -219,7 +261,7 @@
   3.102    Options are:
   3.103      -B NAME      include session NAME and all descendants
   3.104      -D DIR       include session directory and select its sessions
   3.105 -    -I           operation: report potential session imports
   3.106 +    -I           operation: report session imports
   3.107      -M           operation: Mercurial repository check for theory files
   3.108      -R           operate on requirements of selected sessions
   3.109      -U           operation: update theory imports to use session qualifiers