author | wenzelm |
Sat, 13 Aug 2022 15:41:12 +0200 | |
changeset 75844 | 7d27944d7141 |
parent 75394 | 42267c650205 |
child 76122 | b8f26c20d3b1 |
permissions | -rw-r--r-- |
73815 | 1 |
/* Title: Pure/System/components.scala |
69395 | 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 |
|
75393 | 13 |
object Components { |
69413 | 14 |
/* archive name */ |
15 |
||
75393 | 16 |
object Archive { |
69413 | 17 |
val suffix: String = ".tar.gz" |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
18 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
19 |
def apply(name: String): String = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
20 |
if (name == "") error("Bad component name: " + quote(name)) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
21 |
else name + suffix |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
22 |
|
75393 | 23 |
def unapply(archive: String): Option[String] = { |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
24 |
for { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
25 |
name0 <- Library.try_unsuffix(suffix, archive) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
26 |
name <- proper_string(name0) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
27 |
} yield name |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
28 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
29 |
|
69413 | 30 |
def get_name(archive: String): String = |
31 |
unapply(archive) getOrElse |
|
32 |
error("Bad component archive name (expecting .tar.gz): " + quote(archive)) |
|
33 |
} |
|
34 |
||
35 |
||
69395 | 36 |
/* component collections */ |
37 |
||
73240
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
73173
diff
changeset
|
38 |
def default_component_repository: String = |
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
73173
diff
changeset
|
39 |
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") |
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
73173
diff
changeset
|
40 |
|
71601 | 41 |
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") |
69434 | 42 |
|
69395 | 43 |
def admin(dir: Path): Path = dir + Path.explode("Admin/components") |
44 |
||
45 |
def contrib(dir: Path = Path.current, name: String = ""): Path = |
|
46 |
dir + Path.explode("contrib") + Path.explode(name) |
|
47 |
||
75393 | 48 |
def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { |
69413 | 49 |
val name = Archive.get_name(archive.file_name) |
50 |
progress.echo("Unpacking " + name) |
|
69425 | 51 |
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check |
69413 | 52 |
name |
53 |
} |
|
54 |
||
69401
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
55 |
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
|
56 |
target_dir: Option[Path] = None, |
70102 | 57 |
copy_dir: Option[Path] = None, |
75393 | 58 |
progress: Progress = new Progress |
59 |
): Unit = { |
|
72375 | 60 |
Isabelle_System.make_directory(base_dir) |
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
61 |
for (name <- names) { |
69413 | 62 |
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
|
63 |
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
|
64 |
if (!archive.is_file) { |
73240
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
73173
diff
changeset
|
65 |
val remote = Components.default_component_repository + "/" + archive_name |
73566 | 66 |
Isabelle_System.download_file(remote, archive, progress = progress) |
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
67 |
} |
70102 | 68 |
for (dir <- copy_dir) { |
72375 | 69 |
Isabelle_System.make_directory(dir) |
73317 | 70 |
Isabelle_System.copy_file(archive, dir) |
70102 | 71 |
} |
69413 | 72 |
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
|
73 |
} |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
74 |
} |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
75 |
|
73637 | 76 |
private val platforms_family: Map[Platform.Family.Value, Set[String]] = |
77 |
Map( |
|
78 |
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), |
|
79 |
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), |
|
80 |
Platform.Family.macos -> |
|
81 |
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), |
|
82 |
Platform.Family.windows -> |
|
83 |
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) |
|
84 |
||
85 |
private val platforms_all: Set[String] = |
|
86 |
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) |
|
87 |
||
75393 | 88 |
def purge(dir: Path, platform: Platform.Family.Value): Unit = { |
73637 | 89 |
val purge_set = platforms_all -- platforms_family(platform) |
69401
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
90 |
|
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
91 |
File.find_files(dir.file, |
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
92 |
(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
|
93 |
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
|
94 |
} |
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
95 |
|
69395 | 96 |
|
73815 | 97 |
/* component directories */ |
98 |
||
99 |
def directories(): List[Path] = |
|
100 |
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) |
|
101 |
||
102 |
||
69395 | 103 |
/* component directory content */ |
104 |
||
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
105 |
def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
106 |
def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") |
69395 | 107 |
|
108 |
def check_dir(dir: Path): Boolean = |
|
109 |
settings(dir).is_file || components(dir).is_file |
|
110 |
||
111 |
def read_components(dir: Path): List[String] = |
|
112 |
split_lines(File.read(components(dir))).filter(_.nonEmpty) |
|
113 |
||
114 |
def write_components(dir: Path, lines: List[String]): Unit = |
|
115 |
File.write(components(dir), terminate_lines(lines)) |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
116 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
117 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
118 |
/* component repository content */ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
119 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
120 |
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
121 |
|
75393 | 122 |
sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) { |
75350
93943e7e38a4
prefer Isabelle shasum over the old command-line tool with its extra marker character;
wenzelm
parents:
75349
diff
changeset
|
123 |
override def toString: String = digest.shasum(name) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
124 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
125 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
126 |
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
127 |
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
128 |
Word.explode(line) match { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
129 |
case Nil => None |
75349 | 130 |
case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name)) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
131 |
case _ => error("Bad components.sha1 entry: " + quote(line)) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
132 |
}) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
133 |
|
71601 | 134 |
def write_components_sha1(entries: List[SHA1_Digest]): Unit = |
75349 | 135 |
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n")) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
136 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
137 |
|
73172 | 138 |
/** manage user components **/ |
139 |
||
75349 | 140 |
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") |
73172 | 141 |
|
142 |
def read_components(): List[String] = |
|
143 |
if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) |
|
144 |
else Nil |
|
145 |
||
75393 | 146 |
def write_components(lines: List[String]): Unit = { |
73172 | 147 |
Isabelle_System.make_directory(components_path.dir) |
148 |
File.write(components_path, Library.terminate_lines(lines)) |
|
149 |
} |
|
150 |
||
75393 | 151 |
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { |
73172 | 152 |
val path = path0.expand.absolute |
73814
c8b4a4f69068
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);
wenzelm
parents:
73813
diff
changeset
|
153 |
if (!check_dir(path) && !Sessions.is_session_dir(path)) error("Bad component directory: " + path) |
73172 | 154 |
|
155 |
val lines1 = read_components() |
|
156 |
val lines2 = |
|
157 |
lines1.filter(line => |
|
158 |
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) |
|
159 |
val lines3 = if (add) lines2 ::: List(path.implode) else lines2 |
|
160 |
||
161 |
if (lines1 != lines3) write_components(lines3) |
|
162 |
||
163 |
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" |
|
164 |
progress.echo(prefix + " component " + path) |
|
165 |
} |
|
166 |
||
167 |
||
168 |
/* main entry point */ |
|
169 |
||
75393 | 170 |
def main(args: Array[String]): Unit = { |
73172 | 171 |
Command_Line.tool { |
172 |
for (arg <- args) { |
|
173 |
val add = |
|
174 |
if (arg.startsWith("+")) true |
|
175 |
else if (arg.startsWith("-")) false |
|
176 |
else error("Bad argument: " + quote(arg)) |
|
177 |
val path = Path.explode(arg.substring(1)) |
|
178 |
update_components(add, path, progress = new Console_Progress) |
|
179 |
} |
|
180 |
} |
|
181 |
} |
|
182 |
||
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
183 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
184 |
/** build and publish components **/ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
185 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
186 |
def build_components( |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
187 |
options: Options, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
188 |
components: List[Path], |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
189 |
progress: Progress = new Progress, |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
190 |
publish: Boolean = false, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
191 |
force: Boolean = false, |
75393 | 192 |
update_components_sha1: Boolean = false |
193 |
): Unit = { |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
194 |
val archives: List[Path] = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
195 |
for (path <- components) yield { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
196 |
path.file_name match { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
197 |
case Archive(_) => path |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
198 |
case name => |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
199 |
if (!path.is_dir) error("Bad component directory: " + path) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
200 |
else if (!check_dir(path)) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
201 |
error("Malformed component directory: " + path + |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
202 |
"\n (requires " + settings() + " or " + Components.components() + ")") |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
203 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
204 |
else { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
205 |
val component_path = path.expand |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
206 |
val archive_dir = component_path.dir |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
207 |
val archive_name = Archive(name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
208 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
209 |
val archive = archive_dir + Path.explode(archive_name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
210 |
if (archive.is_file && !force) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
211 |
error("Component archive already exists: " + archive) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
212 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
213 |
|
69439 | 214 |
progress.echo("Packaging " + archive_name) |
69430 | 215 |
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
216 |
dir = archive_dir).check |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
217 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
218 |
archive |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
219 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
220 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
221 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
222 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
223 |
if ((publish && archives.nonEmpty) || update_components_sha1) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
224 |
options.string("isabelle_components_server") match { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
225 |
case SSH.Target(user, host) => |
75394 | 226 |
using(SSH.open_session(options, host = host, user = user)) { ssh => |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
227 |
val components_dir = Path.explode(options.string("isabelle_components_dir")) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
228 |
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
229 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
230 |
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
231 |
error("Bad remote directory: " + dir) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
232 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
233 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
234 |
if (publish) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
235 |
for (archive <- archives) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
236 |
val archive_name = archive.file_name |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
237 |
val name = Archive.get_name(archive_name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
238 |
val remote_component = components_dir + archive.base |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
239 |
val remote_contrib = contrib_dir + Path.explode(name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
240 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
241 |
// component archive |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
242 |
if (ssh.is_file(remote_component) && !force) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
243 |
error("Remote component archive already exists: " + remote_component) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
244 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
245 |
progress.echo("Uploading " + archive_name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
246 |
ssh.write_file(remote_component, archive) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
247 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
248 |
// contrib directory |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
249 |
val is_standard_component = |
75394 | 250 |
Isabelle_System.with_tmp_dir("component") { tmp_dir => |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
251 |
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
252 |
check_dir(tmp_dir + Path.explode(name)) |
75394 | 253 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
254 |
if (is_standard_component) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
255 |
if (ssh.is_dir(remote_contrib)) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
256 |
if (force) ssh.rm_tree(remote_contrib) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
257 |
else error("Remote component directory already exists: " + remote_contrib) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
258 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
259 |
progress.echo("Unpacking remote " + archive_name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
260 |
ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
261 |
ssh.bash_path(remote_component)).check |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
262 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
263 |
else { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
264 |
progress.echo_warning("No unpacking of non-standard component: " + archive_name) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
265 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
266 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
267 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
268 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
269 |
// remote SHA1 digests |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
270 |
if (update_components_sha1) { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
271 |
val lines = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
272 |
for { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
273 |
entry <- ssh.read_dir(components_dir) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
274 |
if entry.is_file && entry.name.endsWith(Archive.suffix) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
275 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
276 |
yield { |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
277 |
progress.echo("Digesting remote " + entry.name) |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73240
diff
changeset
|
278 |
ssh.execute("cd " + ssh.bash_path(components_dir) + |
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73240
diff
changeset
|
279 |
"; sha1sum " + Bash.string(entry.name)).check.out |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
280 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
281 |
write_components_sha1(read_components_sha1(lines)) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
282 |
} |
75394 | 283 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
284 |
case s => error("Bad isabelle_components_server: " + quote(s)) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
285 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
286 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
287 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
288 |
// local SHA1 digests |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
289 |
{ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
290 |
val new_entries = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
291 |
for (archive <- archives) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
292 |
yield { |
75349 | 293 |
val name = archive.file_name |
294 |
progress.echo("Digesting local " + name) |
|
295 |
SHA1_Digest(SHA1.digest(archive), name) |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
296 |
} |
75349 | 297 |
val new_names = new_entries.map(_.name).toSet |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
298 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
299 |
write_components_sha1( |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
300 |
new_entries ::: |
75349 | 301 |
read_components_sha1().filterNot(entry => new_names.contains(entry.name))) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
302 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
303 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
304 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
305 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
306 |
/* Isabelle tool wrapper */ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
307 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
308 |
private val relevant_options = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
309 |
List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
310 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
311 |
val isabelle_tool = |
72763 | 312 |
Isabelle_Tool("build_components", "build and publish Isabelle components", |
75394 | 313 |
Scala_Project.here, |
314 |
{ args => |
|
315 |
var publish = false |
|
316 |
var update_components_sha1 = false |
|
317 |
var force = false |
|
318 |
var options = Options.init() |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
319 |
|
75394 | 320 |
def show_options: String = |
75844
7d27944d7141
clarified signature: avoid public representation;
wenzelm
parents:
75394
diff
changeset
|
321 |
cat_lines(relevant_options.flatMap(options.get).map(_.print)) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
322 |
|
75394 | 323 |
val getopts = Getopts(""" |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
324 |
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
325 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
326 |
Options are: |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
327 |
-P publish on SSH server (see options below) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
328 |
-f force: overwrite existing component archives and directories |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
329 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
330 |
-u update all SHA1 keys in Isabelle repository Admin/components |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
331 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
332 |
Build and publish Isabelle components as .tar.gz archives on SSH server, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
333 |
depending on system options: |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
334 |
|
73736 | 335 |
""" + Library.indent_lines(2, show_options) + "\n", |
75394 | 336 |
"P" -> (_ => publish = true), |
337 |
"f" -> (_ => force = true), |
|
338 |
"o:" -> (arg => options = options + arg), |
|
339 |
"u" -> (_ => update_components_sha1 = true)) |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
340 |
|
75394 | 341 |
val more_args = getopts(args) |
342 |
if (more_args.isEmpty && !update_components_sha1) getopts.usage() |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
343 |
|
75394 | 344 |
val progress = new Console_Progress |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
345 |
|
75394 | 346 |
build_components(options, more_args.map(Path.explode), progress = progress, |
347 |
publish = publish, force = force, update_components_sha1 = update_components_sha1) |
|
348 |
}) |
|
69395 | 349 |
} |