# HG changeset patch # User wenzelm # Date 1635776693 -3600 # Node ID e911be10306612ea8b31e71ffb6fa25f4a6cca2b # Parent b04a820c345ec1a5ebfaab0a94b07cf0902fc989 some reordering for release; diff -r b04a820c345e -r e911be103066 NEWS --- a/NEWS Mon Nov 01 14:58:04 2021 +0100 +++ b/NEWS Mon Nov 01 15:24:53 2021 +0100 @@ -9,11 +9,12 @@ *** General *** -* Commands 'syntax' and 'no_syntax' now work in a local theory context, -but in contrast to 'notation' and 'no_notation' there is no proper way -to refer to local entities. Note that local syntax works well with -'bundle', e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory -Main of Isabelle/HOL. +* The Isabelle/Haskell library ($ISABELLE_HOME/src/Tools/Haskell) has +been significantly improved. In particular, module Isabelle.Bytes +provides type Bytes for light-weight byte strings (with optional UTF8 +interpretation), similar to type string in Isabelle/ML. Isabelle symbols +now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs. +Isabelle/Scala/PIDE. * Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled @@ -26,39 +27,42 @@ theorem test by (simp add: test_def) end +* Theory_Data / Generic_Data: "val extend = I" has been removed; +obsolete since Isabelle2021. + * More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit. -* The Isabelle/Haskell library ($ISABELLE_HOME/src/Tools/Haskell) has -been significantly improved. In particular, module Isabelle.Bytes -provides type Bytes for light-weight byte strings (with optional UTF8 -interpretation), similar to type string in Isabelle/ML. Isabelle symbols -now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs. -Isabelle/Scala/PIDE. - -* Theory_Data / Generic_Data: "val extend = I" has been removed; -obsolete since Isabelle2021. - *** Isar *** +* Commands 'syntax' and 'no_syntax' now work in a local theory context, +but in contrast to 'notation' and 'no_notation' there is no proper way +to refer to local entities. Note that local syntax works well with +'bundle', e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory +Main of Isabelle/HOL. + * The improper proof command 'guess' is no longer part of by Pure, but provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY, existing applications need to import session "Pure-ex" and theory "Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess' command, using explicit 'obtain' instead. +* More robust 'proof' outline for method "induct": support nested cases. + *** Isabelle/jEdit Prover IDE *** -* More robust 'proof' outline for method "induct": support nested cases. - -* Support for built-in font substitution of jEdit text area. - * The main plugin for Isabelle/jEdit can be deactivated and reactivated as documented --- was broken at least since Isabelle2018. +* Isabelle/jEdit is now composed more conventionally from the original +jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle +plugins that are produced in $JEDIT_SETTINGS/jars on demand. The main +isabelle.jedit module is now part of Isabelle/Scala (as one big +$ISABELLE_SCALA_JAR). + * Add-on components may provide their own jEdit plugins, via the new Scala/Java module concept: instances of class isabelle.Scala_Project.Plugin that are declared as "services" within @@ -66,15 +70,17 @@ existing isabelle.jedit.JEdit_Plugin0 (for isabelle_jedit_base.jar) and isabelle.jedit.JEdit_Plugin1 (for isabelle_jedit_main.jar). +* Support for built-in font substitution of jEdit text area. + *** Document preparation *** +* High-quality blackboard-bold symbols from font "txmia" (LaTeX package +"pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\. + * More predefined symbols: \ \ \ (package "stmaryrd"), \ \ (LaTeX package "pifont"). -* High-quality blackboard-bold symbols from font "txmia" (LaTeX package -"pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\. - * Document antiquotations for ML text have been refined: "def" and "ref" variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def} (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit @@ -147,15 +153,6 @@ *** HOL *** -* Theory "HOL-Analysis.Infinite_Sum": new theory for infinite sums with -a more general definition than the existing theory Infinite_Set_Sum. -(Infinite_Set_Sum contains theorems relating the two definitions.) - -* Theory "HOL-Analysis.Product_Vector": Instantiation of the product of -uniform spaces as a uniform space. Minor INCOMPATIBILITY: the old -definition "uniformity_prod_def" is available as a derived fact -"uniformity_dist". - * Theorems "antisym" and "eq_iff" in class "order" have been renamed to "order.antisym" and "order.eq_iff", to coexist locally with "antisym" and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant @@ -182,8 +179,7 @@ operations. INCOMPATIBILITY. * Simplified class hierarchy for bit operations: bit operations reside -in classes (semi)ring_bit_operations, class semiring_bit_shifts is -gone. +in classes (semi)ring_bit_operations, class semiring_bit_shifts is gone. * Consecutive conversions to and from words are not collapsed in any case: rules unsigned_of_nat, unsigned_of_int, signed_of_int, @@ -195,8 +191,7 @@ "setBit", "clearBit". See there further the changelog in theory Guide. INCOMPATIBILITY. -* Reorganized classes and locales for boolean algebras. -INCOMPATIBILITY. +* Reorganized classes and locales for boolean algebras. INCOMPATIBILITY. * New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3, min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor @@ -219,17 +214,16 @@ rewritten using combinators, but the combinators are kept opaque, i.e. without definitions. -* Nitpick: - - External solver "MiniSat" is available for all supported Isabelle - platforms (including Windows and ARM); while "MiniSat_JNI" only - works for Intel Linux and macOS. - * Metis: - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. - Updated the Metis prover underlying the "metis" proof method to version 2.4 (release 20200713). The new version fixes one implementation defect. Very slight INCOMPATIBILITY. +* Nitpick: External solver "MiniSat" is available for all supported +Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only +works for Intel Linux and macOS. + * Theory HOL-Library.Lattice_Syntax has been superseded by bundle "lattice_syntax": it can be used in a local context via 'include' or in a global theory via 'unbundle'. The opposite declarations are bundled as @@ -264,16 +258,6 @@ this code setup should import "HOL-Library.Code_Cardinality". Minor INCOMPATIBILITY. -* Session "HOL-Analysis" and "HOL-Probability": indexed products of -discrete distributions, negative binomial distribution, Hoeffding's -inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, -and some more small lemmas. Some theorems that were stated awkwardly -before were corrected. Minor INCOMPATIBILITY. - -* Session "HOL-Analysis": the complex Arg function has been identified -with the function "arg" of Complex_Main, renaming arg ~> Arg also in the -names of arg_bounded. Minor INCOMPATIBILITY. - * Theory "HOL-Library.Permutation" has been renamed to the more specific "HOL-Library.List_Permutation". Note that most notions from that theory are already present in theory "HOL-Combinatorics.Permutations". @@ -287,15 +271,83 @@ * Theory "HOL-Combinatorics.Transposition" provides elementary swap operation "transpose". +* Theory "HOL-Analysis.Infinite_Sum": new theory for infinite sums with +a more general definition than the existing theory Infinite_Set_Sum. +(Infinite_Set_Sum contains theorems relating the two definitions.) + +* Theory "HOL-Analysis.Product_Vector": Instantiation of the product of +uniform spaces as a uniform space. Minor INCOMPATIBILITY: the old +definition "uniformity_prod_def" is available as a derived fact +"uniformity_dist". + +* Session "HOL-Analysis" and "HOL-Probability": indexed products of +discrete distributions, negative binomial distribution, Hoeffding's +inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, +and some more small lemmas. Some theorems that were stated awkwardly +before were corrected. Minor INCOMPATIBILITY. + +* Session "HOL-Analysis": the complex Arg function has been identified +with the function "arg" of Complex_Main, renaming arg ~> Arg also in the +names of arg_bounded. Minor INCOMPATIBILITY. + * Session "HOL-Statespace": various improvements and cleanup. *** ML *** -* Antiquotation for embedded lemma supports local fixes, as usual in -many other Isar language elements. For example: - - @{lemma "x = x" for x :: nat by (rule refl)} +* External bash processes are always managed by Isabelle/Scala, in +contrast to Isabelle2021 where this was only done for macOS on Apple +Silicon. + +The main Isabelle/ML interface is Isabelle_System.bash_process with +result type Process_Result.T (resembling class Process_Result in Scala); +derived operations Isabelle_System.bash and Isabelle_System.bash_output +provide similar functionality as before. The underlying TCP/IP server +within Isabelle/Scala is available to other programming languages as +well, notably Isabelle/Haskell. + +Rare INCOMPATIBILITY due to subtle semantic differences: + + - Processes invoked from Isabelle/ML actually run in the context of + the Java VM of Isabelle/Scala. The settings environment and current + working directory are usually the same on both sides, but there can be + subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML). + + - Output via stdout and stderr is line-oriented: Unix vs. Windows + line-endings are normalized towards Unix; presence or absence of a + final newline is irrelevant. The original lines are available as + Process_Result.out_lines/err_lines; the concatenated versions + Process_Result.out/err *omit* a trailing newline (using + Library.trim_line, which was occasional seen in applications before, + but is no longer necessary). + + - Output needs to be plain text encoded in UTF-8: Isabelle/Scala + recodes it temporarily as UTF-16. This works for well-formed Unicode + text, but not for arbitrary byte strings. In such cases, the bash + script should write tempory files, managed by Isabelle/ML operations + like Isabelle_System.with_tmp_file to create a file name and + File.read to retrieve its content. + + - The Isabelle/Scala "bash_process" server requires a PIDE session + context. This could be a regular batch session (e.g. "isabelle + build"), a PIDE editor session (e.g. "isabelle jedit"), or headless + PIDE (e.g. "isabelle dump" or "isabelle server"). Note that old + "isabelle console" or raw "isabelle process" don't have that. + +New Process_Result.timing works as in Isabelle/Scala, based on direct +measurements of the bash_process wrapper in C: elapsed time is always +available, CPU time is only available on Linux and macOS, GC time is +unavailable. + +* The following Isabelle/ML system operations are run in the context of +Isabelle/Scala, within a PIDE session context: + + - Isabelle_System.make_directory + - Isabelle_System.copy_dir + - Isabelle_System.copy_file + - Isabelle_System.copy_base_file + - Isabelle_System.rm_tree + - Isabelle_System.download * Term operations under abstractions are now more robust (and more strict) by using the formal proof context in subsequent operations: @@ -374,6 +426,11 @@ \<^instantiate>\'a = A in lemma (schematic) \x = y \ y = x\ for x y :: 'a by simp\ +* ML antiquotation for embedded lemma supports local fixes, as usual in +many other Isar language elements. For example: + + @{lemma "x = x" for x :: nat by (rule refl)} + * ML antiquotations for type constructors and term constants: \<^Type>\c\ @@ -431,60 +488,6 @@ \<^if_windows>\...\ \<^if_unix>\...\ -* External bash processes are always managed by Isabelle/Scala, in -contrast to Isabelle2021 where this was only done for macOS on Apple -Silicon. - -The main Isabelle/ML interface is Isabelle_System.bash_process with -result type Process_Result.T (resembling class Process_Result in Scala); -derived operations Isabelle_System.bash and Isabelle_System.bash_output -provide similar functionality as before. The underlying TCP/IP server -within Isabelle/Scala is available to other programming languages as -well, notably Isabelle/Haskell. - -Rare INCOMPATIBILITY due to subtle semantic differences: - - - Processes invoked from Isabelle/ML actually run in the context of - the Java VM of Isabelle/Scala. The settings environment and current - working directory are usually the same on both sides, but there can be - subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML). - - - Output via stdout and stderr is line-oriented: Unix vs. Windows - line-endings are normalized towards Unix; presence or absence of a - final newline is irrelevant. The original lines are available as - Process_Result.out_lines/err_lines; the concatenated versions - Process_Result.out/err *omit* a trailing newline (using - Library.trim_line, which was occasional seen in applications before, - but is no longer necessary). - - - Output needs to be plain text encoded in UTF-8: Isabelle/Scala - recodes it temporarily as UTF-16. This works for well-formed Unicode - text, but not for arbitrary byte strings. In such cases, the bash - script should write tempory files, managed by Isabelle/ML operations - like Isabelle_System.with_tmp_file to create a file name and - File.read to retrieve its content. - - - The Isabelle/Scala "bash_process" server requires a PIDE session - context. This could be a regular batch session (e.g. "isabelle - build"), a PIDE editor session (e.g. "isabelle jedit"), or headless - PIDE (e.g. "isabelle dump" or "isabelle server"). Note that old - "isabelle console" or raw "isabelle process" don't have that. - -New Process_Result.timing works as in Isabelle/Scala, based on direct -measurements of the bash_process wrapper in C: elapsed time is always -available, CPU time is only available on Linux and macOS, GC time is -unavailable. - -* The following Isabelle/ML system operations are run in the context of -Isabelle/Scala, within a PIDE session context: - - - Isabelle_System.make_directory - - Isabelle_System.copy_dir - - Isabelle_System.copy_file - - Isabelle_System.copy_base_file - - Isabelle_System.rm_tree - - Isabelle_System.download - * ML profiling has been updated and reactivated, after some degration in Isabelle2021: @@ -499,13 +502,13 @@ *** System *** +* Update to OpenJDK 17: the current long-term support version of Java. + * Update to Poly/ML 5.9 with improved support for ARM on Linux. On macOS, the Intel version works more smoothly with Rosetta 2, as already used in Isabelle2021. Further changes to Poly/ML are documented here: http://lists.inf.ed.ac.uk/pipermail/polyml/2021-May/002451.html -* Update to OpenJDK 17: the current long-term support version of Java. - * Perl is no longer required by Isabelle proper, and longer provided by specific Isabelle execution environments (Docker, Cygwin on Windows). Minor INCOMPATIBILITY, add-on applications involving perl need to @@ -529,19 +532,6 @@ - more sources may be given on the command-line, - options -f and -D make the tool more convenient. -* Isabelle/jEdit is now composed more conventionally from the original -jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle -plugins that are produced in $JEDIT_SETTINGS/jars on demand. The main -isabelle.jedit module is now part of Isabelle/Scala (as one big -$ISABELLE_SCALA_JAR). - -* Timeouts for Isabelle/ML tools are subject to system option -"timeout_scale" --- this already used for the overall session build -process before, and allows to adapt to slow machines. The underlying -Timeout.apply in Isabelle/ML treats an original timeout specification 0 -as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY -in boundary cases. - * Remote provers from SystemOnTPTP (notably for Sledgehammer) are now managed via Isabelle/Scala instead of perl; the dependency on libwww-perl has been eliminated (notably on Linux). Rare @@ -568,6 +558,13 @@ ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64 (native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon). +* Timeouts for Isabelle/ML tools are subject to system option +"timeout_scale" --- this already used for the overall session build +process before, and allows to adapt to slow machines. The underlying +Timeout.apply in Isabelle/ML treats an original timeout specification 0 +as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY +in boundary cases. + New in Isabelle2021 (February 2021)