Admin/PLATFORMS
changeset 46006 36cd232b18bb
parent 44977 1b2ce8d0f8e3
child 48833 10584ca5785f
equal deleted inserted replaced
46005:ae721b158a79 46006:36cd232b18bb
    59 
    59 
    60 
    60 
    61 32 bit vs. 64 bit platforms
    61 32 bit vs. 64 bit platforms
    62 ---------------------------
    62 ---------------------------
    63 
    63 
    64 64 bit hardware becomes more and more important for many users.
    64 Most users already have 64 bit hardware, and many of them are running
    65 Add-on tools need to work seamlessly without manual user
    65 a 64 bit operating system.  Native 64 bit support for ML and Scala/JVM
    66 configuration, although it is often sufficient to fall back on 32 bit
    66 is increasingly important for big Isabelle applications, but 32 bit is
    67 executables.
    67 often the default to get started.  Add-on executables need to work
       
    68 seamlessly without manual user configuration, either as native 64 bit
       
    69 executables or in 32 bit mode on a 64 bit platform.
    68 
    70 
    69 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    71 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    70 the platform, even on 64 bit hardware.  Power-tools need to indicate
    72 the platform, even on 64 bit hardware.  Tools need to indicate 64 bit
    71 64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
    73 support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
    72 setting.  The following bash expression prefers the 64 bit platform,
    74 this is really required.  The following bash expression prefers the 64
    73 if that is available:
    75 bit platform, if that is available:
    74 
    76 
    75   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
    77   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
    76 
    78 
    77 Note that ML and JVM may have a different idea of the platform,
    79 Note that ML and JVM may have a different idea of the platform,
    78 depending on the respective binaries that are actually run.
    80 depending on the respective binaries that are actually run.  The
       
    81 "uname" Unix tool usually only tells about its own executable format,
       
    82 not the underlying platform.
    79 
    83 
    80 
    84 
    81 Dependable system tools
    85 Dependable system tools
    82 -----------------------
    86 -----------------------
    83 
    87