--- 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"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
+
* More predefined symbols: \<Parallel> \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX
package "pifont").
-* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
-"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
-
* 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>\<open>'a = A in
lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
+* 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>\<open>c\<close>
@@ -431,60 +488,6 @@
\<^if_windows>\<open>...\<close>
\<^if_unix>\<open>...\<close>
-* 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)