moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
authorwenzelm
Fri Nov 05 23:19:20 2010 +0100 (2010-11-05)
changeset 40387e4c9e0dad473
parent 40386 bdce9a9ec0cd
child 40388 cb9fd7dd641c
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
NEWS
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Basics.tex
doc-src/System/Thy/document/Presentation.tex
etc/settings
     1.1 --- a/NEWS	Fri Nov 05 22:03:57 2010 +0100
     1.2 +++ b/NEWS	Fri Nov 05 23:19:20 2010 +0100
     1.3 @@ -6,6 +6,13 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
     1.8 +(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
     1.9 +while the default heap location within that directory lacks that extra
    1.10 +suffix.  This isolates multiple Isabelle installations from each
    1.11 +other, avoiding problems with old settings in new versions.
    1.12 +INCOMPATIBILITY, need to copy/upgrade old user settings manually.
    1.13 +
    1.14  * Significantly improved Isabelle/Isar implementation manual.
    1.15  
    1.16  * Explicit treatment of UTF8 sequences as Isabelle symbols, such that
     2.1 --- a/doc-src/System/Thy/Basics.thy	Fri Nov 05 22:03:57 2010 +0100
     2.2 +++ b/doc-src/System/Thy/Basics.thy	Fri Nov 05 23:19:20 2010 +0100
     2.3 @@ -95,7 +95,8 @@
     2.4    \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
     2.5    exists) is run in the same way as the site default settings. Note
     2.6    that the variable @{setting ISABELLE_HOME_USER} has already been set
     2.7 -  before --- usually to @{verbatim "~/.isabelle"}.
     2.8 +  before --- usually to something like @{verbatim
     2.9 +  "$HOME/.isabelle/IsabelleXXXX"}.
    2.10    
    2.11    Thus individual users may override the site-wide defaults.  See also
    2.12    file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
    2.13 @@ -156,11 +157,12 @@
    2.14    
    2.15    \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
    2.16    counterpart of @{setting ISABELLE_HOME}. The default value is
    2.17 -  @{verbatim "~/.isabelle"}, under rare circumstances this may be
    2.18 -  changed in the global setting file.  Typically, the @{setting
    2.19 -  ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
    2.20 -  some extend. In particular, site-wide defaults may be overridden by
    2.21 -  a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
    2.22 +  relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
    2.23 +  this may be changed in the global setting file.  Typically, the
    2.24 +  @{setting ISABELLE_HOME_USER} directory mimics @{setting
    2.25 +  ISABELLE_HOME} to some extend. In particular, site-wide defaults may
    2.26 +  be overridden by a private @{verbatim
    2.27 +  "$ISABELLE_HOME_USER/etc/settings"}.
    2.28    
    2.29    \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
    2.30    set to a symbolic identifier for the underlying hardware and
     3.1 --- a/doc-src/System/Thy/Presentation.thy	Fri Nov 05 22:03:57 2010 +0100
     3.2 +++ b/doc-src/System/Thy/Presentation.thy	Fri Nov 05 23:19:20 2010 +0100
     3.3 @@ -88,10 +88,11 @@
     3.4  \end{ttbox}
     3.5  
     3.6    and then change into the @{"file" "~~/src/FOL"} directory and run
     3.7 -  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
     3.8 -  make}~@{verbatim all}.  The presentation output will appear in
     3.9 -  @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    3.10 -  @{verbatim "~/.isabelle/browser_info/FOL"}.  Note that option
    3.11 +  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle}
    3.12 +  @{tool make}~@{verbatim all}.  The presentation output will appear
    3.13 +  in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    3.14 +  something like @{verbatim
    3.15 +  "~/.isabelle/IsabelleXXXX/browser_info/FOL"}.  Note that option
    3.16    @{verbatim "-v true"} will make the internal runs of @{tool usedir}
    3.17    more explicit about such details.
    3.18  
    3.19 @@ -768,7 +769,7 @@
    3.20    This enables users to inspect {\LaTeX} runs in further detail, e.g.\
    3.21    like this:
    3.22  \begin{ttbox}
    3.23 -  cd ~/.isabelle/browser_info/HOL/Test/document
    3.24 +  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
    3.25    isabelle latex -o pdf
    3.26  \end{ttbox}
    3.27  *}
     4.1 --- a/doc-src/System/Thy/document/Basics.tex	Fri Nov 05 22:03:57 2010 +0100
     4.2 +++ b/doc-src/System/Thy/document/Basics.tex	Fri Nov 05 23:19:20 2010 +0100
     4.3 @@ -114,7 +114,7 @@
     4.4    \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
     4.5    exists) is run in the same way as the site default settings. Note
     4.6    that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
     4.7 -  before --- usually to \verb|~/.isabelle|.
     4.8 +  before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
     4.9    
    4.10    Thus individual users may override the site-wide defaults.  See also
    4.11    file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}user{\isacharminus}settings{\isachardot}sample}}}} in the
    4.12 @@ -175,10 +175,10 @@
    4.13    
    4.14    \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}}}] is the user-specific
    4.15    counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
    4.16 -  \verb|~/.isabelle|, under rare circumstances this may be
    4.17 -  changed in the global setting file.  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to
    4.18 -  some extend. In particular, site-wide defaults may be overridden by
    4.19 -  a private \verb|$ISABELLE_HOME_USER/etc/settings|.
    4.20 +  relative to \verb|$HOME/.isabelle|, under rare circumstances
    4.21 +  this may be changed in the global setting file.  Typically, the
    4.22 +  \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to some extend. In particular, site-wide defaults may
    4.23 +  be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
    4.24    
    4.25    \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
    4.26    set to a symbolic identifier for the underlying hardware and
     5.1 --- a/doc-src/System/Thy/document/Presentation.tex	Fri Nov 05 22:03:57 2010 +0100
     5.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Fri Nov 05 23:19:20 2010 +0100
     5.3 @@ -104,9 +104,10 @@
     5.4  \end{ttbox}
     5.5  
     5.6    and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
     5.7 -  \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear in
     5.8 -  \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
     5.9 -  \verb|~/.isabelle/browser_info/FOL|.  Note that option
    5.10 +  \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
    5.11 +  \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear
    5.12 +  in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
    5.13 +  something like \verb|~/.isabelle/IsabelleXXXX/browser_info/FOL|.  Note that option
    5.14    \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
    5.15    more explicit about such details.
    5.16  
    5.17 @@ -776,7 +777,7 @@
    5.18    This enables users to inspect {\LaTeX} runs in further detail, e.g.\
    5.19    like this:
    5.20  \begin{ttbox}
    5.21 -  cd ~/.isabelle/browser_info/HOL/Test/document
    5.22 +  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
    5.23    isabelle latex -o pdf
    5.24  \end{ttbox}%
    5.25  \end{isamarkuptext}%
     6.1 --- a/etc/settings	Fri Nov 05 22:03:57 2010 +0100
     6.2 +++ b/etc/settings	Fri Nov 05 23:19:20 2010 +0100
     6.3 @@ -103,7 +103,7 @@
     6.4  ###
     6.5  
     6.6  # The place for user configuration, heap files, etc.
     6.7 -ISABELLE_HOME_USER=~/.isabelle
     6.8 +ISABELLE_HOME_USER="$HOME/.isabelle/$ISABELLE_IDENTIFIER"
     6.9  
    6.10  # Where to look for isabelle tools (multiple dirs separated by ':').
    6.11  ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
    6.12 @@ -112,10 +112,10 @@
    6.13  ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
    6.14  
    6.15  # Heap input locations. ML system identifier is included in lookup.
    6.16 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
    6.17 +ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
    6.18  
    6.19  # Heap output location. ML system identifier is appended automatically later on.
    6.20 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
    6.21 +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
    6.22  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    6.23  
    6.24  # Site settings check -- just to make it a little bit harder to copy this file verbatim!