# HG changeset patch # User wenzelm # Date 1228046300 -3600 # Node ID f993cbffc42a285cbe56d2cb9b84be94e055b4fc # Parent 86ed1c86e0efbd63b7a83750680f68b94f59092b default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle; diff -r 86ed1c86e0ef -r f993cbffc42a NEWS --- a/NEWS Sun Nov 30 12:25:54 2008 +0100 +++ b/NEWS Sun Nov 30 12:58:20 2008 +0100 @@ -31,6 +31,16 @@ purge installed copies of Isabelle executables and re-run "isabelle install -p ...", or use symlinks. +* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the +old ~/isabelle, which was slightly non-standard and apt cause +surprises on case-insensitive file-systems. + +INCOMPATIBILITY, need to move existing ~/isabelle/etc, +~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special +care is required when using older releases of Isabelle. Note that +ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any +Isabelle distribution. + * The Isabelle System Manual (system) has been updated, with formally checked references as hyperlinks. diff -r 86ed1c86e0ef -r f993cbffc42a doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Sun Nov 30 12:25:54 2008 +0100 +++ b/doc-src/System/Thy/Basics.thy Sun Nov 30 12:58:20 2008 +0100 @@ -100,7 +100,7 @@ \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 @{verbatim "~/.isabelle"}. Thus individual users may override the site-wide defaults. See also file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the @@ -161,7 +161,7 @@ \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 + @{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 diff -r 86ed1c86e0ef -r f993cbffc42a doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Sun Nov 30 12:25:54 2008 +0100 +++ b/doc-src/System/Thy/Presentation.thy Sun Nov 30 12:58:20 2008 +0100 @@ -93,7 +93,7 @@ @{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/browser_info/FOL"}. Note that option @{verbatim "-v true"} will make the internal runs of @{tool usedir} more explicit about such details. @@ -756,7 +756,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/browser_info/HOL/Test/document isabelle latex -o pdf \end{ttbox} *} diff -r 86ed1c86e0ef -r f993cbffc42a doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Sun Nov 30 12:25:54 2008 +0100 +++ b/doc-src/System/Thy/document/Basics.tex Sun Nov 30 12:58:20 2008 +0100 @@ -117,7 +117,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 \verb|~/.isabelle|. 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 @@ -178,7 +178,7 @@ \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 + \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|. diff -r 86ed1c86e0ef -r f993cbffc42a doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Sun Nov 30 12:25:54 2008 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Sun Nov 30 12:58:20 2008 +0100 @@ -108,7 +108,7 @@ 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/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. @@ -764,7 +764,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/browser_info/HOL/Test/document isabelle latex -o pdf \end{ttbox}% \end{isamarkuptext}% diff -r 86ed1c86e0ef -r f993cbffc42a doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Sun Nov 30 12:25:54 2008 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Sun Nov 30 12:58:20 2008 +0100 @@ -344,7 +344,7 @@ session is derived from a single parent, usually an object-logic image like \texttt{HOL}. This results in an overall tree structure, which is reflected by the output location in the file system - (usually rooted at \verb,~/isabelle/browser_info,). + (usually rooted at \verb,~/.isabelle/browser_info,). \medskip The easiest way to manage Isabelle sessions is via \texttt{isabelle mkdir} (generates an initial session source setup) diff -r 86ed1c86e0ef -r f993cbffc42a etc/settings --- a/etc/settings Sun Nov 30 12:25:54 2008 +0100 +++ b/etc/settings Sun Nov 30 12:58:20 2008 +0100 @@ -128,7 +128,7 @@ ### # The place for user configuration, heap files, etc. -ISABELLE_HOME_USER=~/isabelle +ISABELLE_HOME_USER=~/.isabelle # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" diff -r 86ed1c86e0ef -r f993cbffc42a etc/user-settings.sample --- a/etc/user-settings.sample Sun Nov 30 12:25:54 2008 +0100 +++ b/etc/user-settings.sample Sun Nov 30 12:58:20 2008 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- # $Id$ # -# Isabelle user settings sample -- for use in ~/isabelle/etc/settings +# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings ISABELLE_USEDIR_OPTIONS="-i true -d pdf" HOL_USEDIR_OPTIONS="-p 1"