author | wenzelm |
Tue, 24 Jan 2023 11:36:15 +0100 | |
changeset 77068 | ef1831744f00 |
parent 77067 | 9ca1e7fc2663 |
child 77083 | 092449efcb0e |
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 |
|
77055 | 43 |
val default_catalogs: List[String] = List("main") |
44 |
val optional_catalogs: List[String] = List("main", "optional") |
|
45 |
||
69395 | 46 |
def admin(dir: Path): Path = dir + Path.explode("Admin/components") |
47 |
||
48 |
def contrib(dir: Path = Path.current, name: String = ""): Path = |
|
49 |
dir + Path.explode("contrib") + Path.explode(name) |
|
50 |
||
77059 | 51 |
def unpack( |
52 |
dir: Path, |
|
53 |
archive: Path, |
|
54 |
ssh: SSH.System = SSH.Local, |
|
55 |
progress: Progress = new Progress |
|
56 |
): String = { |
|
69413 | 57 |
val name = Archive.get_name(archive.file_name) |
58 |
progress.echo("Unpacking " + name) |
|
77059 | 59 |
ssh.execute( |
77066 | 60 |
"tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive), |
77059 | 61 |
progress_stdout = progress.echo, |
62 |
progress_stderr = progress.echo).check |
|
69413 | 63 |
name |
64 |
} |
|
65 |
||
77059 | 66 |
def resolve( |
67 |
base_dir: Path, |
|
77067 | 68 |
name: String, |
69401
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
69 |
target_dir: Option[Path] = None, |
70102 | 70 |
copy_dir: Option[Path] = None, |
77057 | 71 |
component_repository: String = Components.default_component_repository, |
77059 | 72 |
ssh: SSH.System = SSH.Local, |
75393 | 73 |
progress: Progress = new Progress |
74 |
): Unit = { |
|
77059 | 75 |
ssh.make_directory(base_dir) |
77067 | 76 |
val archive_name = Archive(name) |
77068 | 77 |
val archive = base_dir + Path.basic(archive_name) |
77067 | 78 |
if (!ssh.is_file(archive)) { |
79 |
val remote = Url.append_path(component_repository, archive_name) |
|
80 |
ssh.download_file(remote, archive, progress = progress) |
|
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
81 |
} |
77067 | 82 |
for (dir <- copy_dir) { |
83 |
ssh.make_directory(dir) |
|
84 |
ssh.copy_file(archive, dir) |
|
85 |
} |
|
86 |
unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress) |
|
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
87 |
} |
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
88 |
|
73637 | 89 |
private val platforms_family: Map[Platform.Family.Value, Set[String]] = |
90 |
Map( |
|
91 |
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), |
|
92 |
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), |
|
93 |
Platform.Family.macos -> |
|
94 |
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), |
|
95 |
Platform.Family.windows -> |
|
96 |
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) |
|
97 |
||
98 |
private val platforms_all: Set[String] = |
|
99 |
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) |
|
100 |
||
75393 | 101 |
def purge(dir: Path, platform: Platform.Family.Value): Unit = { |
73637 | 102 |
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
|
103 |
|
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
104 |
File.find_files(dir.file, |
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
105 |
(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
|
106 |
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
|
107 |
} |
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
108 |
|
69395 | 109 |
|
73815 | 110 |
/* component directories */ |
111 |
||
112 |
def directories(): List[Path] = |
|
113 |
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) |
|
114 |
||
115 |
||
69395 | 116 |
/* component directory content */ |
117 |
||
76518 | 118 |
object Directory { |
119 |
def apply(path: Path): Directory = new Directory(path.absolute) |
|
120 |
} |
|
121 |
||
122 |
class Directory private(val path: Path) { |
|
123 |
override def toString: String = path.toString |
|
124 |
||
125 |
def etc: Path = path + Path.basic("etc") |
|
126 |
def src: Path = path + Path.basic("src") |
|
127 |
def lib: Path = path + Path.basic("lib") |
|
128 |
def settings: Path = etc + Path.basic("settings") |
|
129 |
def components: Path = etc + Path.basic("components") |
|
130 |
def build_props: Path = etc + Path.basic("build.props") |
|
131 |
def README: Path = path + Path.basic("README") |
|
132 |
def LICENSE: Path = path + Path.basic("LICENSE") |
|
133 |
||
76547 | 134 |
def create(progress: Progress = new Progress): Directory = { |
135 |
progress.echo("Creating component directory " + path) |
|
136 |
Isabelle_System.new_directory(path) |
|
137 |
Isabelle_System.make_directory(etc) |
|
138 |
this |
|
139 |
} |
|
140 |
||
76550 | 141 |
def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path) |
142 |
||
143 |
def check: Directory = |
|
144 |
if (!path.is_dir) error("Bad component directory: " + path) |
|
145 |
else if (!ok) { |
|
146 |
error("Malformed component directory: " + path + |
|
147 |
"\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") |
|
148 |
} |
|
149 |
else this |
|
69395 | 150 |
|
76519 | 151 |
def read_components(): List[String] = |
152 |
split_lines(File.read(components)).filter(_.nonEmpty) |
|
153 |
def write_components(lines: List[String]): Unit = |
|
154 |
File.write(components, terminate_lines(lines)) |
|
76548 | 155 |
|
156 |
def write_settings(text: String): Unit = |
|
157 |
File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) |
|
76519 | 158 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
159 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
160 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
161 |
/* component repository content */ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
162 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
163 |
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
|
164 |
|
75393 | 165 |
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
|
166 |
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
|
167 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
168 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
169 |
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
|
170 |
(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
|
171 |
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
|
172 |
case Nil => None |
75349 | 173 |
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
|
174 |
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
|
175 |
}) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
176 |
|
71601 | 177 |
def write_components_sha1(entries: List[SHA1_Digest]): Unit = |
75349 | 178 |
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
|
179 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
180 |
|
73172 | 181 |
/** manage user components **/ |
182 |
||
75349 | 183 |
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") |
73172 | 184 |
|
185 |
def read_components(): List[String] = |
|
186 |
if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) |
|
187 |
else Nil |
|
188 |
||
75393 | 189 |
def write_components(lines: List[String]): Unit = { |
73172 | 190 |
Isabelle_System.make_directory(components_path.dir) |
191 |
File.write(components_path, Library.terminate_lines(lines)) |
|
192 |
} |
|
193 |
||
75393 | 194 |
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { |
73172 | 195 |
val path = path0.expand.absolute |
76551
c7996b073524
clarified check: allow to remove bad directories;
wenzelm
parents:
76550
diff
changeset
|
196 |
if (add) Directory(path).check |
73172 | 197 |
|
198 |
val lines1 = read_components() |
|
199 |
val lines2 = |
|
200 |
lines1.filter(line => |
|
201 |
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) |
|
202 |
val lines3 = if (add) lines2 ::: List(path.implode) else lines2 |
|
203 |
||
204 |
if (lines1 != lines3) write_components(lines3) |
|
205 |
||
206 |
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" |
|
207 |
progress.echo(prefix + " component " + path) |
|
208 |
} |
|
209 |
||
210 |
||
211 |
/* main entry point */ |
|
212 |
||
75393 | 213 |
def main(args: Array[String]): Unit = { |
73172 | 214 |
Command_Line.tool { |
215 |
for (arg <- args) { |
|
216 |
val add = |
|
217 |
if (arg.startsWith("+")) true |
|
218 |
else if (arg.startsWith("-")) false |
|
219 |
else error("Bad argument: " + quote(arg)) |
|
220 |
val path = Path.explode(arg.substring(1)) |
|
221 |
update_components(add, path, progress = new Console_Progress) |
|
222 |
} |
|
223 |
} |
|
224 |
} |
|
225 |
||
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
226 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
227 |
/** 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
|
228 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
229 |
def build_components( |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
230 |
options: Options, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
231 |
components: List[Path], |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
232 |
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
|
233 |
publish: Boolean = false, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
234 |
force: Boolean = false, |
75393 | 235 |
update_components_sha1: Boolean = false |
236 |
): Unit = { |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
237 |
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
|
238 |
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
|
239 |
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
|
240 |
case Archive(_) => path |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
241 |
case name => |
76550 | 242 |
Directory(path).check |
243 |
val component_path = path.expand |
|
244 |
val archive_dir = component_path.dir |
|
245 |
val archive_name = Archive(name) |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
246 |
|
76550 | 247 |
val archive = archive_dir + Path.explode(archive_name) |
248 |
if (archive.is_file && !force) { |
|
249 |
error("Component archive already exists: " + archive) |
|
250 |
} |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
251 |
|
76550 | 252 |
progress.echo("Packaging " + archive_name) |
253 |
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), |
|
254 |
dir = archive_dir).check |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
255 |
|
76550 | 256 |
archive |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
257 |
} |
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 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
260 |
if ((publish && archives.nonEmpty) || update_components_sha1) { |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
261 |
val server = options.string("isabelle_components_server") |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
262 |
if (server.isEmpty) error("Undefined option isabelle_components_server") |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
263 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
264 |
using(SSH.open_session(options, server)) { ssh => |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
265 |
val components_dir = Path.explode(options.string("isabelle_components_dir")) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
266 |
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
267 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
268 |
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
269 |
error("Bad remote directory: " + dir) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
270 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
271 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
272 |
if (publish) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
273 |
for (archive <- archives) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
274 |
val archive_name = archive.file_name |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
275 |
val name = Archive.get_name(archive_name) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
276 |
val remote_component = components_dir + archive.base |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
277 |
val remote_contrib = contrib_dir + Path.explode(name) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
278 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
279 |
// component archive |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
280 |
if (ssh.is_file(remote_component) && !force) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
281 |
error("Remote component archive already exists: " + remote_component) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
282 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
283 |
progress.echo("Uploading " + archive_name) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
284 |
ssh.write_file(remote_component, archive) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
285 |
|
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
286 |
// contrib directory |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
287 |
val is_standard_component = |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
288 |
Isabelle_System.with_tmp_dir("component") { tmp_dir => |
76540
83de6e9ae983
clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents:
76519
diff
changeset
|
289 |
Isabelle_System.extract(archive, tmp_dir) |
76550 | 290 |
Directory(tmp_dir + Path.explode(name)).ok |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
291 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
292 |
if (is_standard_component) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
293 |
if (ssh.is_dir(remote_contrib)) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
294 |
if (force) ssh.rm_tree(remote_contrib) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
295 |
else error("Remote component directory already exists: " + remote_contrib) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
296 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
297 |
progress.echo("Unpacking remote " + archive_name) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
298 |
ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
299 |
ssh.bash_path(remote_component)).check |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
300 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
301 |
else { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
302 |
progress.echo_warning("No unpacking of non-standard component: " + archive_name) |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
303 |
} |
75394 | 304 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
305 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
306 |
|
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
307 |
// remote SHA1 digests |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
308 |
if (update_components_sha1) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
309 |
val lines = |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
310 |
for { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
311 |
entry <- ssh.read_dir(components_dir) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
312 |
if ssh.is_file(components_dir + Path.basic(entry)) && |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
313 |
entry.endsWith(Archive.suffix) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
314 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
315 |
yield { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
316 |
progress.echo("Digesting remote " + entry) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
317 |
ssh.execute("cd " + ssh.bash_path(components_dir) + |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
318 |
"; sha1sum " + Bash.string(entry)).check.out |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
319 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
320 |
write_components_sha1(read_components_sha1(lines)) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
321 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
322 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
323 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
324 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
325 |
// local SHA1 digests |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
326 |
{ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
327 |
val new_entries = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
328 |
for (archive <- archives) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
329 |
yield { |
75349 | 330 |
val name = archive.file_name |
331 |
progress.echo("Digesting local " + name) |
|
332 |
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
|
333 |
} |
75349 | 334 |
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
|
335 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
336 |
write_components_sha1( |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
337 |
new_entries ::: |
75349 | 338 |
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
|
339 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
340 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
341 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
342 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
343 |
/* Isabelle tool wrapper */ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
344 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
345 |
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
|
346 |
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
|
347 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
348 |
val isabelle_tool = |
72763 | 349 |
Isabelle_Tool("build_components", "build and publish Isabelle components", |
75394 | 350 |
Scala_Project.here, |
351 |
{ args => |
|
352 |
var publish = false |
|
353 |
var update_components_sha1 = false |
|
354 |
var force = false |
|
355 |
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
|
356 |
|
75394 | 357 |
def show_options: String = |
75844
7d27944d7141
clarified signature: avoid public representation;
wenzelm
parents:
75394
diff
changeset
|
358 |
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
|
359 |
|
75394 | 360 |
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
|
361 |
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
|
362 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
363 |
Options are: |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
364 |
-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
|
365 |
-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
|
366 |
-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
|
367 |
-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
|
368 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
369 |
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
|
370 |
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
|
371 |
|
73736 | 372 |
""" + Library.indent_lines(2, show_options) + "\n", |
75394 | 373 |
"P" -> (_ => publish = true), |
374 |
"f" -> (_ => force = true), |
|
375 |
"o:" -> (arg => options = options + arg), |
|
376 |
"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
|
377 |
|
75394 | 378 |
val more_args = getopts(args) |
379 |
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
|
380 |
|
75394 | 381 |
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
|
382 |
|
75394 | 383 |
build_components(options, more_args.map(Path.explode), progress = progress, |
384 |
publish = publish, force = force, update_components_sha1 = update_components_sha1) |
|
385 |
}) |
|
69395 | 386 |
} |