Admin/PLATFORMS
changeset 65073 b5bf76cf2b4e
parent 64406 492de9062cd2
child 65369 27c1b5e952bd
equal deleted inserted replaced
65072:36c650d1a90d 65073:b5bf76cf2b4e
    55 Most users have 64 bit hardware and are running a 64 bit operating
    55 Most users have 64 bit hardware and are running a 64 bit operating
    56 system by default.  For Linux this usually means missing 32 bit shared
    56 system by default.  For Linux this usually means missing 32 bit shared
    57 libraries, so native x86_64-linux needs to be used by default, despite
    57 libraries, so native x86_64-linux needs to be used by default, despite
    58 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    58 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    59 x86-darwin personality usually works seamlessly for C/C++ programs,
    59 x86-darwin personality usually works seamlessly for C/C++ programs,
    60 but the Java platform is only available for x86_64-darwin.
    60 but the Java platform is always for x86_64-darwin.
    61 
    61 
    62 Add-on executables are expected to work without manual user
    62 Add-on executables are expected to work without manual user
    63 configuration.  Each component settings script needs to determine the
    63 configuration.  Each component settings script needs to determine the
    64 platform details appropriately.
    64 platform details appropriately.
       
    65 
    65 
    66 
    66 The Isabelle settings environment provides the following variables to
    67 The Isabelle settings environment provides the following variables to
    67 help configuring platform-dependent tools:
    68 help configuring platform-dependent tools:
    68 
    69 
    69   ISABELLE_PLATFORM64  (potentially empty)
    70   ISABELLE_PLATFORM64  (potentially empty)
    74 the platform, even on 64 bit hardware.  Using regular bash notation,
    75 the platform, even on 64 bit hardware.  Using regular bash notation,
    75 tools may express their preference for 64 bit with a fall-back for 32
    76 tools may express their preference for 64 bit with a fall-back for 32
    76 bit as follows:
    77 bit as follows:
    77 
    78 
    78   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    79   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
       
    80 
       
    81 
       
    82 There is a second set of settings for native Windows (instead of the
       
    83 POSIX emulation of Cygwin used before):
       
    84 
       
    85   ISABELLE_WINDOWS_PLATFORM64  (potentially empty)
       
    86   ISABELLE_WINDOWS_PLATFORM32
       
    87   ISABELLE_WINDOWS_PLATFORM
       
    88 
       
    89 It can be used like this:
       
    90 
       
    91   "${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"
       
    92 
       
    93   "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
       
    94 
    79 
    95 
    80 Moreover note that ML and JVM usually have a different idea of the
    96 Moreover note that ML and JVM usually have a different idea of the
    81 platform, depending on the respective binaries that are actually run.
    97 platform, depending on the respective binaries that are actually run.
    82 Poly/ML 5.6.x performs best in 32 bit mode, even for large
    98 Poly/ML 5.6.x performs best in 32 bit mode, even for large
    83 applications, thanks to its sophisticated heap management.  The JVM
    99 applications, thanks to its sophisticated heap management.  The JVM