# HG changeset patch # User wenzelm # Date 1633199233 -7200 # Node ID 5294a44efc49e950cb6300ec415481515bda8bfd # Parent b618749bb8f4147a1d6ef46ac5652cb913f6cfbf misc tuning for release; diff -r b618749bb8f4 -r 5294a44efc49 NEWS --- a/NEWS Sat Oct 02 20:00:02 2021 +0200 +++ b/NEWS Sat Oct 02 20:27:13 2021 +0200 @@ -4,16 +4,16 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) -New in this Isabelle version ----------------------------- +New in Isabelle2021 (December 2021) +----------------------------------- *** General *** * Commands 'syntax' and 'no_syntax' now work in a local theory context, -but there is no proper way to refer to local entities --- in contrast to -'notation' and 'no_notation'. Local syntax works well with 'bundle', -e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of -Isabelle/HOL. +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. * Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled @@ -26,19 +26,6 @@ theorem test by (simp add: test_def) end -* 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 -INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties -https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html - * More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit. @@ -143,6 +130,63 @@ *** HOL *** +* 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 +potential for change can be avoided if interpretations of type class +"order" are replaced or augmented by interpretations of locale +"ordering". + +* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor +INCOMPATIBILITY; note that for most applications less elementary lemmas +exists. + +* Lemma "permutes_induct" has been given stronger hypotheses and named +premises. INCOMPATIBILITY. + +* Combinator "Fun.swap" resolved into a mere input abbreviation in +separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. + +* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in +bundle bit_operations_syntax. INCOMPATIBILITY. + +* Bit operations set_bit, unset_bit and flip_bit are now class +operations. INCOMPATIBILITY. + +* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY. + +* Simplified class hierarchy for bit operations: bit operations reside +in classes (semi)ring_bit_operations, class semiring_bit_shifts is +gone. + +* Expressions of the form "NOT (numeral _)" are not simplified by +default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq +as simp rule explicitly if needed. + +* Abbreviation "max_word" has been moved to session Word_Lib in the AFP, +as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", +"setBit", "clearBit". See there further the changelog in theory Guide. +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 +INCOMPATIBILITY. + +* Sledgehammer: + - Removed legacy "lam_lifting" (synonym for "lifting") from option + "lam_trans". Minor INCOMPATIBILITY. + - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor + INCOMPATIBILITY. + - Added "opaque_combs" to option "lam_trans": lambda expressions are + rewritten using combinators, but the combinators are kept opaque, + i.e. without definitions. + +* Metis: Renamed option "hide_lams" to "opaque_lifting". Minor +INCOMPATIBILITY. + * 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 @@ -181,20 +225,9 @@ 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 +with the function "arg" of Complex_Main, renaming arg ~> Arg also in the names of arg_bounded. Minor INCOMPATIBILITY. -* 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 -potential for change can be avoided if interpretations of type class -"order" are replaced or augmented by interpretations of locale -"ordering". - -* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor -INCOMPATIBILITY; note that for most applications less elementary lemmas -exists. - * 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". @@ -208,52 +241,6 @@ * Theory "HOL-Combinatorics.Transposition" provides elementary swap operation "transpose". -* Lemma "permutes_induct" has been given stronger hypotheses and named -premises. INCOMPATIBILITY. - -* Combinator "Fun.swap" resolved into a mere input abbreviation in -separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. - -* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in -bundle bit_operations_syntax. INCOMPATIBILITY. - -* Bit operations set_bit, unset_bit and flip_bit are now class -operations. INCOMPATIBILITY. - -* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY. - -* Simplified class hierarchy for bit operations: bit operations reside -in classes (semi)ring_bit_operations, class semiring_bit_shifts is -gone. - -* Expressions of the form "NOT (numeral _)" are not simplified by -default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq -as simp rule explicitly if needed. - -* Abbreviation "max_word" has been moved to session Word_Lib in the AFP, -as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", -"setBit", "clearBit". See there further the changelog in theory Guide. -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 -INCOMPATIBILITY. - -* Sledgehammer: - - Removed legacy "lam_lifting" (synonym for "lifting") from option - "lam_trans". Minor INCOMPATIBILITY. - - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". - Minor INCOMPATIBILITY. - - Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten - using combinators, but the combinators are kept opaque, i.e. without - definitions. - -* Metis: - - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. - *** ML *** @@ -380,6 +367,17 @@ - Isabelle_System.rm_tree - Isabelle_System.download +* ML profiling has been updated and reactivated, after some degration in +Isabelle2021: + + - "isabelle build -o threads=1 -o profiling=..." works properly + within the PIDE session context; + + - "isabelle profiling_report" now uses the session build database + (like "isabelle log"); + + - output uses non-intrusive tracing messages, instead of warnings. + *** System *** @@ -406,16 +404,18 @@ isabelle.jedit module is now part of Isabelle/Scala (as one big $ISABELLE_SCALA_JAR). -* ML profiling has been updated and reactivated, after some degration in -Isabelle2021: - - - "isabelle build -o threads=1 -o profiling=..." works properly - within the PIDE session context; - - - "isabelle profiling_report" now uses the session build database - (like "isabelle log"); - - - output uses non-intrusive tracing messages, instead of warnings. +* 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 +INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties +https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html * System option "system_log" specifies an optional log file for internal messages produced by Output.system_message in Isabelle/ML; the value @@ -429,7 +429,7 @@ can be used in the short form. E.g. "isabelle build -o document". * Command-line tool "isabelle version" supports repository archives -(without full .hg directory). More options. +(without full .hg directory). It also provides more options. * Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued. Note that only Windows supports old 32 bit executables, via settings