Quelle ml_settings.scala Sprache: Scala

/*  Title:      Pure/ML/ml_settings.scala
    Author:     Makarius

ML system settings.
*/

package isabelle

object ML_Settings {
  def apply(options: Options,
    env: Isabelle_System.Settings = Isabelle_System.Settings()
  ): ML_Settings =
    new ML_Settings {
      override def polyml_home: Path = Path.variable("POLYML_HOME").expand_env(env)
      override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
      override def ml_platform: String = {
        proper_string(options.string("ML_platform")) orElse
        proper_string(Isabelle_System.getenv("ML_PLATFORM", env = env)) getOrElse {
          val platform_64 =
            Isabelle_Platform.make(env = env)
              .ISABELLE_PLATFORM(windows = true, apple = options.bool("ML_system_apple"))
          if (options.bool("ML_system_64")) platform_64
          else platform_64.replace("64", "64_32")
        }
      }
      override def ml_options: String =
        proper_string(Isabelle_System.getenv("ML_OPTIONS", env = env)) getOrElse
          Isabelle_System.getenv(if (ml_platform_is_64_32) "ML_OPTIONS32" else "ML_OPTIONS64")
    }

  def init(ml_platform: String = ""): ML_Settings =
    apply(Options.init(specs =
      if (ml_platform.isEmpty) Nil else List(Options.Spec("ML_platform", Some(ml_platform)))))
}

abstract class ML_Settings {
  def polyml_home: Path
  def ml_system: String
  def ml_platform: String
  def ml_options: String

  def ml_identifier: String = ml_system + "_" + ml_platform
  def ml_home: Path = polyml_home + Path.basic(ml_platform)

  def ml_platform_is_arm: Boolean = ml_platform.containsSlice("arm64")
  def ml_platform_is_windows: Boolean = ml_platform.containsSlice("windows")
  def ml_platform_is_64_32: Boolean = ml_platform.containsSlice("64_32")

  def ml_sources: Path = polyml_home + Path.basic("src")
  def ml_sources_root: (String, String) =
    ("ML_SOURCES_ROOT", if (ml_platform_is_arm) "src/ROOT0.ML" else "src/ROOT.ML")

  def polyml_exe: Path =
    ml_home + Path.basic("poly").exe_if(ml_platform_is_windows)

  override def toString: String = ml_identifier
}

quality100%

¤ Dauer der Verarbeitung: 0.13 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.