# HG changeset patch # User haftmann # Date 1271739230 -7200 # Node ID 27137425b102036b1a193bbbb624b7baadbf146b # Parent 74c5e6e3c1d345ef543dadfe8c71b94b0e4bcb0a# Parent 03a41196a9a0ffc0a7432111f5aa2ea403eb7565 merged diff -r 03a41196a9a0 -r 27137425b102 Admin/PLATFORMS --- a/Admin/PLATFORMS Mon Apr 19 15:31:58 2010 +0200 +++ b/Admin/PLATFORMS Tue Apr 20 06:53:50 2010 +0200 @@ -1,5 +1,5 @@ -Some notes on platform support of Isabelle -========================================== +Some notes on multi-platform support of Isabelle +================================================ Preamble -------- @@ -11,32 +11,34 @@ The basic Isabelle system infrastructure provides some facilities to make this work, e.g. see the ML structures File and Path, or functions like bash_output. The settings environment also provides some means -for portability, e.g. jvm_path to hold up the impression that even -Java on Windows/Cygwin adheres to Isabelle/POSIX standards. +for portability, e.g. jvm_path to hold up the impression that Java on +Windows/Cygwin adheres to Isabelle/POSIX standards. When producing add-on tools, it is important to stay within this clean room of Isabelle, and refrain from overly ambitious system hacking. +The existing Isabelle scripts follow a certain style that might look +odd at first sight, but reflects long years of experience in getting +system plumbing right (which is quite hard). Supported platforms ------------------- The following hardware and operating system platforms are officially -supported by the Isabelle distribution (and bundled tools): - - x86-linux - x86-darwin - x86-cygwin - x86_64-linux - x86_64-darwin +supported by the Isabelle distribution (and bundled tools), with the +following reference versions (which have been selected to be neither +too old nor too new): -As of Cygwin 1.7 there is only a 32 bit version of that platform. The -other 64 bit platforms become more and more important for power users -and always need to be taken into account when testing tools. + x86-linux Ubuntu 8.04 LTS Server + x86-darwin Mac OS Leopard + x86-cygwin Cygwin 1.7 -All of the above platforms are 100% supported -- end-users should not -have to care about the differences at all. There are also some -secondary platforms where Poly/ML also happens to work: + x86_64-linux Ubuntu 8.04 LTS Server (64) + x86_64-darwin Mac OS Leopard + +All of the above platforms are 100% supported by Isabelle -- end-users +should not have to care about the differences at all. There are also +some secondary platforms where Poly/ML also happens to work: ppc-darwin sparc-solaris @@ -45,7 +47,27 @@ There is no guarantee that Isabelle add-ons work on these fringe platforms. Even Isabelle/Scala already fails on ppc-darwin due to -lack of JVM 1.6 support on that platform. +lack of JVM 1.6 support by Apple. + + +32 bit vs. 64 bit platforms +--------------------------- + +64 bit hardware becomes more and more important for power users. +Add-on tools need to work seamlessly without manual user +configuration, although it is often sufficient to fall back on 32 bit +executables. + +The ISABELLE_PLATFORM setting variable refers to the 32 bit version of +the platform, even on 64 bit hardware. Power-tools need to indicate +64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64 +setting. The following bash expressions prefers the 64 bit platform, +if that is available: + + "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}" + +Note that ML and JVM may have a different idea of the platform, +depending the the respective binaries that are actually run. Dependable system tools @@ -53,17 +75,17 @@ The following portable system tools can be taken for granted: - * GNU bash as uniform shell on all platforms. Note that the POSIX - "standard" shell /bin/sh is *not* appropriate, because there are - too many different implementations of it. +* GNU bash as uniform shell on all platforms. The POSIX "standard" + shell /bin/sh is *not* appropriate, because there are too many + different implementations of it. - * Perl as largely portable system programming language. In some - situations Python may as an alternative, but it usually performs - not as well in addressing various delicate details of basic - operating system concepts (processes, signals, sockets etc.). +* Perl as largely portable system programming language. In some + situations Python may serve as an alternative, but it usually + performs not as well in addressing various delicate details of + operating system concepts (processes, signals, sockets etc.). - * Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons - out many oddities and portability problems of the Java platform. +* Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons + out many oddities and portability problems of the Java platform. Known problems @@ -71,11 +93,18 @@ * Mac OS: If MacPorts is installed and its version of Perl takes precedence over /usr/bin/perl in the PATH, then the end-user needs - to take care of installing add-on modules, e.g. HTTP support. Such - add-ons are usually included in Apple's /usr/bin/perl by default. + to take care of installing extra modules, e.g. for HTTP support. + Such add-ons are usually included in Apple's /usr/bin/perl by + default. * The Java runtime has its own idea about the underlying platform, - e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM + e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM could be x86_64-linux. This affects Java native libraries in - particular -- which are very hard to support in a platform - independent manner, and should be avoided in the first place. + particular -- which cause extra portability problems and can make + the JVM crash anyway. + + 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. diff -r 03a41196a9a0 -r 27137425b102 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Apr 19 15:31:58 2010 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 20 06:53:50 2010 +0200 @@ -290,15 +290,14 @@ val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation, token_translation} = syn_ext; - val input' = if inout then fold (insert (op =)) xprods input else input; - val changed = length input <> length input'; + val new_xprods = + if inout then distinct (op =) (filter_out (member (op =) input) xprods) else []; fun if_inout xs = if inout then xs else []; in Syntax - ({input = input', - lexicon = - if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon, - gram = if changed then Parser.extend_gram gram xprods else gram, + ({input = new_xprods @ input, + lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon, + gram = Parser.extend_gram gram new_xprods, consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2), prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)), parse_ast_trtab = diff -r 03a41196a9a0 -r 27137425b102 src/Pure/System/gui_setup.scala --- a/src/Pure/System/gui_setup.scala Mon Apr 19 15:31:58 2010 +0200 +++ b/src/Pure/System/gui_setup.scala Tue Apr 20 06:53:50 2010 +0200 @@ -43,15 +43,16 @@ } // values - text.append("JVM platform: " + Platform.jvm_platform() + "\n") if (Platform.is_windows) text.append("Cygwin root: " + Cygwin.check_root() + "\n") + text.append("JVM platform: " + Platform.jvm_platform + "\n") try { val isabelle_system = new Isabelle_System - text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n") + text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n") text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n") val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64") if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n") + text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n") text.append("Isabelle java: " + isabelle_system.this_java() + "\n") } catch { case e: RuntimeException => text.append(e.getMessage + "\n") diff -r 03a41196a9a0 -r 27137425b102 src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Mon Apr 19 15:31:58 2010 +0200 +++ b/src/Pure/System/platform.scala Tue Apr 20 06:53:50 2010 +0200 @@ -31,7 +31,7 @@ private val Sparc = new Regex("sparc") private val PPC = new Regex("PowerPC|ppc") - def jvm_platform(): String = + lazy val jvm_platform: String = { val arch = java.lang.System.getProperty("os.arch") match {