Quelle other_isabelle.scala Sprache: Scala

/*  Title:      Pure/System/other_isabelle.scala
    Author:     Makarius

Manage other Isabelle distributions: support historic versions starting from
tag "build_history_base".
*/

package isabelle

object Other_Isabelle {
  def apply(
    root: Path,
    isabelle_identifier: String = "",
    ssh: SSH.System = SSH.Local,
    progress: Progress = new Progress
  ): Other_Isabelle = {
    val (isabelle_home, url_prefix) =
      ssh match {
        case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix)
        case _ =>
          if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
            error(
              "Cannot manage other Isabelle distribution: ISABELLE_SETTINGS_PRESENT " +
                "-- consider using SSH")
          }
          (root.canonical, "")
      }
    val isabelle_home_url = url_prefix + isabelle_home.implode
    new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress)
  }
}

final class Other_Isabelle private(
  val isabelle_home: Path,
  val isabelle_identifier: String,
  isabelle_home_url: String,
  val ssh: SSH.System,
  val progress: Progress
) {
  other_isabelle =>

  override def toString: String = isabelle_home_url
  def error_context: String = "\nThe error(s) above occurred for other Isabelle " + toString

  /* static system */

  def bash_context(script: String, cwd: Path = isabelle_home): String =
    Bash.context(script,
      user_home = ssh.user_home,
      isabelle_identifier = isabelle_identifier,
      cwd = cwd)

  def bash(
    script: String,
    cwd: Path = isabelle_home,
    input: String = "",
    redirect: Boolean = false,
    echo: Boolean = false,
    strict: Boolean = true
  ): Process_Result = {
    ssh.bash(bash_context(script, cwd = cwd),
      progress_stdout = progress.echo_if(echo, _),
      progress_stderr = progress.echo_if(echo, _),
      input = input,
      redirect = redirect,
      settings = false,
      strict = strict)
  }

  def getenv(name: String): String =
    ssh.execute(bash_context("bin/isabelle getenv -b " + Bash.string(name)),
      settings = false).check.out

  def getenv_strict(name: String): String =
    proper_string(getenv(name)) getOrElse
      error("Undefined Isabelle environment variable: " + quote(name) + error_context)

  val settings: Isabelle_System.Settings = (name: String) => getenv(name)

  def expand_path(path: Path): Path = path.expand_env(settings)
  def bash_path(path: Path): String = Bash.string(expand_path(path).implode)

  val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))

  def host_db: Path = isabelle_home_user + Path.explode("host.db")

  def etc: Path = isabelle_home_user + Path.explode("etc")
  def etc_settings: Path = etc + Path.explode("settings")
  def etc_preferences: Path = etc + Path.explode("preferences")

  def cleanup(): Unit =
    ssh.delete(host_db, etc_settings, etc_preferences, etc, isabelle_home_user)

  /* components */

  def init_components(
    components_base: String = Components.dynamic_components_base,
    catalogs: List[String] = Components.default_catalogs,
    components: List[String] = Nil
  ): List[String] = {
    val admin = Components.admin(Path.ISABELLE_HOME).implode

    catalogs.map(name =>
      "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) :::
    components.map(name =>
      "init_component " + quote(components_base) + "/" + name)
  }

  def resolve_components(
    echo: Boolean = false,
    clean_platforms: Option[List[Platform.Family]] = None,
    clean_archives: Boolean = false,
    component_repository: String = Components.static_component_repository
  ): Unit = {
    val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
    for (path <- missing) {
      Components.resolve(path.dir, path.file_name,
        clean_platforms = clean_platforms,
        clean_archives = clean_archives,
        component_repository = component_repository,
        ssh = ssh,
        progress = if (echo) progress else new Progress)
    }
  }

  def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = {
    if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes"))

    val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
    val dummy_stty_remote = expand_path(dummy_stty)
    if (!ssh.is_file(dummy_stty_remote)) {
      ssh.make_directory(dummy_stty_remote.dir)
      ssh.write_file(dummy_stty_remote, dummy_stty)
      ssh.set_executable(dummy_stty_remote)
    }
    try {
      bash(
        "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" +
        "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
        "bin/isabelle jedit -b", echo = echo).check
    }
    catch {
      case ERROR(msg) =>
        error("Failed to build Isabelle/Scala/Java modules:\n" + msg + error_context)
    }
  }

  /* settings */

  def clean_settings(): Boolean =
    if (!ssh.is_file(etc_settings)) true
    else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) {
      ssh.delete(etc_settings)
      true
    }
    else false

  def init_settings(settings: List[String]): Unit = {
    if (clean_settings()) {
      ssh.make_directory(etc_settings.dir)
      ssh.write(etc_settings,
        "# generated by Isabelle " + Date.now() + "\n" +
        "#-*- shell-script -*- :mode=shellscript:\n" +
        settings.mkString("\n", "\n", "\n"))
    }
    else error("Cannot proceed with existing user settings file: " + etc_settings + error_context)
  }

  def debug_settings(): List[String] = {
    val debug = System.getProperty("isabelle.debug", "") == "true"
    if (debug) {
      List("ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.debug=true\"")
    }
    else Nil
  }

  /* init */

  def init(
    other_settings: List[String] = init_components(),
    fresh: Boolean = false,
    echo: Boolean = false,
    clean_platforms: Option[List[Platform.Family]] = None,
    clean_archives: Boolean = false,
    component_repository: String = Components.static_component_repository
  ): Unit = {
    init_settings(other_settings)
    resolve_components(
      echo = echo,
      clean_platforms = clean_platforms,
      clean_archives = clean_archives,
      component_repository = component_repository)
    scala_build(fresh = fresh, echo = echo)
    Setup_Tool.init(other_isabelle)
  }

  /* ML system settings */

  val ml_settings: ML_Settings =
    new ML_Settings {
      override def polyml_home: Path =
        getenv("POLYML_HOME") match {
          case "" =>
            try { expand_path(Path.variable("ML_HOME")).dir }
            catch { case ERROR(msg) => error("Bad ML_HOME: " + msg + error_context) }
          case s => Path.explode(s)
        }

      override def ml_system: String = getenv_strict("ML_SYSTEM")

      override def ml_platform: String =
        if (ssh.is_file(isabelle_home + Path.explode("lib/Tools/console"))) {
          val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
          val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
          val result = bash("bin/isabelle console -r", input = input)
          result.out match {
            case Pattern(a) if result.ok && a.nonEmpty => a
            case _ =>
              error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
                if_proper(result.err, "\n" + result.err) + error_context)
          }
        }
        else getenv_strict("ML_PLATFORM")

      override def ml_options: String =
        proper_string(getenv("ML_OPTIONS")) getOrElse
          getenv(if (ml_platform_is_64_32) "ML_OPTIONS32" else "ML_OPTIONS64")
    }

  def user_output_dir: Path =
    isabelle_home_user + Path.basic("heaps") + Path.basic(ml_settings.ml_identifier)
}

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.