clarified store directories;
authorwenzelm
Sat May 19 15:45:45 2018 +0200 (14 months ago)
changeset 68219c0341c0080e2
parent 68218 92050155593e
child 68220 8fc4e3d1df86
clarified store directories;
discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;
NEWS
etc/settings
lib/scripts/getsettings
src/Doc/System/Environment.thy
src/Doc/System/Misc.thy
src/Doc/System/Server.thy
src/Doc/System/Sessions.thy
src/Pure/Admin/build_history.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Sat May 19 14:52:01 2018 +0200
     1.2 +++ b/NEWS	Sat May 19 15:45:45 2018 +0200
     1.3 @@ -351,6 +351,12 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
     1.8 +heap images and session databases are always stored in
     1.9 +$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
    1.10 +$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
    1.11 +"isabelle jedit -s" or "isabelle build -s").
    1.12 +
    1.13  * The command-line tool retrieves theory exports from the session build
    1.14  database.
    1.15  
     2.1 --- a/etc/settings	Sat May 19 14:52:01 2018 +0200
     2.2 +++ b/etc/settings	Sat May 19 15:45:45 2018 +0200
     2.3 @@ -77,11 +77,7 @@
     2.4  # Location for temporary files (should be on a local file system).
     2.5  ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
     2.6  
     2.7 -# Heap input locations. ML system identifier is included in lookup.
     2.8 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
     2.9 -
    2.10 -# Heap output location. ML system identifier is appended automatically later on.
    2.11 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
    2.12 +# HTML browser info.
    2.13  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    2.14  
    2.15  # Site settings check -- just to make it a little bit harder to copy this file verbatim!
     3.1 --- a/lib/scripts/getsettings	Sat May 19 14:52:01 2018 +0200
     3.2 +++ b/lib/scripts/getsettings	Sat May 19 15:45:45 2018 +0200
     3.3 @@ -99,8 +99,6 @@
     3.4    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
     3.5  fi
     3.6  
     3.7 -ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
     3.8 -
     3.9  #enforce JAVA_HOME
    3.10  if [ -d "$ISABELLE_JDK_HOME/jre" ]
    3.11  then
     4.1 --- a/src/Doc/System/Environment.thy	Sat May 19 14:52:01 2018 +0200
     4.2 +++ b/src/Doc/System/Environment.thy	Sat May 19 15:45:45 2018 +0200
     4.3 @@ -73,14 +73,9 @@
     4.4    minimum.
     4.5  
     4.6    \<^medskip>
     4.7 -  A few variables are somewhat special:
     4.8 -
     4.9 -    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
    4.10 -    name of the @{executable isabelle} executables.
    4.11 -
    4.12 -    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
    4.13 -    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
    4.14 -    @{setting ML_IDENTIFIER}) appended automatically to its value.
    4.15 +  A few variables are somewhat special, e.g. @{setting_def ISABELLE_TOOL} is
    4.16 +  set automatically to the absolute path name of the @{executable isabelle}
    4.17 +  executables.
    4.18  
    4.19    \<^medskip>
    4.20    Note that the settings environment may be inspected with the @{tool getenv}
    4.21 @@ -180,15 +175,6 @@
    4.22    always the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>,
    4.23    \<^verbatim>\<open>x86_64-windows\<close>.
    4.24  
    4.25 -  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
    4.26 -  colons) where Isabelle logic images may reside. When looking up heaps files,
    4.27 -  the value of @{setting ML_IDENTIFIER} is appended to each component
    4.28 -  internally.
    4.29 -
    4.30 -  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
    4.31 -  should be stored by default. The ML system and Isabelle version identifier
    4.32 -  is appended here, too.
    4.33 -
    4.34    \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
    4.35    browser information is stored as HTML and PDF (see also \secref{sec:info}).
    4.36    The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
     5.1 --- a/src/Doc/System/Misc.thy	Sat May 19 14:52:01 2018 +0200
     5.2 +++ b/src/Doc/System/Misc.thy	Sat May 19 15:45:45 2018 +0200
     5.3 @@ -145,7 +145,7 @@
     5.4    \<^medskip>
     5.5    Get the value only of the same settings variable, which is particularly
     5.6    useful in shell scripts:
     5.7 -  @{verbatim [display] \<open>isabelle getenv -b ISABELLE_OUTPUT\<close>}
     5.8 +  @{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>}
     5.9  \<close>
    5.10  
    5.11  
     6.1 --- a/src/Doc/System/Server.thy	Sat May 19 14:52:01 2018 +0200
     6.2 +++ b/src/Doc/System/Server.thy	Sat May 19 15:45:45 2018 +0200
     6.3 @@ -709,8 +709,7 @@
     6.4    \<^medskip>
     6.5    The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
     6.6    log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
     6.7 -  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
     6.8 -  ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
     6.9 +  @{path "$ISABELLE_HOME_USER/heaps"}. See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
    6.10  
    6.11    \<^medskip>
    6.12    The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
     7.1 --- a/src/Doc/System/Sessions.thy	Sat May 19 14:52:01 2018 +0200
     7.2 +++ b/src/Doc/System/Sessions.thy	Sat May 19 15:45:45 2018 +0200
     7.3 @@ -391,8 +391,7 @@
     7.4    \<^medskip>
     7.5    Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
     7.6    and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
     7.7 -  default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting
     7.8 -  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
     7.9 +  default location @{path "$ISABELLE_HOME_USER/heaps"}.
    7.10  
    7.11    \<^medskip>
    7.12    Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
     8.1 --- a/src/Pure/Admin/build_history.scala	Sat May 19 14:52:01 2018 +0200
     8.2 +++ b/src/Pure/Admin/build_history.scala	Sat May 19 15:45:45 2018 +0200
     8.3 @@ -190,7 +190,9 @@
     8.4        val ml_platform =
     8.5          augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
     8.6  
     8.7 -      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
     8.8 +      val isabelle_output =
     8.9 +        other_isabelle.isabelle_home_user + Path.explode("heaps") +
    8.10 +          Path.explode(other_isabelle("getenv -b ML_IDENTIFIER").check.out)
    8.11        val isabelle_output_log = isabelle_output + Path.explode("log")
    8.12        val isabelle_base_log = isabelle_output + Path.explode("../base_log")
    8.13  
     9.1 --- a/src/Pure/Thy/sessions.scala	Sat May 19 14:52:01 2018 +0200
     9.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 19 15:45:45 2018 +0200
     9.3 @@ -966,6 +966,9 @@
     9.4  
     9.5    class Store private[Sessions](val options: Options, val system_mode: Boolean)
     9.6    {
     9.7 +    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
     9.8 +
     9.9 +
    9.10      /* file names */
    9.11  
    9.12      def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
    9.13 @@ -973,19 +976,26 @@
    9.14      def log_gz(name: String): Path = log(name).ext("gz")
    9.15  
    9.16  
    9.17 -    /* output */
    9.18 +    /* directories */
    9.19 +
    9.20 +    def system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
    9.21 +    def user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
    9.22 +
    9.23 +    def output_dir: Path =
    9.24 +      if (system_mode) system_output_dir else user_output_dir
    9.25 +
    9.26 +    def input_dirs: List[Path] =
    9.27 +      if (system_mode) List(system_output_dir)
    9.28 +      else List(user_output_dir, system_output_dir)
    9.29  
    9.30      val browser_info: Path =
    9.31        if (system_mode) Path.explode("~~/browser_info")
    9.32        else Path.explode("$ISABELLE_BROWSER_INFO")
    9.33  
    9.34 -    val output_dir: Path =
    9.35 -      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
    9.36 -      else Path.explode("$ISABELLE_OUTPUT")
    9.37  
    9.38 -    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
    9.39 +    /* output */
    9.40  
    9.41 -    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    9.42 +    def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    9.43  
    9.44      def output_heap(name: String): Path = output_dir + Path.basic(name)
    9.45      def output_log(name: String): Path = output_dir + log(name)
    9.46 @@ -997,13 +1007,6 @@
    9.47  
    9.48      /* input */
    9.49  
    9.50 -    private val input_dirs =
    9.51 -      if (system_mode) List(output_dir)
    9.52 -      else {
    9.53 -        val ml_ident = Path.explode("$ML_IDENTIFIER").expand
    9.54 -        output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
    9.55 -      }
    9.56 -
    9.57      def find_heap(name: String): Option[Path] =
    9.58        input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    9.59  
    10.1 --- a/src/Pure/Tools/build.scala	Sat May 19 14:52:01 2018 +0200
    10.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 15:45:45 2018 +0200
    10.3 @@ -465,7 +465,7 @@
    10.4  
    10.5      val queue = Queue(progress, deps.sessions_structure, store)
    10.6  
    10.7 -    store.prepare_output()
    10.8 +    store.prepare_output_dir()
    10.9  
   10.10      // cleanup
   10.11      def cleanup(name: String, echo: Boolean = false)