--- a/ANNOUNCE Fri Sep 09 21:28:35 2022 +0200
+++ b/ANNOUNCE Sat Sep 10 16:57:18 2022 +0200
@@ -1,49 +1,35 @@
-Subject: Announcing Isabelle2021-1
+Subject: Announcing Isabelle2022
To: isabelle-users@cl.cam.ac.uk
-Isabelle2021-1 is now available.
+Isabelle2022 is now available.
-This version introduces many changes over Isabelle2020-1: see the NEWS
-file for further details. Here are various details:
-
-* HTML presentation now includes links to formal entities.
-
-* Isar: local theory support for 'syntax' and 'no_syntax' commands.
+This version introduces notable changes over Isabelle2021-1: see the
+NEWS file for further details. Here are various details:
-* Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala
-modules and plugins.
+* HTML presentation is more robust and covers more files and links.
-* HOL: new order prover.
+* Display of instantiation for schematic goals.
-* HOL: many changes and improvements on bit operations and word types.
+* PIDE: improved Isabelle/VSCode based on bundled VSCodium engine.
-* HOL: various library improvements (HOL-Library, HOL-Combinatorics,
-HOL-Analysis, HOL-Statespace)
+* HOL: various improvements of theory libraries.
-* Sledgehammer: update of ATPs and SMTs: E prover, veriT, Zipperposition,
-Vampire (now with Open-Source license).
-
-* Nitpick: external MiniSat solver for all supported Isabelle platforms.
+* HOL: updates and improvements of Sledgehammer.
-* ML: uniform treatment of external processes via Isabelle/Scala.
+* HOL: improved simproc support for record types.
-* ML: advanced antiquotations for Type/Const constructors, and for inline
-instantiation of types, terms, facts.
+* ML: scalable type Bytes.T with support for XZ compression.
-* Haskell: substantially improved Isabelle/Haskell library.
+* System: bundled Node.js/Chromium/Electron platform (part VSCodium).
-* System: more predefined Isabelle symbols (blackboard-bold, Z notation).
-
-* System: support for Isabelle/Scala modules defined in user-space.
+* System: Isabelle/Scala is based on Scala 3 (dotty compiler).
-* System: improved document preparation using Isabelle/Scala.
+* System: tools to sync hg repositories, notably Isabelle + AFP.
-* System: update to current Java 17 LTS.
-
-* System: update to Poly/ML 5.9 with improved support for ARM64 on Linux.
+* System: improved "isabelle log" tool with regex filtering.
-You may get Isabelle2021-1 from the following mirror sites:
+You may get Isabelle2022 from the following mirror sites:
Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle
Munich (Germany) https://isabelle.in.tum.de
--- a/src/Doc/System/Sessions.thy Fri Sep 09 21:28:35 2022 +0200
+++ b/src/Doc/System/Sessions.thy Sat Sep 10 16:57:18 2022 +0200
@@ -865,6 +865,7 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
+ -b follow session build dependencies (default: source imports)
-d DIR include session directory
-g NAME select session group NAME
-x NAME exclude session NAME and all descendants
@@ -884,7 +885,15 @@
@{verbatim [display] \<open> isabelle sessions -a\<close>}
\<^medskip>
- Sessions that are based on \<^verbatim>\<open>ZF\<close> (and required by it):
+ Sessions that are imported by \<^verbatim>\<open>ZF\<close>:
+ @{verbatim [display] \<open> isabelle sessions ZF\<close>}
+
+ \<^medskip>
+ Sessions that are required to build \<^verbatim>\<open>ZF\<close>:
+ @{verbatim [display] \<open> isabelle sessions -b ZF\<close>}
+
+ \<^medskip>
+ Sessions that are based on \<^verbatim>\<open>ZF\<close> (and imported by it):
@{verbatim [display] \<open> isabelle sessions -B ZF\<close>}
\<^medskip>
--- a/src/Pure/Thy/sessions.scala Fri Sep 09 21:28:35 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Sep 10 16:57:18 2022 +0200
@@ -1167,6 +1167,7 @@
var requirements = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
+ var build_graph = false
var dirs: List[Path] = Nil
var session_groups: List[String] = Nil
var exclude_sessions: List[String] = Nil
@@ -1180,6 +1181,7 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
+ -b follow session build dependencies (default: source imports)
-d DIR include session directory
-g NAME select session group NAME
-x NAME exclude session NAME and all descendants
@@ -1192,6 +1194,7 @@
"R" -> (_ => requirements = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
+ "b" -> (_ => build_graph = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
@@ -1207,9 +1210,10 @@
val sessions_structure =
load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
- for (name <- sessions_structure.imports_topological_order) {
- Output.writeln(name, stdout = true)
- }
+ val order =
+ if (build_graph) sessions_structure.build_topological_order
+ else sessions_structure.imports_topological_order
+ for (name <- order) Output.writeln(name, stdout = true)
})