# HG changeset patch # User wenzelm # Date 1662821838 -7200 # Node ID e9f9e8de1ab91a2ea5d7575e4a514c3227741544 # Parent bdab17df07a9fe1a05c318e112bd3b120772bdd8# Parent 98cab94326d4e0e1429681afc8a50ef1fb55d95d merged; diff -r 98cab94326d4 -r e9f9e8de1ab9 ANNOUNCE --- 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 diff -r 98cab94326d4 -r e9f9e8de1ab9 src/Doc/System/Sessions.thy --- 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] \ isabelle sessions -a\} \<^medskip> - Sessions that are based on \<^verbatim>\ZF\ (and required by it): + Sessions that are imported by \<^verbatim>\ZF\: + @{verbatim [display] \ isabelle sessions ZF\} + + \<^medskip> + Sessions that are required to build \<^verbatim>\ZF\: + @{verbatim [display] \ isabelle sessions -b ZF\} + + \<^medskip> + Sessions that are based on \<^verbatim>\ZF\ (and imported by it): @{verbatim [display] \ isabelle sessions -B ZF\} \<^medskip> diff -r 98cab94326d4 -r e9f9e8de1ab9 src/Pure/Thy/sessions.scala --- 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) })