clarified modules;
authorwenzelm
Thu Oct 13 12:13:43 2016 +0200 (2016-10-13)
changeset 64188f88bae1922c4
parent 64187 450e06dabdd9
child 64189 dfb63036c4f6
clarified modules;
src/Pure/Admin/build_history.scala
src/Pure/Admin/other_isabelle.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Admin/build_history.scala	Thu Oct 13 12:04:48 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_history.scala	Thu Oct 13 12:13:43 2016 +0200
     1.3 @@ -20,137 +20,75 @@
     1.4    val META_INFO_MARKER = "\fmeta_info = "
     1.5  
     1.6  
     1.7 -
     1.8 -  /** other Isabelle environment **/
     1.9 -
    1.10 -  private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
    1.11 -  {
    1.12 -    other_isabelle =>
    1.13 -
    1.14 -
    1.15 -    /* static system */
    1.16 +  /* augment settings */
    1.17  
    1.18 -    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    1.19 -      Isabelle_System.bash(
    1.20 -        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
    1.21 -        env = null, cwd = isabelle_home.file, redirect = redirect,
    1.22 -        progress_stdout = progress.echo_if(echo, _),
    1.23 -        progress_stderr = progress.echo_if(echo, _))
    1.24 +  def augment_settings(
    1.25 +    other_isabelle: Other_Isabelle,
    1.26 +    threads: Int,
    1.27 +    arch_64: Boolean = false,
    1.28 +    heap: Int = default_heap,
    1.29 +    max_heap: Option[Int] = None,
    1.30 +    more_settings: List[String]): String =
    1.31 +  {
    1.32 +    val (ml_platform, ml_settings) =
    1.33 +    {
    1.34 +      val windows_32 = "x86-windows"
    1.35 +      val windows_64 = "x86_64-windows"
    1.36 +      val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
    1.37 +      val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
    1.38 +      val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
    1.39  
    1.40 -    def copy_dir(dir1: Path, dir2: Path): Unit =
    1.41 -      bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
    1.42 -
    1.43 -    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    1.44 -      bash("bin/isabelle " + cmdline, redirect, echo)
    1.45 +      val polyml_home =
    1.46 +        try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
    1.47 +        catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
    1.48  
    1.49 -    def resolve_components(echo: Boolean): Unit =
    1.50 -      other_isabelle("components -a", redirect = true, echo = echo).check
    1.51 +      def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
    1.52  
    1.53 -    val isabelle_home_user: Path =
    1.54 -      Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    1.55 +      def err(platform: String): Nothing =
    1.56 +        error("Platform " + platform + " unavailable on this machine")
    1.57  
    1.58 -    val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    1.59 -    val log_dir: Path = isabelle_home_user + Path.explode("log")
    1.60 -
    1.61 -
    1.62 -    /* reset settings */
    1.63 -
    1.64 -    def reset_settings(components_base: String, nonfree: Boolean)
    1.65 -    {
    1.66 -      if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
    1.67 -        error("Cannot proceed with existing user settings file: " + etc_settings)
    1.68 +      def check_dir(platform: String): Boolean =
    1.69 +        platform != "" && ml_home(platform).is_dir
    1.70  
    1.71 -      Isabelle_System.mkdirs(etc_settings.dir)
    1.72 -      File.write(etc_settings,
    1.73 -        "# generated by Isabelle " + Date.now() + "\n" +
    1.74 -        "#-*- shell-script -*- :mode=shellscript:\n")
    1.75 +      val ml_platform =
    1.76 +        if (Platform.is_windows && arch_64) {
    1.77 +          if (check_dir(windows_64)) windows_64 else err(windows_64)
    1.78 +        }
    1.79 +        else if (Platform.is_windows && !arch_64) {
    1.80 +          if (check_dir(windows_32)) windows_32
    1.81 +          else platform_32  // x86-cygwin
    1.82 +        }
    1.83 +        else {
    1.84 +          val (platform, platform_name) =
    1.85 +            if (arch_64) (platform_64, "x86_64-" + platform_family)
    1.86 +            else (platform_32, "x86-" + platform_family)
    1.87 +          if (check_dir(platform)) platform else err(platform_name)
    1.88 +        }
    1.89  
    1.90 -      val component_settings =
    1.91 -      {
    1.92 -        val components_base_path =
    1.93 -          if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
    1.94 -          else Path.explode(components_base).expand
    1.95 +      val ml_options =
    1.96 +        "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
    1.97 +        " --gcthreads " + threads +
    1.98 +        (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
    1.99  
   1.100 -        val catalogs =
   1.101 -          if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
   1.102 -
   1.103 -        catalogs.map(catalog =>
   1.104 -          "init_components " + File.bash_path(components_base_path) +
   1.105 -            " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
   1.106 -      }
   1.107 -      File.append(etc_settings, "\n" + terminate_lines(component_settings))
   1.108 +      (ml_platform,
   1.109 +        List(
   1.110 +          "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
   1.111 +          "ML_PLATFORM=" + quote(ml_platform),
   1.112 +          "ML_OPTIONS=" + quote(ml_options)))
   1.113      }
   1.114  
   1.115 -
   1.116 -    /* augment settings */
   1.117 -
   1.118 -    def augment_settings(
   1.119 -      threads: Int,
   1.120 -      arch_64: Boolean = false,
   1.121 -      heap: Int = default_heap,
   1.122 -      max_heap: Option[Int] = None,
   1.123 -      more_settings: List[String]): String =
   1.124 -    {
   1.125 -      val (ml_platform, ml_settings) =
   1.126 -      {
   1.127 -        val windows_32 = "x86-windows"
   1.128 -        val windows_64 = "x86_64-windows"
   1.129 -        val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
   1.130 -        val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
   1.131 -        val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
   1.132 -
   1.133 -        val polyml_home =
   1.134 -          try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
   1.135 -          catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
   1.136 -
   1.137 -        def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
   1.138 -
   1.139 -        def err(platform: String): Nothing =
   1.140 -          error("Platform " + platform + " unavailable on this machine")
   1.141 -
   1.142 -        def check_dir(platform: String): Boolean =
   1.143 -          platform != "" && ml_home(platform).is_dir
   1.144 +    val thread_settings =
   1.145 +      List(
   1.146 +        "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
   1.147 +        "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
   1.148  
   1.149 -        val ml_platform =
   1.150 -          if (Platform.is_windows && arch_64) {
   1.151 -            if (check_dir(windows_64)) windows_64 else err(windows_64)
   1.152 -          }
   1.153 -          else if (Platform.is_windows && !arch_64) {
   1.154 -            if (check_dir(windows_32)) windows_32
   1.155 -            else platform_32  // x86-cygwin
   1.156 -          }
   1.157 -          else {
   1.158 -            val (platform, platform_name) =
   1.159 -              if (arch_64) (platform_64, "x86_64-" + platform_family)
   1.160 -              else (platform_32, "x86-" + platform_family)
   1.161 -            if (check_dir(platform)) platform else err(platform_name)
   1.162 -          }
   1.163 -
   1.164 -        val ml_options =
   1.165 -          "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
   1.166 -          " --gcthreads " + threads +
   1.167 -          (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
   1.168 +    val settings =
   1.169 +      List(ml_settings, thread_settings) :::
   1.170 +        (if (more_settings.isEmpty) Nil else List(more_settings))
   1.171  
   1.172 -        (ml_platform,
   1.173 -          List(
   1.174 -            "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
   1.175 -            "ML_PLATFORM=" + quote(ml_platform),
   1.176 -            "ML_OPTIONS=" + quote(ml_options)))
   1.177 -      }
   1.178 +    File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
   1.179  
   1.180 -      val thread_settings =
   1.181 -        List(
   1.182 -          "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
   1.183 -          "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
   1.184 -
   1.185 -      val settings =
   1.186 -        List(ml_settings, thread_settings) :::
   1.187 -          (if (more_settings.isEmpty) Nil else List(more_settings))
   1.188 -
   1.189 -      File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
   1.190 -
   1.191 -      ml_platform
   1.192 -    }
   1.193 +    ml_platform
   1.194    }
   1.195  
   1.196  
   1.197 @@ -216,10 +154,10 @@
   1.198      {
   1.199        /* init settings */
   1.200  
   1.201 -      other_isabelle.reset_settings(components_base, nonfree)
   1.202 +      other_isabelle.init_settings(components_base, nonfree)
   1.203        other_isabelle.resolve_components(verbose)
   1.204        val ml_platform =
   1.205 -        other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
   1.206 +        augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
   1.207  
   1.208        val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
   1.209        val isabelle_output_log = isabelle_output + Path.explode("log")
   1.210 @@ -253,7 +191,7 @@
   1.211        /* output log */
   1.212  
   1.213        val log_path =
   1.214 -        other_isabelle.log_dir +
   1.215 +        other_isabelle.isabelle_home_user + Path.explode("log") +
   1.216            Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
   1.217  
   1.218        val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Admin/other_isabelle.scala	Thu Oct 13 12:13:43 2016 +0200
     2.3 @@ -0,0 +1,66 @@
     2.4 +/*  Title:      Pure/Admin/other_isabelle.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Manage other Isabelle distributions.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
    2.14 +{
    2.15 +  other_isabelle =>
    2.16 +
    2.17 +
    2.18 +  /* static system */
    2.19 +
    2.20 +  def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    2.21 +    Isabelle_System.bash(
    2.22 +      "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
    2.23 +      env = null, cwd = isabelle_home.file, redirect = redirect,
    2.24 +      progress_stdout = progress.echo_if(echo, _),
    2.25 +      progress_stderr = progress.echo_if(echo, _))
    2.26 +
    2.27 +  def copy_dir(dir1: Path, dir2: Path): Unit =
    2.28 +    bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
    2.29 +
    2.30 +  def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    2.31 +    bash("bin/isabelle " + cmdline, redirect, echo)
    2.32 +
    2.33 +  def resolve_components(echo: Boolean): Unit =
    2.34 +    other_isabelle("components -a", redirect = true, echo = echo).check
    2.35 +
    2.36 +  val isabelle_home_user: Path =
    2.37 +    Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    2.38 +
    2.39 +  val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    2.40 +
    2.41 +
    2.42 +  /* init settings */
    2.43 +
    2.44 +  def init_settings(components_base: String, nonfree: Boolean)
    2.45 +  {
    2.46 +    if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
    2.47 +      error("Cannot proceed with existing user settings file: " + etc_settings)
    2.48 +
    2.49 +    Isabelle_System.mkdirs(etc_settings.dir)
    2.50 +    File.write(etc_settings,
    2.51 +      "# generated by Isabelle " + Date.now() + "\n" +
    2.52 +      "#-*- shell-script -*- :mode=shellscript:\n")
    2.53 +
    2.54 +    val component_settings =
    2.55 +    {
    2.56 +      val components_base_path =
    2.57 +        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
    2.58 +        else Path.explode(components_base).expand
    2.59 +
    2.60 +      val catalogs =
    2.61 +        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
    2.62 +
    2.63 +      catalogs.map(catalog =>
    2.64 +        "init_components " + File.bash_path(components_base_path) +
    2.65 +          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
    2.66 +    }
    2.67 +    File.append(etc_settings, "\n" + terminate_lines(component_settings))
    2.68 +  }
    2.69 +}
     3.1 --- a/src/Pure/build-jars	Thu Oct 13 12:04:48 2016 +0200
     3.2 +++ b/src/Pure/build-jars	Thu Oct 13 12:13:43 2016 +0200
     3.3 @@ -17,6 +17,7 @@
     3.4    Admin/ci_api.scala
     3.5    Admin/ci_profile.scala
     3.6    Admin/isabelle_cronjob.scala
     3.7 +  Admin/other_isabelle.scala
     3.8    Admin/remote_dmg.scala
     3.9    Concurrent/consumer_thread.scala
    3.10    Concurrent/counter.scala