--- a/NEWS Fri Nov 05 22:03:57 2010 +0100
+++ b/NEWS Fri Nov 05 23:19:20 2010 +0100
@@ -6,6 +6,13 @@
*** General ***
+* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
+(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
+while the default heap location within that directory lacks that extra
+suffix. This isolates multiple Isabelle installations from each
+other, avoiding problems with old settings in new versions.
+INCOMPATIBILITY, need to copy/upgrade old user settings manually.
+
* Significantly improved Isabelle/Isar implementation manual.
* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
--- a/doc-src/System/Thy/Basics.thy Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/Basics.thy Fri Nov 05 23:19:20 2010 +0100
@@ -95,7 +95,8 @@
\item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
exists) is run in the same way as the site default settings. Note
that the variable @{setting ISABELLE_HOME_USER} has already been set
- before --- usually to @{verbatim "~/.isabelle"}.
+ before --- usually to something like @{verbatim
+ "$HOME/.isabelle/IsabelleXXXX"}.
Thus individual users may override the site-wide defaults. See also
file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
@@ -156,11 +157,12 @@
\item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
counterpart of @{setting ISABELLE_HOME}. The default value is
- @{verbatim "~/.isabelle"}, under rare circumstances this may be
- changed in the global setting file. Typically, the @{setting
- ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
- some extend. In particular, site-wide defaults may be overridden by
- a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
+ relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
+ this may be changed in the global setting file. Typically, the
+ @{setting ISABELLE_HOME_USER} directory mimics @{setting
+ ISABELLE_HOME} to some extend. In particular, site-wide defaults may
+ be overridden by a private @{verbatim
+ "$ISABELLE_HOME_USER/etc/settings"}.
\item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
set to a symbolic identifier for the underlying hardware and
--- a/doc-src/System/Thy/Presentation.thy Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/Presentation.thy Fri Nov 05 23:19:20 2010 +0100
@@ -88,10 +88,11 @@
\end{ttbox}
and then change into the @{"file" "~~/src/FOL"} directory and run
- @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
- make}~@{verbatim all}. The presentation output will appear in
- @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
- @{verbatim "~/.isabelle/browser_info/FOL"}. Note that option
+ @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle}
+ @{tool make}~@{verbatim all}. The presentation output will appear
+ in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
+ something like @{verbatim
+ "~/.isabelle/IsabelleXXXX/browser_info/FOL"}. Note that option
@{verbatim "-v true"} will make the internal runs of @{tool usedir}
more explicit about such details.
@@ -768,7 +769,7 @@
This enables users to inspect {\LaTeX} runs in further detail, e.g.\
like this:
\begin{ttbox}
- cd ~/.isabelle/browser_info/HOL/Test/document
+ cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
\end{ttbox}
*}
--- a/doc-src/System/Thy/document/Basics.tex Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Fri Nov 05 23:19:20 2010 +0100
@@ -114,7 +114,7 @@
\item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
exists) is run in the same way as the site default settings. Note
that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
- before --- usually to \verb|~/.isabelle|.
+ before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
Thus individual users may override the site-wide defaults. See also
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
@@ -175,10 +175,10 @@
\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
counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
- \verb|~/.isabelle|, under rare circumstances this may be
- 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
- some extend. In particular, site-wide defaults may be overridden by
- a private \verb|$ISABELLE_HOME_USER/etc/settings|.
+ relative to \verb|$HOME/.isabelle|, under rare circumstances
+ this may be 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 some extend. In particular, site-wide defaults may
+ be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
\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
set to a symbolic identifier for the underlying hardware and
--- a/doc-src/System/Thy/document/Presentation.tex Fri Nov 05 22:03:57 2010 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Fri Nov 05 23:19:20 2010 +0100
@@ -104,9 +104,10 @@
\end{ttbox}
and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
- \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
- \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
- \verb|~/.isabelle/browser_info/FOL|. Note that option
+ \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 \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
+ something like \verb|~/.isabelle/IsabelleXXXX/browser_info/FOL|. Note that option
\verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
more explicit about such details.
@@ -776,7 +777,7 @@
This enables users to inspect {\LaTeX} runs in further detail, e.g.\
like this:
\begin{ttbox}
- cd ~/.isabelle/browser_info/HOL/Test/document
+ cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
\end{ttbox}%
\end{isamarkuptext}%
--- a/etc/settings Fri Nov 05 22:03:57 2010 +0100
+++ b/etc/settings Fri Nov 05 23:19:20 2010 +0100
@@ -103,7 +103,7 @@
###
# The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER=~/.isabelle
+ISABELLE_HOME_USER="$HOME/.isabelle/$ISABELLE_IDENTIFIER"
# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
@@ -112,10 +112,10 @@
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
# Site settings check -- just to make it a little bit harder to copy this file verbatim!