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