# HG changeset patch # User wenzelm # Date 1568290967 -7200 # Node ID 9cde8c4ea5a5aa8d7b79c312cd318838b7698888 # Parent c1597167563ebe70002dff1b2533d5fb0ca97cc0 discontinued obsolete "isabelle imports" and all_known data; diff -r c1597167563e -r 9cde8c4ea5a5 NEWS --- a/NEWS Thu Sep 12 13:39:04 2019 +0200 +++ b/NEWS Thu Sep 12 14:22:47 2019 +0200 @@ -85,6 +85,11 @@ *** System *** +* The command-line tool "isabelle imports" has been discontinued: strict +checking of session directories enforces session-qualified theory names +in applications -- users are responsible to specify session ROOT entries +properly. + * Theory export via Isabelle/Scala has been reworked. The former "fact" name space is now split into individual "thm" items: names are potentially indexed, such as "foo" for singleton facts, or "bar(1)", diff -r c1597167563e -r 9cde8c4ea5a5 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Thu Sep 12 13:39:04 2019 +0200 +++ b/src/Doc/System/Sessions.thy Thu Sep 12 14:22:47 2019 +0200 @@ -484,92 +484,6 @@ \ -section \Maintain theory imports wrt.\ session structure\ - -text \ - The @{tool_def "imports"} tool helps to maintain theory imports wrt.\ - session structure. It supports three main operations via options \<^verbatim>\-I\, - \<^verbatim>\-M\, \<^verbatim>\-U\. Its command-line usage is: @{verbatim [display] -\Usage: isabelle imports [OPTIONS] [SESSIONS ...] - - Options are: - -B NAME include session NAME and all descendants - -D DIR include session directory and select its sessions - -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 - -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 - -i incremental update according to session graph structure - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -v verbose - -x NAME exclude session NAME and all descendants - - Maintain theory imports wrt. session structure. At least one operation - needs to be specified (see options -I -M -U).\} - - \<^medskip> - The selection of sessions and session directories works as for @{tool build} - via options \<^verbatim>\-B\, \<^verbatim>\-D\, \<^verbatim>\-R\, \<^verbatim>\-X\, \<^verbatim>\-a\, \<^verbatim>\-d\, \<^verbatim>\-g\, \<^verbatim>\-x\ (see - \secref{sec:tool-build}). - - \<^medskip> - Option \<^verbatim>\-o\ overrides Isabelle system options as for @{tool build} - (see \secref{sec:tool-build}). - - \<^medskip> - Option \<^verbatim>\-v\ increases the general level of verbosity. - - \<^medskip> - Option \<^verbatim>\-I\ 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>\ROOT\ file entry, a - proper session-qualified theory name can be used (cf.\ option \<^verbatim>\-U\). For - example, adhoc \<^theory_text>\imports\ \<^verbatim>\"~~/src/HOL/Library/Multiset"\ becomes formal - \<^theory_text>\imports\ \<^verbatim>\"HOL-Library.Multiset"\ after adding \isakeyword{sessions} - \<^verbatim>\"HOL-Library"\ to the \<^verbatim>\ROOT\ 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>\-M\ checks imported theories against the Mercurial repositories of - the underlying session directories; non-repository directories are ignored. - This helps to find files that are accidentally ignored, e.g.\ due to - rearrangements of the session structure. - - \<^medskip> - Option \<^verbatim>\-U\ updates theory imports with old-style directory specifications - to canonical session-qualified theory names, according to the theory name - space imported via \isakeyword{sessions} within the \<^verbatim>\ROOT\ specification. - - Option \<^verbatim>\-i\ modifies the meaning of option \<^verbatim>\-U\ to proceed incrementally, - following to the session graph structure in bottom-up order. This may - lead to more accurate results in complex session hierarchies. -\ - -subsubsection \Examples\ - -text \ - Determine potential session imports for some project directory: - @{verbatim [display] \isabelle imports -I -D 'some/where/My_Project'\} - - \<^smallskip> - Mercurial repository check for some project directory: - @{verbatim [display] \isabelle imports -M -D 'some/where/My_Project'\} - - \<^smallskip> - Incremental update of theory imports for some project directory: - @{verbatim [display] \isabelle imports -U -i -D 'some/where/My_Project'\} -\ - - section \Retrieve theory exports \label{sec:tool-export}\ text \ diff -r c1597167563e -r 9cde8c4ea5a5 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Thu Sep 12 13:39:04 2019 +0200 +++ b/src/Pure/System/isabelle_tool.scala Thu Sep 12 14:22:47 2019 +0200 @@ -148,7 +148,6 @@ Doc.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, - Imports.isabelle_tool, ML_Process.isabelle_tool, Mkroot.isabelle_tool, Options.isabelle_tool, diff -r c1597167563e -r 9cde8c4ea5a5 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Sep 12 13:39:04 2019 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Sep 12 14:22:47 2019 +0200 @@ -182,8 +182,7 @@ imports getOrElse Base.bootstrap(session_directories, global_theories) } - sealed case class Deps( - sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known) + sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { override def toString: String = "Sessions.Deps(" + sessions_structure + ")" @@ -429,10 +428,7 @@ } }) - val all_known = - Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_))) - - Deps(sessions_structure, session_bases, all_known) + Deps(sessions_structure, session_bases) } diff -r c1597167563e -r 9cde8c4ea5a5 src/Pure/Tools/imports.scala --- a/src/Pure/Tools/imports.scala Thu Sep 12 13:39:04 2019 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,325 +0,0 @@ -/* Title: Pure/Tools/imports.scala - Author: Makarius - -Maintain theory imports wrt. session structure. -*/ - -package isabelle - - -import java.io.{File => JFile} - - -object Imports -{ - /* repository files */ - - def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true) - : List[JFile] = - Mercurial.find_repository(start) match { - case None => - progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)") - Nil - case Some(hg) => - val start_path = start.canonical_file.toPath - for { - name <- hg.known_files() - file = (hg.root + Path.explode(name)).file - if pred(file) && File.canonical(file).toPath.startsWith(start_path) - } yield file - } - - - /* 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) - { - def edits: List[Text.Edit] = - Text.Edit.replace(range.start, old_text, new_text) - - override def toString: String = - range.toString + ": " + old_text + " -> " + new_text - } - - def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String) - : Option[(JFile, Update)] = - { - val file = - pos match { - case Position.File(file) => Path.explode(file).canonical_file - case _ => error("Missing file in position" + Position.here(pos)) - } - - val text = File.read(file) - - val range = - pos match { - case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range) - case _ => error("Missing range in position" + Position.here(pos)) - } - - Token.read_name(keywords, range.substring(text)) match { - case Some(tok) => - val s1 = tok.source - val s2 = Token.quote_name(keywords, update(tok.content)) - if (s1 == s2) None else Some((file, Update(range, s1, s2))) - case None => error("Name token expected" + Position.here(pos)) - } - } - - - /* collective operations */ - - def imports( - options: Options, - operation_imports: Boolean = false, - operation_repository_files: Boolean = false, - operation_update: Boolean = false, - update_message: String = "", - progress: Progress = No_Progress, - selection: Sessions.Selection = Sessions.Selection.empty, - dirs: List[Path] = Nil, - select_dirs: List[Path] = Nil, - verbose: Boolean = false) = - { - val sessions_structure = - Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs) - - val deps = - sessions_structure.selection_deps(options, selection, progress = progress, verbose = verbose). - check_errors - - val root_keywords = Sessions.root_syntax.keywords - - if (operation_imports) { - val report_imports: List[Report] = - sessions_structure.build_topological_order.map((session_name: String) => - { - val info = sessions_structure(session_name) - val session_base = deps(session_name) - - val declared_imports = - sessions_structure.imports_requirements(List(session_name)).toSet - - val extra_imports = - (for { - 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) - if !declared_imports.contains(qualifier) - } yield qualifier).toSet - - val loaded_imports = - sessions_structure.imports_requirements( - session_base.loaded_theories.keys.map(a => - session_base.theory_qualifier(session_base.known.theories(a).name))) - .toSet - session_name - - val minimal_imports = - loaded_imports.filter(s1 => - !loaded_imports.exists(s2 => sessions_structure.imports_graph.is_edge(s1, s2))) - - def make_result(set: Set[String]): Option[List[String]] = - if (set.isEmpty) None - else Some(sessions_structure.imports_topological_order.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) { - progress.echo("\nMercurial repository check:") - val unused_files = - for { - (_, dir) <- Sessions.directories(dirs, select_dirs) - file <- repository_files(progress, dir, file => file.getName.endsWith(".thy")) - if deps.all_known.get_file(file).isEmpty - } yield file - unused_files.foreach(file => progress.echo("unused file " + quote(file.toString))) - } - - if (operation_update) { - progress.echo("\nUpdate theory imports" + update_message + ":") - val updates = - sessions_structure.build_topological_order.flatMap(session_name => - { - val info = sessions_structure(session_name) - val session_base = deps(session_name) - val session_resources = new Resources(sessions_structure, session_base) - val imports_base = session_base.get_imports - val imports_resources = new Resources(sessions_structure, imports_base) - - def standard_import(qualifier: String, dir: String, s: String): String = - imports_resources.standard_import(session_base, qualifier, dir, s) - - val updates_root = - for { - (_, pos) <- info.theories.flatMap(_._2) - upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _)) - } yield upd - - val updates_theories = - (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_pos - upd <- update_name(session_base.overall_syntax.keywords, pos, - standard_import(session_base.theory_qualifier(name), name.master_dir, _)) - } yield upd).toList - - updates_root ::: updates_theories - }) - - val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) - val conflicts = - file_updates.iterator_list.flatMap({ case (file, upds) => - Library.duplicates(upds.sortBy(_.range.start), - (x: Update, y: Update) => x.range overlaps y.range) match - { - case Nil => None - case bad => Some((file, bad)) - } - }) - if (conflicts.nonEmpty) - error(cat_lines( - conflicts.map({ case (file, bad) => - "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) - - for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) { - progress.echo("file " + quote(file.toString)) - val edits = - upds.sortBy(upd => - upd.range.start).flatMap(upd => - Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) - val new_text = - (File.read(file) /: edits)({ case (text, edit) => - edit.edit(text, 0) match { - case (None, text1) => text1 - case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) - } - }) - File.write_backup2(Path.explode(File.standard_path(file)), new_text) - } - } - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = - Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args => - { - var base_sessions: List[String] = Nil - var select_dirs: List[Path] = Nil - var operation_imports = false - var operation_repository_files = false - var requirements = false - var operation_update = false - var exclude_session_groups: List[String] = Nil - var all_sessions = false - var dirs: List[Path] = Nil - var session_groups: List[String] = Nil - var incremental_update = false - var options = Options.init() - var verbose = false - var exclude_sessions: List[String] = Nil - - val getopts = Getopts(""" -Usage: isabelle imports [OPTIONS] [SESSIONS ...] - - Options are: - -B NAME include session NAME and all descendants - -D DIR include session directory and select its sessions - -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 - -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 - -i incremental update according to session graph structure - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -v verbose - -x NAME exclude session NAME and all descendants - - Maintain theory imports wrt. session structure. At least one operation - needs to be specified (see options -I -M -U). -""", - "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), - "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), - "I" -> (_ => operation_imports = true), - "M" -> (_ => operation_repository_files = true), - "R" -> (_ => requirements = true), - "U" -> (_ => operation_update = true), - "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), - "a" -> (_ => all_sessions = true), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "g:" -> (arg => session_groups = session_groups ::: List(arg)), - "i" -> (_ => incremental_update = true), - "o:" -> (arg => options = options + arg), - "v" -> (_ => verbose = true), - "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) - - val sessions = getopts(args) - if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update)) - getopts.usage() - - val selection = - Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, - exclude_sessions, session_groups, sessions) - - val progress = new Console_Progress(verbose = verbose) - - if (operation_imports || operation_repository_files || - operation_update && !incremental_update) - { - imports(options, operation_imports = operation_imports, - operation_repository_files = operation_repository_files, - operation_update = operation_update, - progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs, - verbose = verbose) - } - else if (operation_update && incremental_update) { - Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs). - selection(selection).imports_topological_order.foreach(name => - { - imports(options, operation_update = operation_update, progress = progress, - update_message = " for session " + quote(name), - selection = Sessions.Selection(sessions = List(name)), - dirs = dirs ::: select_dirs, verbose = verbose) - }) - } - }) -} diff -r c1597167563e -r 9cde8c4ea5a5 src/Pure/build-jars --- a/src/Pure/build-jars Thu Sep 12 13:39:04 2019 +0200 +++ b/src/Pure/build-jars Thu Sep 12 14:22:47 2019 +0200 @@ -151,7 +151,6 @@ Tools/doc.scala Tools/dump.scala Tools/fontforge.scala - Tools/imports.scala Tools/main.scala Tools/mkroot.scala Tools/print_operation.scala