added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
authorwenzelm
Sat Apr 17 22:58:29 2010 +0200 (2010-04-17)
changeset 36196cbb9ee265cdd
parent 36195 9c098598db2a
child 36197 2e92aca73cab
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/document/Basics.tex
lib/scripts/getsettings
lib/scripts/isabelle-platform
     1.1 --- a/doc-src/System/Thy/Basics.thy	Sat Apr 17 21:40:29 2010 +0200
     1.2 +++ b/doc-src/System/Thy/Basics.thy	Sat Apr 17 22:58:29 2010 +0200
     1.3 @@ -162,6 +162,17 @@
     1.4    some extend. In particular, site-wide defaults may be overridden by
     1.5    a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
     1.6    
     1.7 +  \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
     1.8 +  set to a symbolic identifier for the underlying hardware and
     1.9 +  operating system.  The Isabelle platform identification always
    1.10 +  refers to the 32 bit variant, even this is a 64 bit machine.  Note
    1.11 +  that the ML or Java runtime may have a different idea, depending on
    1.12 +  which binaries are actually run.
    1.13 +
    1.14 +  \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
    1.15 +  @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
    1.16 +  on a platform that supports this; the value is empty for 32 bit.
    1.17 +
    1.18    \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
    1.19    ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
    1.20    names of the @{executable "isabelle-process"} and @{executable
     2.1 --- a/doc-src/System/Thy/document/Basics.tex	Sat Apr 17 21:40:29 2010 +0200
     2.2 +++ b/doc-src/System/Thy/document/Basics.tex	Sat Apr 17 22:58:29 2010 +0200
     2.3 @@ -180,6 +180,17 @@
     2.4    some extend. In particular, site-wide defaults may be overridden by
     2.5    a private \verb|$ISABELLE_HOME_USER/etc/settings|.
     2.6    
     2.7 +  \item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is automatically
     2.8 +  set to a symbolic identifier for the underlying hardware and
     2.9 +  operating system.  The Isabelle platform identification always
    2.10 +  refers to the 32 bit variant, even this is a 64 bit machine.  Note
    2.11 +  that the ML or Java runtime may have a different idea, depending on
    2.12 +  which binaries are actually run.
    2.13 +
    2.14 +  \item[\indexdef{}{setting}{ISABELLE\_PLATFORM64}\hypertarget{setting.ISABELLE-PLATFORM64}{\hyperlink{setting.ISABELLE-PLATFORM64}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM{\isadigit{6}}{\isadigit{4}}}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is similar to
    2.15 +  \hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}} but refers to the proper 64 bit variant
    2.16 +  on a platform that supports this; the value is empty for 32 bit.
    2.17 +
    2.18    \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
    2.19    names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively.  Thus other tools and scripts
    2.20    need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
     3.1 --- a/lib/scripts/getsettings	Sat Apr 17 21:40:29 2010 +0200
     3.2 +++ b/lib/scripts/getsettings	Sat Apr 17 22:58:29 2010 +0200
     3.3 @@ -27,6 +27,9 @@
     3.4    "$ISABELLE_TOOL" "$@"
     3.5  }
     3.6  
     3.7 +#platform
     3.8 +. "$ISABELLE_HOME/lib/scripts/isabelle-platform"
     3.9 +
    3.10  #Isabelle distribution identifier -- filled in automatically!
    3.11  ISABELLE_IDENTIFIER=""
    3.12  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/lib/scripts/isabelle-platform	Sat Apr 17 22:58:29 2010 +0200
     4.3 @@ -0,0 +1,63 @@
     4.4 +#
     4.5 +# determine general hardware and operating system type for Isabelle
     4.6 +#
     4.7 +# NOTE: The ML system or JVM may have their own idea about the platform!
     4.8 +
     4.9 +ISABELLE_PLATFORM="unknown-platform"
    4.10 +ISABELLE_PLATFORM64=""
    4.11 +
    4.12 +case $(uname -s) in
    4.13 +  Linux)
    4.14 +    case $(uname -m) in
    4.15 +      i?86)
    4.16 +        ISABELLE_PLATFORM=x86-linux
    4.17 +        ;;
    4.18 +      x86_64)
    4.19 +        ISABELLE_PLATFORM=x86-linux
    4.20 +        ISABELLE_PLATFORM64=x86_64-linux
    4.21 +        ;;
    4.22 +    esac
    4.23 +    ;;
    4.24 +  Darwin)
    4.25 +    case $(uname -m) in
    4.26 +      i?86)
    4.27 +        ISABELLE_PLATFORM=x86-darwin
    4.28 +        if [ "$(sysctl -n hw.optional.x86_64 2>/dev/null)" = 1 ]; then
    4.29 +          ISABELLE_PLATFORM64=x86_64-darwin
    4.30 +        fi
    4.31 +        ;;
    4.32 +      Power* | power* | ppc)
    4.33 +        ISABELLE_PLATFORM=ppc-darwin
    4.34 +        ;;
    4.35 +    esac
    4.36 +    ;;
    4.37 +  CYGWIN_NT*)
    4.38 +    case $(uname -m) in
    4.39 +      i?86)
    4.40 +        ISABELLE_PLATFORM=x86-cygwin
    4.41 +        ;;
    4.42 +    esac
    4.43 +    ;;
    4.44 +  SunOS)
    4.45 +    case $(uname -r) in
    4.46 +      5.*)
    4.47 +        case $(uname -p) in
    4.48 +          sparc)
    4.49 +            ISABELLE_PLATFORM=sparc-solaris
    4.50 +            ;;
    4.51 +          i?86)
    4.52 +            ISABELLE_PLATFORM=x86-solaris
    4.53 +            ;;
    4.54 +        esac
    4.55 +        ;;
    4.56 +    esac
    4.57 +    ;;
    4.58 +  FreeBSD|NetBSD)
    4.59 +    case $(uname -m) in
    4.60 +      i?86)
    4.61 +        ISABELLE_PLATFORM=x86-bsd
    4.62 +        ;;
    4.63 +    esac
    4.64 +    ;;
    4.65 +esac
    4.66 +