src/Pure/Tools/build_history.scala

clarified sanity checks;

/*  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
{
  /* 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: Int = 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): Process_Result =
  {
    /* output */

    def output(msg: String) { progress.echo(msg) }
    def output_if(b: Boolean, msg: String) { if (b) output(msg) }


    /* sanity checks */

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

    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")
    }


    /* purge repository */

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


    /* invoke isabelle tools */

    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
      Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
        " " + script, cwd = hg.root.file, env = null, redirect = redirect,
        progress_stdout = output_if(echo, _), progress_stderr = output_if(echo, _))

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

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


    /* reset settings */

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

    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")


    /* initial settings */

    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))


    isabelle("components -a", redirect = true, echo = verbose).check


    /* augmented settings */

    val ml_settings =
    {
      val windows_32 = "x86-windows"
      val windows_64 = "x86_64-windows"
      val platform_32 = isabelle("getenv -b ISABELLE_PLATFORM32").check.out
      val platform_64 = isabelle("getenv -b ISABELLE_PLATFORM64").check.out
      val platform_family = isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out

      val polyml_home =
        try { Path.explode(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 + "\"")

    File.append(etc_settings, "\n" +
      cat_lines(List(ml_settings, thread_settings).map(Library.terminate_lines(_))))

    if (more_settings.nonEmpty)
      File.append(etc_settings, "\n" + Library.terminate_lines(more_settings))


    isabelle("components -a", redirect = true, echo = verbose).check


    /* build */

    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

    isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose)
  }


  /* 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 = 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   number of threads for Poly/ML RTS and Isabelle/ML (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 = Value.Int.parse(arg)),
        "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 res =
            build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
              components_base = components_base, fresh = fresh, nonfree = nonfree,
              threads = threads, 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)
          if (!res.ok) sys.exit(res.rc)
        })
    }
  }
}