misc tuning for release;
authorwenzelm
Tue Apr 02 13:02:03 2019 +0200 (5 months ago)
changeset 700235aef4e9966c4
parent 70022 49e178cbf923
child 70024 f4843d791e70
misc tuning for release;
NEWS
     1.1 --- a/NEWS	Mon Apr 01 21:58:45 2019 +0200
     1.2 +++ b/NEWS	Tue Apr 02 13:02:03 2019 +0200
     1.3 @@ -4,15 +4,11 @@
     1.4  (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
     1.5  
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2019 (June 2019)
    1.10 +-------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 -* Old-style {* verbatim *} tokens are explicitly marked as legacy
    1.15 -feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
    1.16 -via "isabelle update_cartouches -t" (available since Isabelle2015).
    1.17 -
    1.18  * The font family "Isabelle DejaVu" is systematically derived from the
    1.19  existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
    1.20  and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
    1.21 @@ -28,8 +24,13 @@
    1.22  * Old-style inner comments (* ... *) within the term language are no
    1.23  longer supported (legacy feature in Isabelle2018).
    1.24  
    1.25 +* Old-style {* verbatim *} tokens are explicitly marked as legacy
    1.26 +feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
    1.27 +via "isabelle update_cartouches -t" (available since Isabelle2015).
    1.28 +
    1.29  * Infix operators that begin or end with a "*" can now be paranthesized
    1.30 -without additional spaces, eg "(*)" instead of "( * )".
    1.31 +without additional spaces, eg "(*)" instead of "( * )". Minor
    1.32 +INCOMPATIBILITY.
    1.33  
    1.34  * Mixfix annotations may use cartouches instead of old-style double
    1.35  quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
    1.36 @@ -40,13 +41,16 @@
    1.37  need to provide a closed expression -- without trailing semicolon. Minor
    1.38  INCOMPATIBILITY.
    1.39  
    1.40 -* Command keywords of kind thy_decl / thy_goal may be more specifically
    1.41 -fit into the traditional document model of "definition-statement-proof"
    1.42 -via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
    1.43 -
    1.44  
    1.45  *** Isabelle/jEdit Prover IDE ***
    1.46  
    1.47 +* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
    1.48 +DejaVu" collection by default, which provides uniform rendering quality
    1.49 +with the usual Isabelle symbols. Line spacing no longer needs to be
    1.50 +adjusted: properties for the old IsabelleText font had "Global Options /
    1.51 +Text Area / Extra vertical line spacing (in pixels): -2", now it
    1.52 +defaults to 0.
    1.53 +
    1.54  * The jEdit File Browser is more prominent in the default GUI layout of
    1.55  Isabelle/jEdit: various virtual file-systems provide access to Isabelle
    1.56  resources, notably via "favorites:" (or "Edit Favorites").
    1.57 @@ -61,29 +65,23 @@
    1.58  entries are structured according to chapter / session names, the open
    1.59  operation is redirected to the session ROOT file.
    1.60  
    1.61 -* System option "jedit_text_overview" allows to disable the text
    1.62 -overview column.
    1.63 -
    1.64 -* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
    1.65 -DejaVu" collection by default, which provides uniform rendering quality
    1.66 -with the usual Isabelle symbols. Line spacing no longer needs to be
    1.67 -adjusted: properties for the old IsabelleText font had "Global Options /
    1.68 -Text Area / Extra vertical line spacing (in pixels): -2", now it
    1.69 -defaults to 0.
    1.70 -
    1.71 -* Improved sub-pixel font rendering (especially on Linux), thanks to
    1.72 -OpenJDK 11.
    1.73 -
    1.74  * Support for user-defined file-formats via class isabelle.File_Format
    1.75  in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
    1.76  the shell function "isabelle_file_format" in etc/settings (e.g. of an
    1.77  Isabelle component).
    1.78  
    1.79 +* System option "jedit_text_overview" allows to disable the text
    1.80 +overview column.
    1.81 +
    1.82  * Command-line options "-s" and "-u" of "isabelle jedit" override the
    1.83  default for system option "system_heaps" that determines the heap
    1.84  storage directory for "isabelle build". Option "-n" is now clearly
    1.85  separated from option "-s".
    1.86  
    1.87 +* Update to OpenJDK 11, which is the current long-term support line
    1.88 +after Java 8. It provides a very different font renderer, with improved
    1.89 +sub-pixel font rendering.
    1.90 +
    1.91  
    1.92  *** Document preparation ***
    1.93  
    1.94 @@ -102,36 +100,20 @@
    1.95  
    1.96  *** Isar ***
    1.97  
    1.98 -* More robust treatment of structural errors: begin/end blocks take
    1.99 -precedence over goal/proof.
   1.100 -
   1.101  * Implicit cases goal1, goal2, goal3, etc. have been discontinued
   1.102  (legacy feature since Isabelle2016).
   1.103  
   1.104 +* More robust treatment of structural errors: begin/end blocks take
   1.105 +precedence over goal/proof. This is particularly relevant for the
   1.106 +headless PIDE session and server.
   1.107 +
   1.108 +* Command keywords of kind thy_decl / thy_goal may be more specifically
   1.109 +fit into the traditional document model of "definition-statement-proof"
   1.110 +via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
   1.111 +
   1.112  
   1.113  *** HOL ***
   1.114  
   1.115 -* Formal Laurent series and overhaul of Formal power series 
   1.116 -in session HOL-Computational_Algebra.
   1.117 -
   1.118 -* Exponentiation by squaring in session HOL-Library; used for computing
   1.119 -powers in class monoid_mult and modular exponentiation in session
   1.120 -HOL-Number_Theory.
   1.121 -
   1.122 -* More material on residue rings in session HOL-Number_Theory:
   1.123 -Carmichael's function, primitive roots, more properties for "ord".
   1.124 -
   1.125 -* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
   1.126 -(not the corresponding binding operators) now have the same precedence
   1.127 -as any other prefix function symbol.  Minor INCOMPATIBILITY.
   1.128 -
   1.129 -* Slightly more conventional naming schema in structure Inductive.
   1.130 -Minor INCOMPATIBILITY.
   1.131 -
   1.132 -* Various _global variants of specification tools have been removed.
   1.133 -Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result]
   1.134 -to lift specifications to the global theory level.
   1.135 -
   1.136  * Command 'export_code' produces output as logical files within the
   1.137  theory context, as well as formal session exports that can be
   1.138  materialized via command-line tools "isabelle export" or "isabelle build
   1.139 @@ -165,16 +147,15 @@
   1.140  proper module frame, nothing is added magically any longer.
   1.141  INCOMPATIBILITY.
   1.142  
   1.143 -* Code generation: slightly more conventional syntax for
   1.144 -'code_stmts' antiquotation.  Minor INCOMPATIBILITY.
   1.145 -
   1.146 -* The simplifier uses image_cong_simp as a congruence rule. The historic
   1.147 -and not really well-formed congruence rules INF_cong*, SUP_cong*,
   1.148 -are not used by default any longer.  INCOMPATIBILITY; consider using
   1.149 -declare image_cong_simp [cong del] in extreme situations.
   1.150 -
   1.151 -* INF_image and SUP_image are no default simp rules any longer.
   1.152 -INCOMPATIBILITY, prefer image_comp as simp rule if needed.
   1.153 +* Code generation: slightly more conventional syntax for 'code_stmts'
   1.154 +antiquotation. Minor INCOMPATIBILITY.
   1.155 +
   1.156 +* Theory List: the precedence of the list_update operator has changed:
   1.157 +"f a [n := x]" now needs to be written "(f a)[n := x]".
   1.158 +
   1.159 +* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
   1.160 +now have the same precedence as any other prefix function symbol. Minor
   1.161 +INCOMPATIBILITY.
   1.162  
   1.163  * Simplified syntax setup for big operators under image. In rare
   1.164  situations, type conversions are not inserted implicitly any longer
   1.165 @@ -182,53 +163,87 @@
   1.166  SUPREMUM, UNION, INTER should now rarely occur in output and are just
   1.167  retained as migration auxiliary. INCOMPATIBILITY.
   1.168  
   1.169 -* Theory List: the precedence of the list_update operator has changed:
   1.170 -"f a [n := x]" now needs to be written "(f a)[n := x]".
   1.171 -
   1.172 -* Theory "HOL-Library.Multiset": the <Union># operator now has the same
   1.173 -precedence as any other prefix function symbol.
   1.174 -
   1.175 -* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
   1.176 -
   1.177 -* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
   1.178 -and prod_mset.swap, similarly to sum.swap and prod.swap.
   1.179 -INCOMPATIBILITY.
   1.180 +* The simplifier uses image_cong_simp as a congruence rule. The historic
   1.181 +and not really well-formed congruence rules INF_cong*, SUP_cong*, are
   1.182 +not used by default any longer. INCOMPATIBILITY; consider using declare
   1.183 +image_cong_simp [cong del] in extreme situations.
   1.184 +
   1.185 +* INF_image and SUP_image are no default simp rules any longer.
   1.186 +INCOMPATIBILITY, prefer image_comp as simp rule if needed.
   1.187  
   1.188  * Strong congruence rules (with =simp=> in the premises) for constant f
   1.189  are now uniformly called f_cong_simp, in accordance with congruence
   1.190  rules produced for mappers by the datatype package. INCOMPATIBILITY.
   1.191  
   1.192 -* Sledgehammer:
   1.193 -  - The URL for SystemOnTPTP, which is used by remote provers, has
   1.194 -    been updated.
   1.195 -  - The machine-learning-based filter MaSh has been optimized to take
   1.196 -    less time (in most cases).
   1.197 -
   1.198 -* SMT: reconstruction is now possible using the SMT solver veriT.
   1.199 -
   1.200 -* HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping 
   1.201 -and non-exhaustive patterns and handles arbitrarily nested patterns.
   1.202 -It uses on the same algorithm as HOL-Library.Code_Lazy, which assumes
   1.203 -sequential left-to-right pattern matching. The generated
   1.204 +* Retired lemma card_Union_image; use the simpler card_UN_disjoint
   1.205 +instead. INCOMPATIBILITY.
   1.206 +
   1.207 +* Facts sum_mset.commute and prod_mset.commute have been renamed to
   1.208 +sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
   1.209 +INCOMPATIBILITY.
   1.210 +
   1.211 +* ML structure Inductive: slightly more conventional naming schema.
   1.212 +Minor INCOMPATIBILITY.
   1.213 +
   1.214 +* ML: Various _global variants of specification tools have been removed.
   1.215 +Minor INCOMPATIBILITY, prefer combinators
   1.216 +Named_Target.theory_map[_result] to lift specifications to the global
   1.217 +theory level.
   1.218 +
   1.219 +* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
   1.220 +overlapping and non-exhaustive patterns and handles arbitrarily nested
   1.221 +patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
   1.222 +assumes sequential left-to-right pattern matching. The generated
   1.223  equation no longer tuples the arguments on the right-hand side.
   1.224  INCOMPATIBILITY.
   1.225  
   1.226 +* Theory HOL-Library.Multiset: the <Union># operator now has the same
   1.227 +precedence as any other prefix function symbol.
   1.228 +
   1.229 +* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
   1.230 +used for computing powers in class "monoid_mult" and modular
   1.231 +exponentiation.
   1.232 +
   1.233 +* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
   1.234 +of Formal power series.
   1.235 +
   1.236 +* Session HOL-Number_Theory: More material on residue rings in
   1.237 +Carmichael's function, primitive roots, more properties for "ord".
   1.238 +
   1.239  * Session HOL-SPARK: .prv files are no longer written to the
   1.240  file-system, but exported to the session database. Results may be
   1.241  retrieved with the "isabelle export" command-line tool like this:
   1.242  
   1.243    isabelle export -x "*:**.prv" HOL-SPARK-Examples
   1.244  
   1.245 +* Sledgehammer:
   1.246 +  - The URL for SystemOnTPTP, which is used by remote provers, has been
   1.247 +    updated.
   1.248 +  - The machine-learning-based filter MaSh has been optimized to take
   1.249 +    less time (in most cases).
   1.250 +
   1.251 +* SMT: reconstruction is now possible using the SMT solver veriT.
   1.252 +
   1.253  
   1.254  *** ML ***
   1.255  
   1.256 -* Local_Theory.reset is no longer available in user space. Regular
   1.257 -definitional packages should use balanced blocks of
   1.258 -Local_Theory.open_target versus Local_Theory.close_target instead,
   1.259 -or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
   1.260 -
   1.261 -* Original PolyML.pointerEq is retained as a convenience for tools that
   1.262 -don't use Isabelle/ML (where this is called "pointer_eq").
   1.263 +* Command 'generate_file' allows to produce sources for other languages,
   1.264 +with antiquotations in the Isabelle context (only the control-cartouche
   1.265 +form). The default "cartouche" antiquotation evaluates an ML expression
   1.266 +of type string and inlines the result as a string literal of the target
   1.267 +language. For example, this works for Haskell as follows:
   1.268 +
   1.269 +  generate_file "Pure.hs" = \<open>
   1.270 +  module Isabelle.Pure where
   1.271 +    allConst, impConst, eqConst :: String
   1.272 +    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
   1.273 +    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
   1.274 +    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
   1.275 +  \<close>
   1.276 +
   1.277 +The ML function Generate_File.generate writes all generated files from a
   1.278 +given theory to the file-system, e.g. a temporary directory where some
   1.279 +external compiler is applied.
   1.280  
   1.281  * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
   1.282  option ML_environment to select a named environment, such as "Isabelle"
   1.283 @@ -257,36 +272,44 @@
   1.284  preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
   1.285  useful.
   1.286  
   1.287 -* Command 'generate_file' allows to produce sources for other languages,
   1.288 -with antiquotations in the Isabelle context (only the control-cartouche
   1.289 -form). The default "cartouche" antiquotation evaluates an ML expression
   1.290 -of type string and inlines the result as a string literal of the target
   1.291 -language. For example, this works for Haskell as follows:
   1.292 -
   1.293 -  generate_file "Pure.hs" = \<open>
   1.294 -  module Isabelle.Pure where
   1.295 -    allConst, impConst, eqConst :: String
   1.296 -    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
   1.297 -    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
   1.298 -    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
   1.299 -  \<close>
   1.300 -
   1.301 -The ML function Generate_File.generate writes all generated files from a
   1.302 -given theory to the file-system, e.g. a temporary directory where some
   1.303 -external compiler is applied.
   1.304 +* Local_Theory.reset is no longer available in user space. Regular
   1.305 +definitional packages should use balanced blocks of
   1.306 +Local_Theory.open_target versus Local_Theory.close_target instead, or
   1.307 +the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
   1.308 +
   1.309 +* Original PolyML.pointerEq is retained as a convenience for tools that
   1.310 +don't use Isabelle/ML (where this is called "pointer_eq").
   1.311  
   1.312  
   1.313  *** System ***
   1.314  
   1.315 -* The command-line option "isabelle build -e" retrieves theory exports
   1.316 -from the session build database, using 'export_files' in session ROOT
   1.317 -entries.
   1.318 -
   1.319 -* The system option "system_heaps" determines where to store the session
   1.320 +* Update to Java 11: the current long-term support version of OpenJDK.
   1.321 +
   1.322 +* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
   1.323 +the full overhead of 64-bit values everywhere. This special x86_64_32
   1.324 +mode provides up to 16GB ML heap, while program code and stacks are
   1.325 +allocated elsewhere. Thus approx. 5 times more memory is available for
   1.326 +applications compared to old x86 mode (which is no longer used by
   1.327 +Isabelle). The switch to the x86_64 CPU architecture also avoids
   1.328 +compatibility problems with Linux and macOS, where 32-bit applications
   1.329 +are gradually phased out.
   1.330 +
   1.331 +* System option "checkpoint" has been discontinued: obsolete thanks to
   1.332 +improved memory management in Poly/ML.
   1.333 +
   1.334 +* System option "system_heaps" determines where to store the session
   1.335  image of "isabelle build" (and other tools using that internally).
   1.336  Former option "-s" is superseded by option "-o system_heaps".
   1.337  INCOMPATIBILITY in command-line syntax.
   1.338  
   1.339 +* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
   1.340 +source modules for Isabelle tools implemented in Haskell, notably for
   1.341 +Isabelle/PIDE.
   1.342 +
   1.343 +* The command-line tool "isabelle build -e" retrieves theory exports
   1.344 +from the session build database, using 'export_files' in session ROOT
   1.345 +entries.
   1.346 +
   1.347  * The command-line tool "isabelle update" uses Isabelle/PIDE in
   1.348  batch-mode to update theory sources based on semantic markup produced in
   1.349  Isabelle/ML. Actual updates depend on system options that may be enabled
   1.350 @@ -303,11 +326,7 @@
   1.351  function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
   1.352  component).
   1.353  
   1.354 -* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
   1.355 -source modules for Isabelle tools implemented in Haskell, notably for
   1.356 -Isabelle/PIDE.
   1.357 -
   1.358 -* Isabelle server command "use_theories" supports "nodes_status_delay"
   1.359 +* Isabelle Server command "use_theories" supports "nodes_status_delay"
   1.360  for continuous output of node status information. The time interval is
   1.361  specified in seconds; a negative value means it is disabled (default).
   1.362  
   1.363 @@ -351,20 +370,6 @@
   1.364  ISABELLE_OPAM_ROOT, or by resetting these variables in
   1.365  $ISABELLE_HOME_USER/etc/settings.
   1.366  
   1.367 -* Update to Java 11: the latest long-term support version of OpenJDK.
   1.368 -
   1.369 -* System option "checkpoint" has been discontinued: obsolete thanks to
   1.370 -improved memory management in Poly/ML.
   1.371 -
   1.372 -* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
   1.373 -the full overhead of 64-bit values everywhere. This special x86_64_32
   1.374 -mode provides up to 16GB ML heap, while program code and stacks are
   1.375 -allocated elsewhere. Thus approx. 5 times more memory is available for
   1.376 -applications compared to old x86 mode (which is no longer used by
   1.377 -Isabelle). The switch to the x86_64 CPU architecture also avoids
   1.378 -compatibility problems with Linux and macOS, where 32-bit applications
   1.379 -are gradually phased out.
   1.380 -
   1.381  
   1.382  
   1.383  New in Isabelle2018 (August 2018)