Admin/PLATFORMS
changeset 49144 84699f37481d
parent 48836 90a0af19004c
child 55391 eae296b5ef33
equal deleted inserted replaced
49143:ae4fe6e4c3c0 49144:84699f37481d
    66 libraries, so native x86_64-linux needs to be used by default, despite
    66 libraries, so native x86_64-linux needs to be used by default, despite
    67 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    67 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    68 x86-darwin personality usually works seamlessly for C/C++ programs,
    68 x86-darwin personality usually works seamlessly for C/C++ programs,
    69 but the Java 7 platform is only available for x86_64-darwin.
    69 but the Java 7 platform is only available for x86_64-darwin.
    70 
    70 
    71 Add-on executables are expected to without manual user configuration,
    71 Add-on executables are expected to work without manual user
    72 Each component settings script needs to work out the platform details
    72 configuration.  Each component settings script needs to determine the
    73 appropriately.
    73 platform details appropriately.
    74 
    74 
    75 The Isabelle settings environment provides the following variables to
    75 The Isabelle settings environment provides the following variables to
    76 help configuring platform-dependent tools:
    76 help configuring platform-dependent tools:
    77 
    77 
    78   ISABELLE_PLATFORM64  (potentially empty)
    78   ISABELLE_PLATFORM64  (potentially empty)
    86 
    86 
    87   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    87   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    88 
    88 
    89 Moreover note that ML and JVM usually have a different idea of the
    89 Moreover note that ML and JVM usually have a different idea of the
    90 platform, depending on the respective binaries that are actually run.
    90 platform, depending on the respective binaries that are actually run.
    91 Poly/ML 5.5.x runs most efficiently on 32 bit, even for large
    91 Poly/ML 5.5.x performs best in 32 bit mode, even for large
    92 applications.  The JVM usually performs better in 64 bit mode.
    92 applications, thanks to its sophisticated heap management.  The JVM
       
    93 usually works better in 64 bit mode, which allows its heap to grow
       
    94 beyond 2 GB.
    93 
    95 
    94 The traditional "uname" Unix tool usually only tells about its own
    96 The traditional "uname" Unix tool usually only tells about its own
    95 executable format, not the underlying platform!
    97 executable format, not the underlying platform!
    96 
    98 
    97 
    99 
   107 * Perl as largely portable system programming language.  In some
   109 * Perl as largely portable system programming language.  In some
   108   situations Python may serve as an alternative, but it usually
   110   situations Python may serve as an alternative, but it usually
   109   performs not as well in addressing various delicate details of
   111   performs not as well in addressing various delicate details of
   110   operating system concepts (processes, signals, sockets etc.).
   112   operating system concepts (processes, signals, sockets etc.).
   111 
   113 
   112 * Scala with Java 1.7.  The Isabelle/Scala layer irons out many
   114 * Scala with Java 1.7.  Isabelle/Scala irons out many oddities and
   113   oddities and portability issues of the Java platform.
   115   portability issues of the Java platform.
   114 
   116 
   115 
   117 
   116 Known problems
   118 Known problems
   117 --------------
   119 --------------
   118 
   120 
   127   Such add-ons are usually included in Apple's /usr/bin/perl by
   129   Such add-ons are usually included in Apple's /usr/bin/perl by
   128   default.
   130   default.
   129 
   131 
   130 * The Java runtime has its own idea about the underlying platform,
   132 * The Java runtime has its own idea about the underlying platform,
   131   which affects Java native libraries in particular.  In
   133   which affects Java native libraries in particular.  In
   132   Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   134   Isabelle/Scala the function isabelle.Platform.jvm_platform
   133   platform.  Since there can be many different Java installations on
   135   identifies the JVM platform.  Since a particular Java version is
   134   the same machine, which can also be run with different options,
   136   always bundled with Isabelle, the resulting settings also provide
   135   reliable JVM platform identification works from inside the running
   137   some clues about its platform, without running it.
   136   JVM only.