src/Pure/Tools/build_history.scala

allow multiple threads configurations;

/*  Title:      Pure/Tools/build_history.scala
    Author:     Makarius

Build other history versions.
*/

package isabelle


import java.io.{File => JFile}
import java.util.Calendar


object Build_History
{
  /** other Isabelle environment **/

  private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
  {
    other_isabelle =>


    /* static system */

    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
      Isabelle_System.bash(
        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
        env = null, cwd = isabelle_home.file, redirect = redirect,
        progress_stdout = progress.echo_if(echo, _),
        progress_stderr = progress.echo_if(echo, _))

    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
      bash("bin/isabelle " + cmdline, redirect, echo)

    def resolve_components(echo: Boolean): Unit =
      other_isabelle("components -a", redirect = true, echo = echo).check

    val isabelle_home_user: Path =
      Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)

    val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")


    /* reset settings */

    def reset_settings(components_base: String, nonfree: Boolean)
    {
      if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
        error("Cannot proceed with existing user settings file: " + etc_settings)

      Isabelle_System.mkdirs(etc_settings.dir)
      File.write(etc_settings,
        "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
        "#-*- shell-script -*- :mode=shellscript:\n")

      val component_settings =
      {
        val components_base_path =
          if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
          else Path.explode(components_base).expand

        val catalogs =
          if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")

        catalogs.map(catalog =>
          "init_components " + File.bash_path(components_base_path) +
            " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
      }
      File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
    }


    /* augment settings */

    def augment_settings(
      threads: Int,
      arch_64: Boolean = false,
      heap: Int = default_heap,
      max_heap: Option[Int] = None,
      more_settings: List[String])
    {
      val ml_settings =
      {
        val windows_32 = "x86-windows"
        val windows_64 = "x86_64-windows"
        val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
        val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
        val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out

        val polyml_home =
          try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
          catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }

        def ml_home(platform: String): Path = polyml_home + Path.explode(platform)

        def err(platform: String): Nothing =
          error("Platform " + platform + " unavailable on this machine")

        def check_dir(platform: String): Boolean =
          platform != "" && ml_home(platform).is_dir

        val ml_platform =
          if (Platform.is_windows && arch_64) {
            if (check_dir(windows_64)) windows_64 else err(windows_64)
          }
          else if (Platform.is_windows && !arch_64) {
            if (check_dir(windows_32)) windows_32
            else platform_32  // x86-cygwin
          }
          else {
            val (platform, platform_name) =
              if (arch_64) (platform_64, "x86_64-" + platform_family)
              else (platform_32, "x86-" + platform_family)
            if (check_dir(platform)) platform else err(platform_name)
          }

        val ml_options =
          "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
          " --gcthreads " + threads +
          (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")

        List(
          "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
          "ML_PLATFORM=" + quote(ml_platform),
          "ML_OPTIONS=" + quote(ml_options))
      }

      val thread_settings =
        List(
          "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
          "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")

      val settings =
        List(ml_settings, thread_settings) :::
          (if (more_settings.isEmpty) Nil else List(more_settings))

      File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
    }
  }



  /** build_history **/

  private val default_rev = "tip"
  private val default_threads = 1
  private val default_heap = 1000
  private val default_isabelle_identifier = "build_history"

  def build_history(
    progress: Progress,
    hg: Mercurial.Repository,
    rev: String = default_rev,
    isabelle_identifier: String = default_isabelle_identifier,
    components_base: String = "",
    fresh: Boolean = false,
    nonfree: Boolean = false,
    threads_list: List[Int] = List(default_threads),
    arch_64: Boolean = false,
    heap: Int = default_heap,
    max_heap: Option[Int] = None,
    more_settings: List[String] = Nil,
    verbose: Boolean = false,
    build_args: List[String] = Nil): List[Process_Result] =
  {
    /* sanity checks */

    if (File.eq(Path.explode("~~").file, hg.root.file))
      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)

    for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)

    if (heap < 100) error("Bad heap value < 100: " + heap)

    if (max_heap.isDefined && max_heap.get < heap)
      error("Bad max_heap value < heap: " + max_heap.get)

    System.getenv("ISABELLE_SETTINGS_PRESENT") match {
      case null | "" =>
      case _ => error("Cannot run build_history within existing Isabelle settings environment")
    }


    /* init repository */

    hg.update(rev = rev, clean = true)
    progress.echo_if(verbose, hg.log(rev, options = "-l1"))

    val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)


    /* init settings and build */

    var first_build = true
    for (threads <- threads_list)
    yield {
      other_isabelle.reset_settings(components_base, nonfree)
      other_isabelle.resolve_components(verbose)
      other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)

      if (first_build) {
        first_build = false

        other_isabelle.resolve_components(verbose)
        other_isabelle.bash(
          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
            "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
          redirect = true, echo = verbose).check
      }

      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
      Isabelle_System.rm_tree(isabelle_output.file)
      other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = true)
    }
  }


  /* command line entry point */

  def main(args: Array[String])
  {
    Command_Line.tool0 {
      var components_base = ""
      var heap: Option[Int] = None
      var max_heap: Option[Int] = None
      var threads_list = List(default_threads)
      var isabelle_identifier = default_isabelle_identifier
      var more_settings: List[String] = Nil
      var fresh = false
      var arch_64 = false
      var nonfree = false
      var rev = default_rev
      var verbose = false

      val getopts = Getopts("""
Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]

  Options are:
    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
    -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
    -M THREADS   multithreading configurations (comma-separated list, default: """ + default_threads + """)
    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
    -U SIZE      maximal ML heap in MB (default: unbounded)
    -e TEXT      additional text for generated etc/settings
    -f           fresh build of Isabelle/Scala components (recommended)
    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
    -n           include nonfree components
    -r REV       update to revision (default: """ + default_rev + """)
    -v           verbose

  Build Isabelle sessions from the history of another REPOSITORY clone,
  passing ARGS directly to its isabelle build tool.
""",
        "C:" -> (arg => components_base = arg),
        "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
        "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
        "N:" -> (arg => isabelle_identifier = arg),
        "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
        "f" -> (_ => fresh = true),
        "m:" ->
          {
            case "32" | "x86" => arch_64 = false
            case "64" | "x86_64" => arch_64 = true
            case bad => error("Bad processor architecture: " + quote(bad))
          },
        "n" -> (_ => nonfree = true),
        "r:" -> (arg => rev = arg),
        "v" -> (_ => verbose = true))

      val more_args = getopts(args)
      val (root, build_args) =
        more_args match {
          case root :: build_args => (root, build_args)
          case _ => getopts.usage()
        }

      using(Mercurial.open_repository(Path.explode(root)))(hg =>
        {
          val progress = new Console_Progress(false)
          val results =
            build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
              components_base = components_base, fresh = fresh, nonfree = nonfree,
              threads_list = threads_list, arch_64 = arch_64,
              heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
              max_heap = max_heap, more_settings = more_settings, verbose = verbose,
              build_args = build_args)
          val rc = (0 /: results) { case (rc, res) => rc max res.rc }
          if (rc != 0) sys.exit(rc)
        })
    }
  }
}