author | wenzelm |
Sat, 08 Apr 2023 18:46:17 +0200 | |
changeset 77789 | 59ab77f7d021 |
parent 77762 | f73400337c5c |
child 78610 | fd1fec53665b |
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 |
||
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
36 |
/* platforms */ |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
37 |
|
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
38 |
private val family_platforms: Map[Platform.Family.Value, List[String]] = |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
39 |
Map( |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
40 |
Platform.Family.linux_arm -> List("arm64-linux", "arm64_32-linux"), |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
41 |
Platform.Family.linux -> List("x86_64-linux", "x86_64_32-linux"), |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
42 |
Platform.Family.macos -> |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
43 |
List("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
44 |
Platform.Family.windows -> |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
45 |
List("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
46 |
|
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
47 |
private val platform_names: Set[String] = |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
48 |
Set("x86-linux", "x86-cygwin") ++ family_platforms.iterator.flatMap(_._2) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
49 |
|
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
50 |
def platform_purge(platforms: List[Platform.Family.Value]): String => Boolean = { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
51 |
val preserve = |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
52 |
(for { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
53 |
family <- platforms.iterator |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
54 |
platform <- family_platforms(family) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
55 |
} yield platform).toSet |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
56 |
(name: String) => platform_names(name) && !preserve(name) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
57 |
} |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
58 |
|
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
59 |
|
69395 | 60 |
/* component collections */ |
61 |
||
77128
f40c36ab154d
clarified names to emphasize suble differences in meaning;
wenzelm
parents:
77098
diff
changeset
|
62 |
def static_component_repository: String = |
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
|
63 |
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
|
64 |
|
71601 | 65 |
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") |
77128
f40c36ab154d
clarified names to emphasize suble differences in meaning;
wenzelm
parents:
77098
diff
changeset
|
66 |
val dynamic_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" |
77762 | 67 |
val classic_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib") |
69434 | 68 |
|
77055 | 69 |
val default_catalogs: List[String] = List("main") |
70 |
val optional_catalogs: List[String] = List("main", "optional") |
|
71 |
||
69395 | 72 |
def admin(dir: Path): Path = dir + Path.explode("Admin/components") |
73 |
||
74 |
def contrib(dir: Path = Path.current, name: String = ""): Path = |
|
75 |
dir + Path.explode("contrib") + Path.explode(name) |
|
76 |
||
77059 | 77 |
def unpack( |
78 |
dir: Path, |
|
79 |
archive: Path, |
|
80 |
ssh: SSH.System = SSH.Local, |
|
81 |
progress: Progress = new Progress |
|
82 |
): String = { |
|
69413 | 83 |
val name = Archive.get_name(archive.file_name) |
77098
9d6118cdc0fd
tuned message, following "isabelle components -a";
wenzelm
parents:
77097
diff
changeset
|
84 |
progress.echo("Unpacking " + archive.base) |
77059 | 85 |
ssh.execute( |
77066 | 86 |
"tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive), |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77216
diff
changeset
|
87 |
progress_stdout = progress.echo(_), |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77216
diff
changeset
|
88 |
progress_stderr = progress.echo(_)).check |
69413 | 89 |
name |
90 |
} |
|
91 |
||
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
92 |
def clean( |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
93 |
component_dir: Path, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
94 |
platforms: List[Platform.Family.Value] = Platform.Family.list, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
95 |
ssh: SSH.System = SSH.Local, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
96 |
progress: Progress = new Progress |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
97 |
): Unit = { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
98 |
val purge = platform_purge(platforms) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
99 |
for { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
100 |
name <- ssh.read_dir(component_dir) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
101 |
path = Path.basic(name) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
102 |
if purge(name) && ssh.is_dir(component_dir + path) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
103 |
} { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
104 |
progress.echo("Removing " + (component_dir.base + path)) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
105 |
ssh.rm_tree(component_dir + path) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
106 |
} |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
107 |
} |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
108 |
|
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
109 |
def clean_base( |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
110 |
base_dir: Path, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
111 |
platforms: List[Platform.Family.Value] = Platform.Family.list, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
112 |
ssh: SSH.System = SSH.Local, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
113 |
progress: Progress = new Progress |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
114 |
): Unit = { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
115 |
for { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
116 |
name <- ssh.read_dir(base_dir) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
117 |
dir = base_dir + Path.basic(name) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
118 |
if is_component_dir(dir) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
119 |
} clean(dir, platforms = platforms, ssh = ssh, progress = progress) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
120 |
} |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
121 |
|
77059 | 122 |
def resolve( |
123 |
base_dir: Path, |
|
77067 | 124 |
name: String, |
69401
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
125 |
target_dir: Option[Path] = None, |
70102 | 126 |
copy_dir: Option[Path] = None, |
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
127 |
clean_platforms: Option[List[Platform.Family.Value]] = None, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
128 |
clean_archives: Boolean = false, |
77128
f40c36ab154d
clarified names to emphasize suble differences in meaning;
wenzelm
parents:
77098
diff
changeset
|
129 |
component_repository: String = Components.static_component_repository, |
77059 | 130 |
ssh: SSH.System = SSH.Local, |
75393 | 131 |
progress: Progress = new Progress |
132 |
): Unit = { |
|
77059 | 133 |
ssh.make_directory(base_dir) |
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
134 |
|
77067 | 135 |
val archive_name = Archive(name) |
77068 | 136 |
val archive = base_dir + Path.basic(archive_name) |
77067 | 137 |
if (!ssh.is_file(archive)) { |
138 |
val remote = Url.append_path(component_repository, archive_name) |
|
139 |
ssh.download_file(remote, archive, progress = progress) |
|
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
140 |
} |
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
141 |
|
77067 | 142 |
for (dir <- copy_dir) { |
143 |
ssh.make_directory(dir) |
|
144 |
ssh.copy_file(archive, dir) |
|
145 |
} |
|
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
146 |
|
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
147 |
val unpack_dir = target_dir getOrElse base_dir |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
148 |
unpack(unpack_dir, archive, ssh = ssh, progress = progress) |
69398
0698ded5caf1
Components.download similar to "isabelle components", but without unpacking;
wenzelm
parents:
69395
diff
changeset
|
149 |
|
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
150 |
if (clean_platforms.isDefined) { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
151 |
clean(unpack_dir + Path.basic(name), |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
152 |
platforms = clean_platforms.get, ssh = ssh, progress = progress) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
153 |
} |
73637 | 154 |
|
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
155 |
if (clean_archives) { |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
156 |
progress.echo("Removing " + quote(archive_name)) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
157 |
ssh.delete(archive) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
158 |
} |
69401
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
159 |
} |
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents:
69398
diff
changeset
|
160 |
|
77762 | 161 |
def provide(local_dir: Path, |
162 |
base_dir: Path = classic_components_base, |
|
163 |
ssh: SSH.System = SSH.Local, |
|
164 |
progress: Progress = new Progress |
|
165 |
): Directory = { |
|
166 |
val base_name = local_dir.expand.base |
|
167 |
val local_directory = Directory(local_dir).check |
|
168 |
val remote_directory = Directory(base_dir + base_name, ssh = ssh) |
|
169 |
if (!remote_directory.ok) { |
|
170 |
progress.echo("Providing " + base_name + ssh.print) |
|
171 |
Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar => |
|
172 |
ssh.with_tmp_dir { remote_tmp_dir => |
|
173 |
val remote_tmp_tar = remote_tmp_dir + Path.basic("tmp.tar") |
|
174 |
val remote_dir = ssh.make_directory(remote_directory.path) |
|
175 |
Isabelle_System.gnutar( |
|
176 |
"-cf " + File.bash_path(local_tmp_tar) + " .", dir = local_dir).check |
|
177 |
ssh.write_file(remote_tmp_tar, local_tmp_tar) |
|
178 |
ssh.execute( |
|
179 |
"tar -C " + ssh.bash_path(remote_dir) + " -xf " + ssh.bash_path(remote_tmp_tar)).check |
|
180 |
} |
|
181 |
} |
|
182 |
} |
|
183 |
remote_directory.check |
|
184 |
} |
|
185 |
||
69395 | 186 |
|
73815 | 187 |
/* component directories */ |
188 |
||
189 |
def directories(): List[Path] = |
|
190 |
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) |
|
191 |
||
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
192 |
def is_component_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean = |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
193 |
ssh.is_file(dir + Path.explode("etc/settings")) || |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
194 |
ssh.is_file(dir + Path.explode("etc/components")) |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77090
diff
changeset
|
195 |
|
73815 | 196 |
|
69395 | 197 |
/* component directory content */ |
198 |
||
76518 | 199 |
object Directory { |
77760 | 200 |
def apply(path: Path, ssh: SSH.System = SSH.Local): Directory = |
201 |
new Directory(ssh.absolute_path(path), ssh) |
|
76518 | 202 |
} |
203 |
||
77760 | 204 |
class Directory private(val path: Path, val ssh: SSH.System = SSH.Local) { |
77789 | 205 |
override def toString: String = path.toString + ssh.print |
76518 | 206 |
|
207 |
def etc: Path = path + Path.basic("etc") |
|
208 |
def src: Path = path + Path.basic("src") |
|
209 |
def lib: Path = path + Path.basic("lib") |
|
210 |
def settings: Path = etc + Path.basic("settings") |
|
211 |
def components: Path = etc + Path.basic("components") |
|
212 |
def build_props: Path = etc + Path.basic("build.props") |
|
213 |
def README: Path = path + Path.basic("README") |
|
214 |
def LICENSE: Path = path + Path.basic("LICENSE") |
|
215 |
||
76547 | 216 |
def create(progress: Progress = new Progress): Directory = { |
77789 | 217 |
progress.echo("Creating component directory " + toString) |
77760 | 218 |
ssh.new_directory(path) |
219 |
ssh.make_directory(etc) |
|
76547 | 220 |
this |
221 |
} |
|
222 |
||
77760 | 223 |
def ok: Boolean = |
224 |
ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh) |
|
76550 | 225 |
|
226 |
def check: Directory = |
|
77789 | 227 |
if (!ssh.is_dir(path)) error("Bad component directory: " + toString) |
76550 | 228 |
else if (!ok) { |
77789 | 229 |
error("Malformed component directory: " + toString + |
76550 | 230 |
"\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") |
231 |
} |
|
232 |
else this |
|
69395 | 233 |
|
76519 | 234 |
def read_components(): List[String] = |
77760 | 235 |
split_lines(ssh.read(components)).filter(_.nonEmpty) |
76519 | 236 |
def write_components(lines: List[String]): Unit = |
77760 | 237 |
ssh.write(components, terminate_lines(lines)) |
76548 | 238 |
|
239 |
def write_settings(text: String): Unit = |
|
77760 | 240 |
ssh.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) |
76519 | 241 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
242 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
243 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
244 |
/* component repository content */ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
245 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
246 |
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
|
247 |
|
77209 | 248 |
sealed case class SHA1_Entry(digest: SHA1.Digest, name: String) { |
249 |
override def toString: String = SHA1.shasum(digest, name).toString |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
250 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
251 |
|
77209 | 252 |
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Entry] = |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
253 |
(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
|
254 |
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
|
255 |
case Nil => None |
77209 | 256 |
case List(sha1, name) => Some(SHA1_Entry(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
|
257 |
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
|
258 |
}) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
259 |
|
77209 | 260 |
def write_components_sha1(entries: List[SHA1_Entry]): Unit = |
77592 | 261 |
File.write(components_sha1, entries.sortBy(_.name).mkString) |
69429
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 |
|
73172 | 264 |
/** manage user components **/ |
265 |
||
75349 | 266 |
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") |
73172 | 267 |
|
268 |
def read_components(): List[String] = |
|
269 |
if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) |
|
270 |
else Nil |
|
271 |
||
75393 | 272 |
def write_components(lines: List[String]): Unit = { |
73172 | 273 |
Isabelle_System.make_directory(components_path.dir) |
77216 | 274 |
File.write(components_path, terminate_lines(lines)) |
73172 | 275 |
} |
276 |
||
75393 | 277 |
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { |
73172 | 278 |
val path = path0.expand.absolute |
76551
c7996b073524
clarified check: allow to remove bad directories;
wenzelm
parents:
76550
diff
changeset
|
279 |
if (add) Directory(path).check |
73172 | 280 |
|
281 |
val lines1 = read_components() |
|
282 |
val lines2 = |
|
283 |
lines1.filter(line => |
|
284 |
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) |
|
285 |
val lines3 = if (add) lines2 ::: List(path.implode) else lines2 |
|
286 |
||
287 |
if (lines1 != lines3) write_components(lines3) |
|
288 |
||
289 |
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" |
|
290 |
progress.echo(prefix + " component " + path) |
|
291 |
} |
|
292 |
||
293 |
||
294 |
/* main entry point */ |
|
295 |
||
75393 | 296 |
def main(args: Array[String]): Unit = { |
73172 | 297 |
Command_Line.tool { |
298 |
for (arg <- args) { |
|
299 |
val add = |
|
300 |
if (arg.startsWith("+")) true |
|
301 |
else if (arg.startsWith("-")) false |
|
302 |
else error("Bad argument: " + quote(arg)) |
|
303 |
val path = Path.explode(arg.substring(1)) |
|
304 |
update_components(add, path, progress = new Console_Progress) |
|
305 |
} |
|
306 |
} |
|
307 |
} |
|
308 |
||
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
309 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
310 |
/** 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
|
311 |
|
77565
fd87490429aa
renamed "isabelle build_components" to "isabelle components_build" (unrelated to "isabelle build");
wenzelm
parents:
77509
diff
changeset
|
312 |
def components_build( |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
313 |
options: Options, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
314 |
components: List[Path], |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
315 |
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
|
316 |
publish: Boolean = false, |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
317 |
force: Boolean = false, |
75393 | 318 |
update_components_sha1: Boolean = false |
319 |
): Unit = { |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
320 |
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
|
321 |
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
|
322 |
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
|
323 |
case Archive(_) => path |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
324 |
case name => |
76550 | 325 |
Directory(path).check |
326 |
val component_path = path.expand |
|
327 |
val archive_dir = component_path.dir |
|
328 |
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
|
329 |
|
76550 | 330 |
val archive = archive_dir + Path.explode(archive_name) |
331 |
if (archive.is_file && !force) { |
|
332 |
error("Component archive already exists: " + archive) |
|
333 |
} |
|
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
334 |
|
76550 | 335 |
progress.echo("Packaging " + archive_name) |
336 |
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), |
|
337 |
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
|
338 |
|
76550 | 339 |
archive |
69429
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 |
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
|
344 |
val server = options.string("isabelle_components_server") |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
345 |
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
|
346 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
347 |
using(SSH.open_session(options, server)) { ssh => |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
348 |
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
|
349 |
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
|
350 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
351 |
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
|
352 |
error("Bad remote directory: " + dir) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
353 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
354 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
355 |
if (publish) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
356 |
for (archive <- archives) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
357 |
val archive_name = archive.file_name |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
358 |
val name = Archive.get_name(archive_name) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
359 |
val remote_component = components_dir + archive.base |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
360 |
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
|
361 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
362 |
// component archive |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
363 |
if (ssh.is_file(remote_component) && !force) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
364 |
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
|
365 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
366 |
progress.echo("Uploading " + archive_name) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
367 |
ssh.write_file(remote_component, archive) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
368 |
|
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
369 |
// contrib directory |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
370 |
val is_standard_component = |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
371 |
Isabelle_System.with_tmp_dir("component") { tmp_dir => |
76540
83de6e9ae983
clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents:
76519
diff
changeset
|
372 |
Isabelle_System.extract(archive, tmp_dir) |
76550 | 373 |
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
|
374 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
375 |
if (is_standard_component) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
376 |
if (ssh.is_dir(remote_contrib)) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
377 |
if (force) ssh.rm_tree(remote_contrib) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
378 |
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
|
379 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
380 |
progress.echo("Unpacking remote " + archive_name) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
381 |
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
|
382 |
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
|
383 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
384 |
else { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
385 |
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
|
386 |
} |
75394 | 387 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
388 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
389 |
|
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
390 |
// remote SHA1 digests |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
391 |
if (update_components_sha1) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
392 |
val lines = |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
393 |
for { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
394 |
entry <- ssh.read_dir(components_dir) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
395 |
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
|
396 |
entry.endsWith(Archive.suffix) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
397 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
398 |
yield { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
399 |
progress.echo("Digesting remote " + entry) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
400 |
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
|
401 |
"; sha1sum " + Bash.string(entry)).check.out |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
402 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
403 |
write_components_sha1(read_components_sha1(lines)) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76122
diff
changeset
|
404 |
} |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
405 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
406 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
407 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
408 |
// local SHA1 digests |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
409 |
{ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
410 |
val new_entries = |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
411 |
for (archive <- archives) |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
412 |
yield { |
75349 | 413 |
val name = archive.file_name |
414 |
progress.echo("Digesting local " + name) |
|
77209 | 415 |
SHA1_Entry(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
|
416 |
} |
75349 | 417 |
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
|
418 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
419 |
write_components_sha1( |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
420 |
new_entries ::: |
75349 | 421 |
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
|
422 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
423 |
} |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
424 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
425 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
426 |
/* Isabelle tool wrapper */ |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
427 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
428 |
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
|
429 |
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
|
430 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
431 |
val isabelle_tool = |
77565
fd87490429aa
renamed "isabelle build_components" to "isabelle components_build" (unrelated to "isabelle build");
wenzelm
parents:
77509
diff
changeset
|
432 |
Isabelle_Tool("components_build", "build and publish Isabelle components", |
75394 | 433 |
Scala_Project.here, |
434 |
{ args => |
|
435 |
var publish = false |
|
436 |
var update_components_sha1 = false |
|
437 |
var force = false |
|
438 |
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
|
439 |
|
75394 | 440 |
def show_options: String = |
75844
7d27944d7141
clarified signature: avoid public representation;
wenzelm
parents:
75394
diff
changeset
|
441 |
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
|
442 |
|
75394 | 443 |
val getopts = Getopts(""" |
77565
fd87490429aa
renamed "isabelle build_components" to "isabelle components_build" (unrelated to "isabelle build");
wenzelm
parents:
77509
diff
changeset
|
444 |
Usage: isabelle components_build [OPTIONS] ARCHIVES... DIRS... |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
445 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
446 |
Options are: |
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
447 |
-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
|
448 |
-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
|
449 |
-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
|
450 |
-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
|
451 |
|
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69426
diff
changeset
|
452 |
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
|
453 |
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
|
454 |
|
73736 | 455 |
""" + Library.indent_lines(2, show_options) + "\n", |
75394 | 456 |
"P" -> (_ => publish = true), |
457 |
"f" -> (_ => force = true), |
|
458 |
"o:" -> (arg => options = options + arg), |
|
459 |
"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
|
460 |
|
75394 | 461 |
val more_args = getopts(args) |
462 |
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
|
463 |
|
75394 | 464 |
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
|
465 |
|
77565
fd87490429aa
renamed "isabelle build_components" to "isabelle components_build" (unrelated to "isabelle build");
wenzelm
parents:
77509
diff
changeset
|
466 |
components_build(options, more_args.map(Path.explode), progress = progress, |
75394 | 467 |
publish = publish, force = force, update_components_sha1 = update_components_sha1) |
468 |
}) |
|
69395 | 469 |
} |