src/Pure/System/mingw.scala
author wenzelm
Mon, 01 Mar 2021 22:22:12 +0100
changeset 73340 0ffcad1f6130
parent 72432 86f8fcdcff4a
child 75393 87ebf5a50283
permissions -rw-r--r--
tuned --- fewer warnings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/mingw.scala
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     3
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     4
Support for MSYS2/MinGW64 on Windows.
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     5
*/
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     6
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     7
package isabelle
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     8
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     9
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    10
object MinGW
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    11
{
72427
def95a34df8e clarified signature;
wenzelm
parents: 72425
diff changeset
    12
  def environment: List[String] =
def95a34df8e clarified signature;
wenzelm
parents: 72425
diff changeset
    13
    List("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site")
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    14
72427
def95a34df8e clarified signature;
wenzelm
parents: 72425
diff changeset
    15
  def environment_export: String =
def95a34df8e clarified signature;
wenzelm
parents: 72425
diff changeset
    16
    environment.map(a => "export " + Bash.string(a)).mkString("", "\n", "\n")
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    17
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    18
  val none: MinGW = new MinGW(None)
72431
b8b97c49e339 tuned signature;
wenzelm
parents: 72428
diff changeset
    19
  def apply(path: Path) = new MinGW(Some(path))
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    20
}
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    21
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    22
class MinGW private(val root: Option[Path])
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    23
{
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    24
  override def toString: String =
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    25
    root match {
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    26
      case None => "MinGW.none"
72431
b8b97c49e339 tuned signature;
wenzelm
parents: 72428
diff changeset
    27
      case Some(msys_root) => "MinGW(" + msys_root.toString + ")"
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    28
    }
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    29
72428
b7351ffe0dbc clarified signature: allow complex bash script;
wenzelm
parents: 72427
diff changeset
    30
  def bash_script(script: String): String =
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    31
    root match {
72428
b7351ffe0dbc clarified signature: allow complex bash script;
wenzelm
parents: 72427
diff changeset
    32
      case None => script
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    33
      case Some(msys_root) =>
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    34
        File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
72428
b7351ffe0dbc clarified signature: allow complex bash script;
wenzelm
parents: 72427
diff changeset
    35
          " -c " + Bash.string(MinGW.environment_export + script)
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    36
    }
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    37
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    38
  def get_root: Path =
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    39
    if (!Platform.is_windows) error("Windows platform required")
72425
d0937d55eb90 clarified errors;
wenzelm
parents: 72424
diff changeset
    40
    else if (root.isEmpty) error("Windows platform requires msys/mingw root specification")
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    41
    else root.get
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    42
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72432
diff changeset
    43
  def check: Unit =
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    44
  {
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    45
    if (Platform.is_windows) {
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    46
      get_root
72428
b7351ffe0dbc clarified signature: allow complex bash script;
wenzelm
parents: 72427
diff changeset
    47
      try { require(Isabelle_System.bash(bash_script("uname -s")).check.out.startsWith("MSYS")) }
72432
86f8fcdcff4a clarified message;
wenzelm
parents: 72431
diff changeset
    48
      catch { case ERROR(msg) => cat_error("Bad msys/mingw installation " + get_root, msg) }
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    49
    }
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    50
  }
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    51
}