# HG changeset patch # User wenzelm # Date 1346845443 -7200 # Node ID 4c507e92e4a24fd757b56d77379d15d0d393fd74 # Parent c15a7123605c971bb0c17ac84c892ef3e696e132# Parent 0ee5983e3d59c4eea9050327a0566ddfe599fe33 merged diff -r c15a7123605c -r 4c507e92e4a2 Admin/PLATFORMS --- a/Admin/PLATFORMS Wed Sep 05 11:37:22 2012 +0200 +++ b/Admin/PLATFORMS Wed Sep 05 13:44:03 2012 +0200 @@ -68,9 +68,9 @@ x86-darwin personality usually works seamlessly for C/C++ programs, but the Java 7 platform is only available for x86_64-darwin. -Add-on executables are expected to without manual user configuration, -Each component settings script needs to work out the platform details -appropriately. +Add-on executables are expected to work without manual user +configuration. Each component settings script needs to determine the +platform details appropriately. The Isabelle settings environment provides the following variables to help configuring platform-dependent tools: @@ -88,8 +88,10 @@ Moreover note that ML and JVM usually have a different idea of the platform, depending on the respective binaries that are actually run. -Poly/ML 5.5.x runs most efficiently on 32 bit, even for large -applications. The JVM usually performs better in 64 bit mode. +Poly/ML 5.5.x performs best in 32 bit mode, even for large +applications, thanks to its sophisticated heap management. The JVM +usually works better in 64 bit mode, which allows its heap to grow +beyond 2 GB. The traditional "uname" Unix tool usually only tells about its own executable format, not the underlying platform! @@ -109,8 +111,8 @@ performs not as well in addressing various delicate details of operating system concepts (processes, signals, sockets etc.). -* Scala with Java 1.7. The Isabelle/Scala layer irons out many - oddities and portability issues of the Java platform. +* Scala with Java 1.7. Isabelle/Scala irons out many oddities and + portability issues of the Java platform. Known problems @@ -129,8 +131,7 @@ * The Java runtime has its own idea about the underlying platform, which affects Java native libraries in particular. In - Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM - platform. Since there can be many different Java installations on - the same machine, which can also be run with different options, - reliable JVM platform identification works from inside the running - JVM only. + Isabelle/Scala the function isabelle.Platform.jvm_platform + identifies the JVM platform. Since a particular Java version is + always bundled with Isabelle, the resulting settings also provide + some clues about its platform, without running it. diff -r c15a7123605c -r 4c507e92e4a2 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Wed Sep 05 11:37:22 2012 +0200 +++ b/Admin/isatest/isatest-makedist Wed Sep 05 13:44:03 2012 +0200 @@ -116,7 +116,7 @@ sleep 15 $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2" sleep 15 -$SSH macbroy30 "sleep 10800; $MAKEALL $HOME/settings/mac-poly-M2" +$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2" echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 diff -r c15a7123605c -r 4c507e92e4a2 CONTRIBUTORS --- a/CONTRIBUTORS Wed Sep 05 11:37:22 2012 +0200 +++ b/CONTRIBUTORS Wed Sep 05 13:44:03 2012 +0200 @@ -6,6 +6,10 @@ Contributions to this Isabelle version -------------------------------------- +* September 2012: Christian Sternagel, JAIST + Consolidated HOL/Library (theories: Prefix_Order, Sublist, and + Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists. + * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM New (co)datatype package. diff -r c15a7123605c -r 4c507e92e4a2 NEWS --- a/NEWS Wed Sep 05 11:37:22 2012 +0200 +++ b/NEWS Wed Sep 05 13:44:03 2012 +0200 @@ -41,6 +41,51 @@ *** HOL *** +* Renamed theory Library/List_Prefix to Library/Sublist. +INCOMPATIBILITY. Related changes are: + + - Renamed constants: + + prefix ~> prefixeq + strict_prefix ~> prefix + + Renamed lemmas accordingly, INCOMPATIBILITY. + + - Replaced constant "postfix" by "suffixeq" with swapped argument order + (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped old infix + syntax "xs >>= ys"; use "suffixeq ys xs" instead. Renamed lemmas + accordingly. INCOMPATIBILITY. + + - New constant "emb" for homeomorphic embedding on lists. New + abbreviation "sub" for special case "emb (op =)". + + - Library/Sublist does no longer provide "order" and "bot" type class + instances for the prefix order (merely corresponding locale + interpretations). The type class instances are to be found in + Library/Prefix_Order. INCOMPATIBILITY. + + - The sublist relation from Library/Sublist_Order is now based on + "Sublist.sub". Replaced lemmas: + + le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff + le_list_append_mono ~> Sublist.emb_append_mono + le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2 + le_list_Cons_EX ~> Sublist.emb_ConsD + le_list_drop_Cons2 ~> Sublist.sub_Cons2' + le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq + le_list_drop_Cons ~> Sublist.sub_Cons' + le_list_drop_many ~> Sublist.sub_drop_many + le_list_filter_left ~> Sublist.sub_filter_left + le_list_rev_drop_many ~> Sublist.sub_rev_drop_many + le_list_rev_take_iff ~> Sublist.sub_append + le_list_same_length ~> Sublist.sub_same_length + le_list_take_many_iff ~> Sublist.sub_append' + less_eq_list.drop ~> less_eq_list_drop + less_eq_list.induct ~> less_eq_list_induct + not_le_list_length ~> Sublist.not_sub_length + + INCOMPATIBILITY. + * HOL/Codatatype: New (co)datatype package with support for mixed, nested recursion and interesting non-free datatypes.