219 } |
219 } |
220 } |
220 } |
221 } |
221 } |
222 |
222 |
223 if ((publish && archives.nonEmpty) || update_components_sha1) { |
223 if ((publish && archives.nonEmpty) || update_components_sha1) { |
224 options.string("isabelle_components_server") match { |
224 val server = options.string("isabelle_components_server") |
225 case SSH.Target(user, host) => |
225 if (server.isEmpty) error("Undefined option isabelle_components_server") |
226 using(SSH.open_session(options, host = host, user = user)) { ssh => |
226 |
227 val components_dir = Path.explode(options.string("isabelle_components_dir")) |
227 using(SSH.open_session(options, server)) { ssh => |
228 val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) |
228 val components_dir = Path.explode(options.string("isabelle_components_dir")) |
229 |
229 val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) |
230 for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { |
230 |
231 error("Bad remote directory: " + dir) |
231 for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { |
232 } |
232 error("Bad remote directory: " + dir) |
233 |
233 } |
234 if (publish) { |
234 |
235 for (archive <- archives) { |
235 if (publish) { |
236 val archive_name = archive.file_name |
236 for (archive <- archives) { |
237 val name = Archive.get_name(archive_name) |
237 val archive_name = archive.file_name |
238 val remote_component = components_dir + archive.base |
238 val name = Archive.get_name(archive_name) |
239 val remote_contrib = contrib_dir + Path.explode(name) |
239 val remote_component = components_dir + archive.base |
240 |
240 val remote_contrib = contrib_dir + Path.explode(name) |
241 // component archive |
241 |
242 if (ssh.is_file(remote_component) && !force) { |
242 // component archive |
243 error("Remote component archive already exists: " + remote_component) |
243 if (ssh.is_file(remote_component) && !force) { |
244 } |
244 error("Remote component archive already exists: " + remote_component) |
245 progress.echo("Uploading " + archive_name) |
245 } |
246 ssh.write_file(remote_component, archive) |
246 progress.echo("Uploading " + archive_name) |
247 |
247 ssh.write_file(remote_component, archive) |
248 // contrib directory |
248 |
249 val is_standard_component = |
249 // contrib directory |
250 Isabelle_System.with_tmp_dir("component") { tmp_dir => |
250 val is_standard_component = |
251 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
251 Isabelle_System.with_tmp_dir("component") { tmp_dir => |
252 check_dir(tmp_dir + Path.explode(name)) |
252 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
253 } |
253 check_dir(tmp_dir + Path.explode(name)) |
254 if (is_standard_component) { |
|
255 if (ssh.is_dir(remote_contrib)) { |
|
256 if (force) ssh.rm_tree(remote_contrib) |
|
257 else error("Remote component directory already exists: " + remote_contrib) |
|
258 } |
|
259 progress.echo("Unpacking remote " + archive_name) |
|
260 ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + |
|
261 ssh.bash_path(remote_component)).check |
|
262 } |
|
263 else { |
|
264 progress.echo_warning("No unpacking of non-standard component: " + archive_name) |
|
265 } |
|
266 } |
254 } |
267 } |
255 if (is_standard_component) { |
268 |
256 if (ssh.is_dir(remote_contrib)) { |
269 // remote SHA1 digests |
257 if (force) ssh.rm_tree(remote_contrib) |
270 if (update_components_sha1) { |
258 else error("Remote component directory already exists: " + remote_contrib) |
271 val lines = |
259 } |
272 for { |
260 progress.echo("Unpacking remote " + archive_name) |
273 entry <- ssh.read_dir(components_dir) |
261 ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + |
274 if ssh.is_file(components_dir + Path.basic(entry)) && |
262 ssh.bash_path(remote_component)).check |
275 entry.endsWith(Archive.suffix) |
263 } |
276 } |
264 else { |
277 yield { |
265 progress.echo_warning("No unpacking of non-standard component: " + archive_name) |
278 progress.echo("Digesting remote " + entry) |
|
279 ssh.execute("cd " + ssh.bash_path(components_dir) + |
|
280 "; sha1sum " + Bash.string(entry)).check.out |
|
281 } |
|
282 write_components_sha1(read_components_sha1(lines)) |
|
283 } |
266 } |
284 } |
267 } |
285 case s => error("Bad isabelle_components_server: " + quote(s)) |
268 } |
|
269 |
|
270 // remote SHA1 digests |
|
271 if (update_components_sha1) { |
|
272 val lines = |
|
273 for { |
|
274 entry <- ssh.read_dir(components_dir) |
|
275 if ssh.is_file(components_dir + Path.basic(entry)) && |
|
276 entry.endsWith(Archive.suffix) |
|
277 } |
|
278 yield { |
|
279 progress.echo("Digesting remote " + entry) |
|
280 ssh.execute("cd " + ssh.bash_path(components_dir) + |
|
281 "; sha1sum " + Bash.string(entry)).check.out |
|
282 } |
|
283 write_components_sha1(read_components_sha1(lines)) |
|
284 } |
286 } |
285 } |
287 } |
286 } |
288 |
287 |
289 // local SHA1 digests |
288 // local SHA1 digests |
290 { |
289 { |