src/Pure/System/components.scala
author wenzelm
Thu, 06 Dec 2018 15:44:31 +0100
changeset 69413 52727566c1ba
parent 69410 c071fcec4323
child 69418 86ba90f88747
permissions -rw-r--r--
more explicit Components.Archive; support additional components, which also enforces clean bundling;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/components.scala
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     3
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     4
Isabelle system components.
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     5
*/
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     6
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     7
package isabelle
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     8
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
     9
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    10
import java.io.{File => JFile}
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    11
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    12
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    13
object Components
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    14
{
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    15
  /* archive name */
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    16
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    17
  object Archive
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    18
  {
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    19
    val suffix: String = ".tar.gz"
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    20
    def apply(name: String): String = name + suffix
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    21
    def unapply(archive: String): Option[String] = Library.try_unsuffix(suffix, archive)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    22
    def get_name(archive: String): String =
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    23
      unapply(archive) getOrElse
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    24
        error("Bad component archive name (expecting .tar.gz): " + quote(archive))
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    25
  }
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    26
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    27
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    28
  /* component collections */
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    29
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    30
  def admin(dir: Path): Path = dir + Path.explode("Admin/components")
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    31
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    32
  def contrib(dir: Path = Path.current, name: String = ""): Path =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    33
    dir + Path.explode("contrib") + Path.explode(name)
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    34
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    35
  def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    36
  {
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    37
    val name = Archive.get_name(archive.file_name)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    38
    progress.echo("Unpacking " + name)
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    39
    Isabelle_System.gnutar("-C " + File.bash_path(dir) + " -xzf " + File.bash_path(archive)).check
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    40
    name
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    41
  }
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    42
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    43
  def resolve(base_dir: Path, names: List[String],
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    44
    target_dir: Option[Path] = None,
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    45
    progress: Progress = No_Progress)
69398
0698ded5caf1 Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents: 69395
diff changeset
    46
  {
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    47
    Isabelle_System.mkdirs(base_dir)
69398
0698ded5caf1 Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents: 69395
diff changeset
    48
    for (name <- names) {
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    49
      val archive_name = Archive(name)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    50
      val archive = base_dir + Path.explode(archive_name)
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    51
      if (!archive.is_file) {
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    52
        val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    53
        progress.echo("Getting " + remote)
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    54
        Bytes.write(archive, Url.read_bytes(Url(remote)))
69398
0698ded5caf1 Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents: 69395
diff changeset
    55
      }
69413
52727566c1ba more explicit Components.Archive;
wenzelm
parents: 69410
diff changeset
    56
      unpack(target_dir getOrElse base_dir, archive, progress = progress)
69398
0698ded5caf1 Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents: 69395
diff changeset
    57
    }
0698ded5caf1 Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents: 69395
diff changeset
    58
  }
0698ded5caf1 Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents: 69395
diff changeset
    59
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69401
diff changeset
    60
  def purge(dir: Path, platform: Platform.Family.Value)
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    61
  {
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    62
    def purge_platforms(platforms: String*): Set[String] =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    63
      platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    64
    val purge_set =
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    65
      platform match {
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69401
diff changeset
    66
        case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69401
diff changeset
    67
        case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69401
diff changeset
    68
        case Platform.Family.windows => purge_platforms("linux", "darwin")
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    69
      }
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    70
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    71
    File.find_files(dir.file,
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    72
      (file: JFile) => file.isDirectory && purge_set(file.getName),
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    73
      include_dirs = true).foreach(Isabelle_System.rm_tree)
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    74
  }
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 69398
diff changeset
    75
69395
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    76
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    77
  /* component directory content */
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    78
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    79
  def settings(dir: Path): Path = dir + Path.explode("etc/settings")
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    80
  def components(dir: Path): Path = dir + Path.explode("etc/components")
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    81
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    82
  def check_dir(dir: Path): Boolean =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    83
    settings(dir).is_file || components(dir).is_file
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    84
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    85
  def read_components(dir: Path): List[String] =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    86
    split_lines(File.read(components(dir))).filter(_.nonEmpty)
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    87
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    88
  def write_components(dir: Path, lines: List[String]): Unit =
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    89
    File.write(components(dir), terminate_lines(lines))
d1c4a1dee9e7 more explicit support for Isabelle system components;
wenzelm
parents:
diff changeset
    90
}