# HG changeset patch # User wenzelm # Date 1712135398 -7200 # Node ID 1231a7fb251017c2acec4bda2bb036d4f052542c # Parent ee07b7738a24b27bd1eebe888a540147150008eb misc tuning for release; diff -r ee07b7738a24 -r 1231a7fb2510 NEWS --- a/NEWS Wed Apr 03 11:02:09 2024 +0200 +++ b/NEWS Wed Apr 03 11:09:58 2024 +0200 @@ -24,6 +24,11 @@ - MLton - Nunchaku + smbc (experimental) +* The configuration option "unify_trace" (default: false) guards tracing +of higher-order unification, which is ubiquitous in assumption steps and +rule applications via resolution. This is disabled by default to avoid +breakdown due to massive amounts of spurious messages. + *** Document preparation *** @@ -31,14 +36,6 @@ (02-Nov-2023). See also src/Doc/Demo_LLNCS/. -*** Pure *** - -* Added configuration option "unify_trace" (default: false) to guard -tracing of higher-order unification, which is ubiquitous in assumption -steps and rule applications via resolution. This is disabled by default -to avoid breakdown due to massive amounts of spurious messages. - - *** HOL *** * Commands 'inductive_cases', 'inductive_simps', 'case_of_simps', @@ -61,9 +58,6 @@ "preplay_timeout". INCOMPATIBILITY. - Added the action "order" testing the proof method of the same name. -* HOL-ex.Sketch_and_Explore: improvements to generate more natural and -readable proof sketches from proof states. - * Explicit type class for discrete_linear_ordered_semidom for integral semidomains with a discrete linear order. @@ -149,18 +143,21 @@ trans_on_mult transp_on_multp -* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.) -now requires parentheses in most cases. INCOMPATIBILITY. - -* HOL-Analysis: corrected the definition of convex function (convex_on) -to require the underlying set to be convex. INCOMPATIBILITY. - -* HOL-Complex_Analysis: new, more general definition of meromorphicity. -INCOMPATIBILITY. - -* HOL-Data_Structures: automatic translation from HOL functions into -corresponding step-counting running-time functions. See theory -"HOL-Data_Structures.Define_Time_Function". +* Theory "HOL-ex.Sketch_and_Explore": improvements to generate more +natural and readable proof sketches from proof states. + +* Session "HOL-Analysis": the syntax of Lebesgue integrals (LINT, LBINT, +\<integral>, etc.) now requires parentheses in most cases. INCOMPATIBILITY. + +* Session "HOL-Analysis": corrected the definition of convex function +(convex_on) to require the underlying set to be convex. INCOMPATIBILITY. + +* Session "HOL-Complex_Analysis": new, more general definition of +meromorphicity. INCOMPATIBILITY. + +* Session "HOL-Data_Structures": automatic translation from HOL +functions into corresponding step-counting running-time functions. See +theory "HOL-Data_Structures.Define_Time_Function". *** ML *** @@ -178,6 +175,10 @@ the current thread attributes (normally interruptible). Various examples occur in the Isabelle sources (.ML and .thy files). +* Isabelle/ML explicitly rejects 'handle' with catch-all patterns. +INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or +as last resort declare [[ML_catch_all]] within the theory context. + * ML antiquotation "simproc_setup" inlines an invocation of Simplifier.simproc_setup, using the same concrete syntax as the corresponding Isar command. This allows to introduce a new simproc @@ -193,10 +194,6 @@ to work with several versions of the simproc, e.g. due to locale interpretations. -* Isabelle/ML explicitly rejects 'handle' with catch-all patterns. -INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or -as last resort declare [[ML_catch_all]] within the theory context. - * Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. Exn.is_interrupt covers all kinds of interrupts as before, but @@ -217,14 +214,6 @@ sessions on its own account. INCOMPATIBILITY, use "isabelle build -j1 -H" for the old behaviour, to have the local host participate as worker. -* Directory src/Tools/Demo provides an Isabelle system component with -command-line tool that is implemented in Isabelle/Scala. It serves as -demonstration for user-defined tools. - -* Old $ISABELLE_HOME/bin/isabelle_scala_script has been removed. -Command-line tools in Isabelle/Scala should be provided by a proper -system component with etc/build.props, e.g. see src/Tools/Demo/. - * The Isabelle/Scala module isabelle.Registry provides hierarchic system configuration, based on a collection of TOML files (see also https://toml.io/en/v1.0.0). The settings variable ISABELLE_REGISTRY @@ -253,6 +242,16 @@ component javamail (previously javax.mail) from jakarta 2.1.2 using eclipse angus 2.0.2/2.0.1. +* Isabelle/Scala now has some support for web-apps, using HTML 5 forms. + +* Directory src/Tools/Demo provides an Isabelle system component with +command-line tool that is implemented in Isabelle/Scala. It serves as +demonstration for user-defined tools. + +* Old $ISABELLE_HOME/bin/isabelle_scala_script has been removed. +Command-line tools in Isabelle/Scala should be provided by a proper +system component with etc/build.props, e.g. see src/Tools/Demo/. + * The Isabelle component for the MLton compiler now covers macOS and Linux (Intel), while Windows and Linux (ARM) are unsupported. The default for ISABELLE_MLTON_OPTIONS should work most of the time, but may @@ -270,8 +269,8 @@ isabelle go_setup -p all -* Update to GHC stack 2.15.1 with support for all platforms, including -ARM Linux and Apple Silicon. +* Update to GHC stack-2.15.5, stackage-lts-22.15, ghc-9.6.4 with support +for all platforms, including ARM Linux and Apple Silicon. * Update to .NET / Fsharp 8.0.x: the current long-term support version. @@ -279,8 +278,6 @@ * Update to OpenJDK 21: the current long-term support version of Java. -* Isabelle/Scala now has some support for web-apps, using HTML 5 forms. - New in Isabelle2023 (September 2023)