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