--- a/Admin/Release/CHECKLIST Sat Dec 08 20:27:34 2018 +0000
+++ b/Admin/Release/CHECKLIST Sun Dec 09 00:08:59 2018 +0100
@@ -86,7 +86,7 @@
- fully-automated packaging (e.g. on lxbroy10):
- hg up -r DISTNAME && Admin/build_release -M macbroy30 -O -l -R DISTNAME /home/isabelle/dist
+ hg up -r DISTNAME && Admin/build_release -O -l -R DISTNAME /home/isabelle/dist
- Docker image:
--- a/Admin/components/README Sat Dec 08 20:27:34 2018 +0000
+++ b/Admin/components/README Sun Dec 09 00:08:59 2018 +0100
@@ -1,15 +1,28 @@
-Some notes on maintaining the Isabelle component repository at TUM
-==================================================================
+Notes on maintaining the Isabelle component repository at TUM
+=============================================================
Quick reference
---------------
- $ install /home/isabelle/components/screwdriver-3.14.tar.gz
- $ install /home/isabelle/contrib/screwdriver-3.14/
- $ edit Admin/components/main: screwdriver-3.14
- $ isabelle components_checksum -u
- $ hg diff
- $ hg commit
+ * ensure that Isabelle/Scala/SSH can connect to the host specified via
+ system option "isabelle_components_server"; this may require to install
+ an unencrypted ssh host key as follows:
+
+ $ ssh-keyscan -t rsa lxbroy10.informatik.tu-muenchen.de >> ~/.ssh/known_hosts
+
+ * local setup (and test) of component directory, e.g. in
+
+ screwdriver-3.14/
+
+ * packaging (with associated SHA1 digest), e.g.
+
+ $ isabelle build_components screwdriver-3.14
+
+ * publishing, e.g.
+
+ $ isabelle build_components -P screwdriver-3.14.tar.gz
+
+ * manual editing of Admin/components/main: screwdriver-3.14
Unique names
@@ -46,17 +59,20 @@
The file Admin/components/components.sha1 contains SHA1 identifiers
within the Isabelle repository, for integrity checking of the archives
-that are exposed to the public file-system. The components_checksum
-tool helps to update these hash-keys wrt. the information within the
-Isabelle repository.
+that are exposed to the public file-system. The command-line tool
+"isabelle build_components" maintains these hash-keys automatically.
Unpacked copy
-------------
-A second unpacked copy is provided in /home/isabelle/contrib/. This
-allows users within the TUM network to activate arbitrary snapshots of
-the repository with all standard components being available, without
-extra copying or unpacking of the authentic archives. Testing
-services like "isatest" and "mira" do this routinely, and will break
-accordingly if this is omitted.
+A second unpacked copy is provided in /home/isabelle/contrib/. This allows
+users and administrative services within the TUM network to activate arbitrary
+snapshots of the repository with all standard components being available,
+without extra copying or unpacking of the authentic archives. The
+isabelle_cronjob does this routinely: it will break if the unpacked version is
+omitted.
+
+The command-line tool "isabelle build_components -P" takes care of uploading
+the .tar.gz archive and unpacking it, unless it is a special component (e.g.
+for multiplatform application bundling).
--- a/Admin/components/bundled-macos Sat Dec 08 20:27:34 2018 +0000
+++ b/Admin/components/bundled-macos Sun Dec 09 00:08:59 2018 +0100
@@ -1,2 +1,2 @@
#additional components to be bundled for release
-macos_app-20181205
+macos_app-20181208
--- a/Admin/components/components.sha1 Sat Dec 08 20:27:34 2018 +0000
+++ b/Admin/components/components.sha1 Sun Dec 09 00:08:59 2018 +0100
@@ -1,3 +1,11 @@
+59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
+23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
+eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz
+8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
+847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
+8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
+51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz
+8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz
fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz
bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz
81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz
@@ -12,12 +20,12 @@
541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz
1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz
c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz
+3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz
a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz
4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz
b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz
76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz
03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz
-3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
@@ -51,9 +59,6 @@
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
-59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
-23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
-eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz
@@ -80,17 +85,17 @@
13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz
5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz
dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz
+ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz
e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz
d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz
-ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
b66039bc6dc2bdb2992133743005e1e4fc58ae24 jdk-7u72.tar.gz
d980055694ddfae430ee001c7ee877d535e97252 jdk-7u76.tar.gz
baa6de37bb6f7a104ce5fe6506bca3d2572d601a jdk-7u80.tar.gz
7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
baf275a68d3f799a841932e4e9a95a1a604058ae jdk-8u102.tar.gz
+5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
741de6a4a805a0f9fb917d1845409e99346c2747 jdk-8u112.tar.gz
-5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
ae7df8bd0c18eb40237cf54cc28933f4893b9c92 jdk-8u121.tar.gz
51531a3a0c16e180ed95cb7d2bd680c2ec0aa553 jdk-8u131.tar.gz
e45edcf184f608d6f4a7b966d65a5d3289462693 jdk-8u144.tar.gz
@@ -100,8 +105,8 @@
9ae0338a5277d8749b4b4c7e65fc627319d98b27 jdk-8u181.tar.gz
cfecb1383faaf027ffbabfcd77a0b6a6521e0969 jdk-8u20.tar.gz
44ffeeae219782d40ce6822b580e608e72fd4c76 jdk-8u31.tar.gz
+c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz
4132cf52d5025bf330d53b96a5c6466fef432377 jdk-8u51.tar.gz
-c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz
74df343671deba03be7caa49de217d78b693f817 jdk-8u60.tar.gz
dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz
2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz
@@ -152,6 +157,7 @@
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz
+3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz
26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz
fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz
@@ -171,12 +177,13 @@
b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz
1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz
f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz
+21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz
03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz
822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz
bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz
5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz
-21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz
5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz
+80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz
381a70cecf0fdee47f6842e2bdb5107ed52adab6 polyml-5.7.1-1.tar.gz
39dac33b569ac66f76126b8f4edc6d9227bd8a63 polyml-5.7.1-2.tar.gz
0b896ccc35bd3f2541cd55e6f0ed14637ed9fc68 polyml-5.7.1-4.tar.gz
@@ -185,7 +192,6 @@
e3e7e20b1e0e5d5d68df4cd4caa1e1a7410d46b6 polyml-5.7.1-7.tar.gz
1430533c09b17f8be73798a47a5f409d43a04cf4 polyml-5.7.1-8.tar.gz
171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz
-80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz
5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz
4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
@@ -199,11 +205,6 @@
e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40 postgresql-42.2.2.tar.gz
231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz
f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz
-8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
-847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
-8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
-51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz
-8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz
0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz
207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/etc/options Sun Dec 09 00:08:59 2018 +0100
@@ -0,0 +1,12 @@
+(* :mode=isabelle-options: *)
+
+section "Admin tools"
+
+option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de"
+ -- "user@host for SSH connection"
+
+option isabelle_components_dir : string = "/home/isabelle/components"
+ -- "webspace for ISABELLE_COMPONENT_REPOSITORY"
+
+option isabelle_components_contrib_dir : string = "/home/isabelle/contrib"
+ -- "unpacked components for remote build services"
--- a/Admin/lib/Tools/components_checksum Sat Dec 08 20:27:34 2018 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Alexander Krauss
-#
-# DESCRIPTION: compute and validate checksums for component repository
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS] [DIR]"
- echo
- echo " Options are:"
- echo " -u update the recorded checksums in the repository"
- echo " -c compare the actual checksums with the recorded ones"
- echo
- echo " Compute the checksums of component .tar.gz archives in DIR"
- echo " (default \"/home/isabelle/components\") and synchronize them"
- echo " with the Isabelle repository."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-UPDATE=""
-CHECK=""
-COMPONENTS_DIR="/home/isabelle/components"
-
-while getopts "uc" OPT
-do
- case "$OPT" in
- u)
- UPDATE=true
- ;;
- c)
- CHECK=true
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-[ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage
-
-
-# args
-
-[ "$#" -ge 1 ] && { COMPONENTS_DIR="$1"; shift; }
-[ "$#" -ne 0 ] && usage
-
-
-## compute checksums
-
-CHECKSUM_DIR="$ISABELLE_HOME/Admin/components"
-CHECKSUM_FILE="$CHECKSUM_DIR/components.sha1"
-CHECKSUM_TMP="$CHECKSUM_DIR/components.sha1.tmp"
-
-(
- cd "$COMPONENTS_DIR"
- sha1sum *.tar.gz | sort -k2 -f > "$CHECKSUM_TMP"
-)
-
-[ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
-[ -n "$CHECK" ] && {
- diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error"
-}
--- a/etc/options Sat Dec 08 20:27:34 2018 +0000
+++ b/etc/options Sun Dec 09 00:08:59 2018 +0100
@@ -230,13 +230,13 @@
section "Secure Shell"
-option ssh_config_dir : string = "~/.ssh"
+option ssh_config_dir : string = "$HOME/.ssh"
-- "SSH configuration directory"
-option ssh_config_file : string = "~/.ssh/config"
+option ssh_config_file : string = "$HOME/.ssh/config"
-- "main SSH configuration file"
-option ssh_identity_files : string = "~/.ssh/id_dsa:~/.ssh/id_ecdsa:~/.ssh/id_rsa"
+option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
-- "possible SSH identity files (separated by colons)"
option ssh_compression : bool = true
--- a/src/Pure/Admin/build_cygwin.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/Admin/build_cygwin.scala Sun Dec 09 00:08:59 2018 +0100
@@ -54,8 +54,7 @@
(cygwin + Path.explode("Cygwin.bat")).file.delete
val archive = "cygwin-" + Date.Format("uuuuMMdd")(Date.now()) + ".tar.gz"
- Isabelle_System.gnutar("-C " + File.bash_path(tmp_dir) +
- " -czf " + Bash.string(archive) + " cygwin").check
+ Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
})
}
--- a/src/Pure/Admin/build_jdk.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/Admin/build_jdk.scala Sun Dec 09 00:08:59 2018 +0100
@@ -102,8 +102,7 @@
"unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
}
else {
- Isabelle_System.gnutar(
- "-C " + File.bash_path(tmp_dir) + " -xzf " + File.bash_path(archive)).check
+ Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
}
val dir_entry =
@@ -204,8 +203,9 @@
}
progress.echo("Archiving ...")
- Isabelle_System.gnutar("--owner=root --group=root -C " + File.bash_path(dir) +
- " -czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name).check
+ Isabelle_System.gnutar(
+ "-czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name,
+ dir = dir).check
})
}
--- a/src/Pure/Admin/build_release.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/Admin/build_release.scala Sun Dec 09 00:08:59 2018 +0100
@@ -14,10 +14,9 @@
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
- main: String,
- fallback: Option[String])
+ name: String)
{
- def names: List[String] = main :: fallback.toList
+ def path: Path = Path.explode(name)
}
class Release private[Build_Release](
@@ -39,12 +38,9 @@
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
- case Platform.Family.linux =>
- Bundle_Info(platform, "Linux", dist_name + "_app.tar.gz", None)
- case Platform.Family.macos =>
- Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))
- case Platform.Family.windows =>
- Bundle_Info(platform, "Windows", dist_name + ".exe", None)
+ case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
+ case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz")
+ case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
@@ -221,10 +217,7 @@
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String): Unit =
- Isabelle_System.gnutar(args, cwd = dir.file).check
-
- private def tar_options: String =
- if (Platform.is_macos) "--owner=root --group=staff" else "--owner=root --group=root"
+ Isabelle_System.gnutar(args, dir = dir).check
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
@@ -241,8 +234,7 @@
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_library: Boolean = false,
- parallel_jobs: Int = 1,
- remote_mac: String = ""): Release =
+ parallel_jobs: Int = 1): Release =
{
val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
@@ -365,7 +357,7 @@
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
""")
- execute_tar(release.dist_dir, tar_options + " -czf " +
+ execute_tar(release.dist_dir, "-czf " +
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
execute_dist_name("""
@@ -395,16 +387,14 @@
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
- val bundle =
- (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main
- val bundle_archive = release.dist_dir + Path.explode(bundle)
+ val bundle_archive = release.dist_dir + bundle_info.path
if (bundle_archive.is_file && more_components.isEmpty)
progress.echo_warning("Application bundle already exists: " + bundle_archive)
else {
val isabelle_name = release.dist_name
val platform = bundle_info.platform
- progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive)
+ progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
@@ -464,7 +454,7 @@
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
- // platform-specific setup (inside archive)
+ // application bundling
platform match {
case Platform.Family.linux =>
@@ -484,8 +474,14 @@
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(linux_app)
+ val archive_name = isabelle_name + "_linux.tar.gz"
+ progress.echo("Packaging " + archive_name + " ...")
+ execute_tar(tmp_dir,
+ "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ Bash.string(isabelle_name))
+
+
case Platform.Family.macos =>
- File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
File.write(isabelle_target + jedit_props,
File.read(isabelle_target + jedit_props)
.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
@@ -493,101 +489,14 @@
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
.replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
- case Platform.Family.windows =>
- val app_template = Path.explode("~~/Admin/Windows/launch4j")
- val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
- File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
-
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*",
- "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
- .replaceAll("foldPainter=.*", "foldPainter=Square"))
-
- File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
- (java_options_title :: java_options).map(_ + "\r\n").mkString)
-
- val isabelle_xml = Path.explode("isabelle.xml")
- val isabelle_exe = Path.explode(isabelle_name + ".exe")
-
- File.write(tmp_dir + isabelle_xml,
- File.read(app_template + isabelle_xml)
- .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- .replaceAllLiterally("{OUTFILE}",
- File.platform_path(isabelle_target + isabelle_exe))
- .replaceAllLiterally("{ICON}",
- File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
- .replaceAllLiterally("{SPLASH}",
- File.platform_path(app_template + Path.explode("isabelle.bmp")))
- .replaceAllLiterally("{CLASSPATH}",
- cat_lines(classpath.map(cp =>
- " <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
- .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
-
- execute(tmp_dir,
- "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
-
- File.copy(app_template + Path.explode("manifest.xml"),
- isabelle_target + isabelle_exe.ext("manifest"))
-
-
- File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
-
- val cygwin_mirror =
- File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
+ // MacOS application bundle
- val cygwin_bat = Path.explode("Cygwin-Setup.bat")
- File.write(isabelle_target + cygwin_bat,
- File.read(cygwin_template + cygwin_bat)
- .replaceAllLiterally("{MIRROR}", cygwin_mirror))
- File.executable(isabelle_target + cygwin_bat)
-
- for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
- val path = Path.explode(name)
- File.copy(cygwin_template + path,
- isabelle_target + Path.explode("contrib/cygwin") + path)
- }
-
- execute(isabelle_target,
- """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
- (if (Platform.is_macos) "-perm +100" else "-executable") +
- " -print0 > contrib/cygwin/isabelle/executables")
-
- execute(isabelle_target,
- """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
- """> contrib/cygwin/isabelle/symlinks""")
-
- execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
-
- File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
- }
+ File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
-
- // archive
-
- val archive_name = isabelle_name + "_" + platform + ".tar.gz"
- progress.echo("Packaging " + archive_name + " ...")
- execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- Bash.string(isabelle_name))
-
-
- // platform-specific application (outside archive)
-
- progress.echo("Application for " + platform + " ...")
-
- platform match {
- case Platform.Family.linux =>
- File.link(
- Path.explode(isabelle_name + "_linux.tar.gz"),
- release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"),
- force = true)
-
- case Platform.Family.macos =>
- val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
- val app_dir = dmg_dir + Path.explode(isabelle_name + ".app")
- File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir)
+ val isabelle_app = Path.explode(isabelle_name + ".app")
+ val app_dir = tmp_dir + isabelle_app
+ File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
val app_contents = app_dir + Path.explode("Contents")
val app_resources = app_contents + Path.explode("Resources")
@@ -622,33 +531,94 @@
app_dir + Path.explode("Isabelle"),
force = true)
- val dmg = Path.explode(isabelle_name + ".dmg")
- (release.dist_dir + dmg).file.delete
+
+ // application archive
+
+ val archive_name = isabelle_name + "_macos.tar.gz"
+ progress.echo("Packaging " + archive_name + " ...")
+ execute_tar(tmp_dir,
+ "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ File.bash_path(isabelle_app))
+
- val dmg_archive = Path.explode(isabelle_name + "_dmg.tar.gz")
- execute_tar(dmg_dir, "-czf " + File.bash_path(release.dist_dir + dmg_archive) + " .")
+ case Platform.Family.windows =>
+ File.write(isabelle_target + jedit_props,
+ File.read(isabelle_target + jedit_props)
+ .replaceAll("lookAndFeel=.*",
+ "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
+ .replaceAll("foldPainter=.*", "foldPainter=Square"))
+
+
+ // application launcher
+
+ File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+
+ val app_template = Path.explode("~~/Admin/Windows/launch4j")
+
+ File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
+ (java_options_title :: java_options).map(_ + "\r\n").mkString)
+
+ val isabelle_xml = Path.explode("isabelle.xml")
+ val isabelle_exe = Path.explode(isabelle_name + ".exe")
- remote_mac match {
- case SSH.Target(user, host) =>
- progress.echo("Building dmg on " + quote(host) + " ...")
- using(SSH.open_session(options, host = host, user = user))(ssh =>
- {
- ssh.with_tmp_dir(remote_dir =>
- {
- val cd = "cd " + ssh.bash_path(remote_dir) + "; "
- ssh.write_file(remote_dir + dmg_archive, release.dist_dir + dmg_archive)
- ssh.execute(
- cd + "mkdir root && tar -C root -xzf " + ssh.bash_path(dmg_archive)).check
- ssh.execute(
- cd + "hdiutil create -srcfolder root -volname Isabelle " +
- ssh.bash_path(dmg)).check
- ssh.read_file(remote_dir + dmg, release.dist_dir + dmg)
- })
- })
- case _ =>
+ File.write(tmp_dir + isabelle_xml,
+ File.read(app_template + isabelle_xml)
+ .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ .replaceAllLiterally("{OUTFILE}",
+ File.platform_path(isabelle_target + isabelle_exe))
+ .replaceAllLiterally("{ICON}",
+ File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
+ .replaceAllLiterally("{SPLASH}",
+ File.platform_path(app_template + Path.explode("isabelle.bmp")))
+ .replaceAllLiterally("{CLASSPATH}",
+ cat_lines(classpath.map(cp =>
+ " <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
+ .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
+
+ execute(tmp_dir,
+ "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
+
+ File.copy(app_template + Path.explode("manifest.xml"),
+ isabelle_target + isabelle_exe.ext("manifest"))
+
+
+ // Cygwin setup
+
+ val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
+
+ File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
+
+ val cygwin_mirror =
+ File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
+
+ val cygwin_bat = Path.explode("Cygwin-Setup.bat")
+ File.write(isabelle_target + cygwin_bat,
+ File.read(cygwin_template + cygwin_bat)
+ .replaceAllLiterally("{MIRROR}", cygwin_mirror))
+ File.executable(isabelle_target + cygwin_bat)
+
+ for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
+ val path = Path.explode(name)
+ File.copy(cygwin_template + path,
+ isabelle_target + Path.explode("contrib/cygwin") + path)
}
- case Platform.Family.windows =>
+ execute(isabelle_target,
+ """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
+ (if (Platform.is_macos) "-perm +100" else "-executable") +
+ " -print0 > contrib/cygwin/isabelle/executables")
+
+ execute(isabelle_target,
+ """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
+ """> contrib/cygwin/isabelle/symlinks""")
+
+ execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
+
+ File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
+
+
+ // executable archive (self-extracting 7z)
+
val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
exe_archive.file.delete
@@ -656,7 +626,6 @@
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
- val isabelle_exe = Path.explode(isabelle_name + ".exe")
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
@@ -678,8 +647,8 @@
val website_platform_bundles =
for {
bundle_info <- bundle_infos
- bundle <- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file)
- } yield (bundle, bundle_info)
+ if (release.dist_dir + bundle_info.path).is_file
+ } yield (bundle_info.name, bundle_info)
val afp_link =
HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
@@ -723,8 +692,7 @@
execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
- execute_tar(tmp_dir,
- tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) +
+ execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
" " + Bash.string(release.dist_name + "/browser_info"))
})
}
@@ -742,7 +710,6 @@
Command_Line.tool0 {
var afp_rev = ""
var components_base: Option[Path] = None
- var remote_mac = ""
var official_release = false
var proper_release_name: Option[String] = None
var website: Option[Path] = None
@@ -759,7 +726,6 @@
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
- -M USER@HOST remote Mac OS X for dmg build
-O official release (not release-candidate)
-R RELEASE proper release with name
-W WEBSITE produce minimal website in given directory
@@ -774,7 +740,6 @@
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Some(Path.explode(arg))),
- "M:" -> (arg => remote_mac = arg),
"O" -> (_ => official_release = true),
"R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.explode(arg))),
@@ -805,7 +770,7 @@
if (platform_families.isEmpty) default_platform_families
else platform_families,
more_components = more_components, build_library = build_library,
- parallel_jobs = parallel_jobs, remote_mac = remote_mac)
+ parallel_jobs = parallel_jobs)
}
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/components.scala Sun Dec 09 00:08:59 2018 +0100
@@ -0,0 +1,293 @@
+/* Title: Pure/Admin/components.scala
+ Author: Makarius
+
+Isabelle system components.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Components
+{
+ /* archive name */
+
+ object Archive
+ {
+ val suffix: String = ".tar.gz"
+
+ def apply(name: String): String =
+ if (name == "") error("Bad component name: " + quote(name))
+ else name + suffix
+
+ def unapply(archive: String): Option[String] =
+ {
+ for {
+ name0 <- Library.try_unsuffix(suffix, archive)
+ name <- proper_string(name0)
+ } yield name
+ }
+
+ def get_name(archive: String): String =
+ unapply(archive) getOrElse
+ error("Bad component archive name (expecting .tar.gz): " + quote(archive))
+ }
+
+
+ /* component collections */
+
+ def admin(dir: Path): Path = dir + Path.explode("Admin/components")
+
+ def contrib(dir: Path = Path.current, name: String = ""): Path =
+ dir + Path.explode("contrib") + Path.explode(name)
+
+ def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
+ {
+ val name = Archive.get_name(archive.file_name)
+ progress.echo("Unpacking " + name)
+ Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ name
+ }
+
+ def resolve(base_dir: Path, names: List[String],
+ target_dir: Option[Path] = None,
+ progress: Progress = No_Progress)
+ {
+ Isabelle_System.mkdirs(base_dir)
+ for (name <- names) {
+ val archive_name = Archive(name)
+ val archive = base_dir + Path.explode(archive_name)
+ if (!archive.is_file) {
+ val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
+ progress.echo("Getting " + remote)
+ Bytes.write(archive, Url.read_bytes(Url(remote)))
+ }
+ unpack(target_dir getOrElse base_dir, archive, progress = progress)
+ }
+ }
+
+ def purge(dir: Path, platform: Platform.Family.Value)
+ {
+ def purge_platforms(platforms: String*): Set[String] =
+ platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
+ val purge_set =
+ platform match {
+ case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
+ case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
+ case Platform.Family.windows => purge_platforms("linux", "darwin")
+ }
+
+ File.find_files(dir.file,
+ (file: JFile) => file.isDirectory && purge_set(file.getName),
+ include_dirs = true).foreach(Isabelle_System.rm_tree)
+ }
+
+
+ /* component directory content */
+
+ def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings")
+ def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components")
+
+ def check_dir(dir: Path): Boolean =
+ settings(dir).is_file || components(dir).is_file
+
+ def read_components(dir: Path): List[String] =
+ split_lines(File.read(components(dir))).filter(_.nonEmpty)
+
+ def write_components(dir: Path, lines: List[String]): Unit =
+ File.write(components(dir), terminate_lines(lines))
+
+
+ /* component repository content */
+
+ val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
+
+ sealed case class SHA1_Digest(sha1: String, file_name: String)
+ {
+ override def toString: String = sha1 + " " + file_name
+ }
+
+ def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
+ (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
+ Word.explode(line) match {
+ case Nil => None
+ case List(sha1, name) => Some(SHA1_Digest(sha1, name))
+ case _ => error("Bad components.sha1 entry: " + quote(line))
+ })
+
+ def write_components_sha1(entries: List[SHA1_Digest]) =
+ File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
+
+
+
+ /** build and publish components **/
+
+ def build_components(
+ options: Options,
+ components: List[Path],
+ progress: Progress = No_Progress,
+ publish: Boolean = false,
+ force: Boolean = false,
+ update_components_sha1: Boolean = false)
+ {
+ val archives: List[Path] =
+ for (path <- components) yield {
+ path.file_name match {
+ case Archive(_) => path
+ case name =>
+ if (!path.is_dir) error("Bad component directory: " + path)
+ else if (!check_dir(path)) {
+ error("Malformed component directory: " + path +
+ "\n (requires " + settings() + " or " + Components.components() + ")")
+ }
+ else {
+ val component_path = path.expand
+ val archive_dir = component_path.dir
+ val archive_name = Archive(name)
+
+ val archive = archive_dir + Path.explode(archive_name)
+ if (archive.is_file && !force) {
+ error("Component archive already exists: " + archive)
+ }
+
+ progress.echo("Packaging " + archive_name + " ...")
+ Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
+ dir = archive_dir).check
+
+ archive
+ }
+ }
+ }
+
+ if ((publish && archives.nonEmpty) || update_components_sha1) {
+ options.string("isabelle_components_server") match {
+ case SSH.Target(user, host) =>
+ using(SSH.open_session(options, host = host, user = user))(ssh =>
+ {
+ val components_dir = Path.explode(options.string("isabelle_components_dir"))
+ val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
+
+ for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
+ error("Bad remote directory: " + dir)
+ }
+
+ if (publish) {
+ for (archive <- archives) {
+ val archive_name = archive.file_name
+ val name = Archive.get_name(archive_name)
+ val remote_component = components_dir + archive.base
+ val remote_contrib = contrib_dir + Path.explode(name)
+
+ // component archive
+ if (ssh.is_file(remote_component) && !force) {
+ error("Remote component archive already exists: " + remote_component)
+ }
+ progress.echo("Uploading " + archive_name)
+ ssh.write_file(remote_component, archive)
+
+ // contrib directory
+ val is_standard_component =
+ Isabelle_System.with_tmp_dir("component")(tmp_dir =>
+ {
+ Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+ check_dir(tmp_dir + Path.explode(name))
+ })
+ if (is_standard_component) {
+ if (ssh.is_dir(remote_contrib)) {
+ if (force) ssh.rm_tree(remote_contrib)
+ else error("Remote component directory already exists: " + remote_contrib)
+ }
+ progress.echo("Unpacking remote " + archive_name)
+ ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
+ ssh.bash_path(remote_component)).check
+ }
+ else {
+ progress.echo_warning("No unpacking of non-standard component: " + archive_name)
+ }
+ }
+ }
+
+ // remote SHA1 digests
+ if (update_components_sha1) {
+ val lines =
+ for {
+ entry <- ssh.read_dir(components_dir)
+ if entry.is_file && entry.name.endsWith(Archive.suffix)
+ }
+ yield {
+ progress.echo("Digesting remote " + entry.name)
+ Library.trim_line(
+ ssh.execute("cd " + ssh.bash_path(components_dir) +
+ "; sha1sum " + Bash.string(entry.name)).check.out)
+ }
+ write_components_sha1(read_components_sha1(lines))
+ }
+ })
+ case s => error("Bad isabelle_components_server: " + quote(s))
+ }
+ }
+
+ // local SHA1 digests
+ {
+ val new_entries =
+ for (archive <- archives)
+ yield {
+ val file_name = archive.file_name
+ progress.echo("Digesting local " + file_name)
+ val sha1 = SHA1.digest(archive).rep
+ SHA1_Digest(sha1, file_name)
+ }
+ val new_names = new_entries.map(_.file_name).toSet
+
+ write_components_sha1(
+ new_entries :::
+ read_components_sha1().filterNot(entry => new_names.contains(entry.file_name)))
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ private val relevant_options =
+ List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
+
+ val isabelle_tool =
+ Isabelle_Tool("build_components", "build and publish Isabelle components", args =>
+ {
+ var publish = false
+ var update_components_sha1 = false
+ var force = false
+ var options = Options.init()
+
+ def show_options: String =
+ cat_lines(relevant_options.map(name => options.options(name).print))
+
+ val getopts = Getopts("""
+Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
+
+ Options are:
+ -P publish on SSH server (see options below)
+ -f force: overwrite existing component archives and directories
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -u update all SHA1 keys in Isabelle repository Admin/components
+
+ Build and publish Isabelle components as .tar.gz archives on SSH server,
+ depending on system options:
+
+""" + Library.prefix_lines(" ", show_options) + "\n",
+ "P" -> (_ => publish = true),
+ "f" -> (_ => force = true),
+ "o:" -> (arg => options = options + arg),
+ "u" -> (_ => update_components_sha1 = true))
+
+ val more_args = getopts(args)
+ if (more_args.isEmpty && !update_components_sha1) getopts.usage()
+
+ val progress = new Console_Progress
+
+ build_components(options, more_args.map(Path.explode), progress = progress,
+ publish = publish, force = force, update_components_sha1 = update_components_sha1)
+ })
+}
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 09 00:08:59 2018 +0100
@@ -75,8 +75,7 @@
val build_release =
Logger_Task("build_release", logger =>
{
- Isabelle_Devel.release_snapshot(logger.options,
- rev = get_rev(), afp_rev = get_afp_rev(), remote_mac = "macbroy30")
+ Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
})
--- a/src/Pure/Admin/isabelle_devel.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/Admin/isabelle_devel.scala Sun Dec 09 00:08:59 2018 +0100
@@ -54,15 +54,14 @@
options: Options,
rev: String = "",
afp_rev: String = "",
- parallel_jobs: Int = 1,
- remote_mac: String = "")
+ parallel_jobs: Int = 1)
{
Isabelle_System.with_tmp_dir("isadist")(base_dir =>
{
Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
website_dir =>
Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev,
- parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir)))
+ parallel_jobs = parallel_jobs, website = Some(website_dir)))
})
}
--- a/src/Pure/General/file.ML Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/General/file.ML Sun Dec 09 00:08:59 2018 +0100
@@ -117,7 +117,7 @@
| SOME entry => read (f entry x));
in read a end);
-fun read_dir path = rev (fold_dir cons path []);
+fun read_dir path = sort_strings (fold_dir cons path []);
(* input *)
--- a/src/Pure/General/file.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/General/file.scala Sun Dec 09 00:08:59 2018 +0100
@@ -144,7 +144,7 @@
if (!dir.is_dir) error("No such directory: " + dir.toString)
val files = dir.file.listFiles
if (files == null) Nil
- else files.toList.map(_.getName)
+ else files.toList.map(_.getName).sorted
}
def find_files(
--- a/src/Pure/General/ssh.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/General/ssh.scala Sun Dec 09 00:08:59 2018 +0100
@@ -381,7 +381,7 @@
catch { case _: SftpException => false }
}
else attrs.isDir)
- }).toList
+ }).toList.sortBy(_.name)
}
def find_files(
--- a/src/Pure/System/components.scala Sat Dec 08 20:27:34 2018 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-/* Title: Pure/Admin/components.scala
- Author: Makarius
-
-Isabelle system components.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object Components
-{
- /* archive name */
-
- object Archive
- {
- val suffix: String = ".tar.gz"
- def apply(name: String): String = name + suffix
- def unapply(archive: String): Option[String] = Library.try_unsuffix(suffix, archive)
- def get_name(archive: String): String =
- unapply(archive) getOrElse
- error("Bad component archive name (expecting .tar.gz): " + quote(archive))
- }
-
-
- /* component collections */
-
- def admin(dir: Path): Path = dir + Path.explode("Admin/components")
-
- def contrib(dir: Path = Path.current, name: String = ""): Path =
- dir + Path.explode("contrib") + Path.explode(name)
-
- def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
- {
- val name = Archive.get_name(archive.file_name)
- progress.echo("Unpacking " + name)
- Isabelle_System.gnutar(
- "-C " + File.bash_path(dir) + " -xzf " + File.bash_path(archive.absolute)).check
- name
- }
-
- def resolve(base_dir: Path, names: List[String],
- target_dir: Option[Path] = None,
- progress: Progress = No_Progress)
- {
- Isabelle_System.mkdirs(base_dir)
- for (name <- names) {
- val archive_name = Archive(name)
- val archive = base_dir + Path.explode(archive_name)
- if (!archive.is_file) {
- val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
- progress.echo("Getting " + remote)
- Bytes.write(archive, Url.read_bytes(Url(remote)))
- }
- unpack(target_dir getOrElse base_dir, archive, progress = progress)
- }
- }
-
- def purge(dir: Path, platform: Platform.Family.Value)
- {
- def purge_platforms(platforms: String*): Set[String] =
- platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
- val purge_set =
- platform match {
- case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
- case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
- case Platform.Family.windows => purge_platforms("linux", "darwin")
- }
-
- File.find_files(dir.file,
- (file: JFile) => file.isDirectory && purge_set(file.getName),
- include_dirs = true).foreach(Isabelle_System.rm_tree)
- }
-
-
- /* component directory content */
-
- def settings(dir: Path): Path = dir + Path.explode("etc/settings")
- def components(dir: Path): Path = dir + Path.explode("etc/components")
-
- def check_dir(dir: Path): Boolean =
- settings(dir).is_file || components(dir).is_file
-
- def read_components(dir: Path): List[String] =
- split_lines(File.read(components(dir))).filter(_.nonEmpty)
-
- def write_components(dir: Path, lines: List[String]): Unit =
- File.write(components(dir), terminate_lines(lines))
-}
--- a/src/Pure/System/isabelle_system.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/System/isabelle_system.scala Sun Dec 09 00:08:59 2018 +0100
@@ -314,9 +314,17 @@
try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
catch { case ERROR(_) => false }
- def gnutar(args: String, cwd: JFile = null, redirect: Boolean = false): Process_Result =
+ def gnutar(
+ args: String,
+ dir: Path = Path.current,
+ original_owner: Boolean = false,
+ redirect: Boolean = false): Process_Result =
{
- if (gnutar_check) bash("tar " + args, cwd = cwd, redirect = redirect)
+ val options =
+ (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
+ (if (original_owner) "" else "--owner=root --group=staff ")
+
+ if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
--- a/src/Pure/System/isabelle_tool.scala Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/System/isabelle_tool.scala Sun Dec 09 00:08:59 2018 +0100
@@ -172,4 +172,5 @@
Build_PolyML.isabelle_tool2,
Build_Status.isabelle_tool,
Check_Sources.isabelle_tool,
+ Components.isabelle_tool,
isabelle.vscode.Build_VSCode.isabelle_tool)
--- a/src/Pure/build-jars Sat Dec 08 20:27:34 2018 +0000
+++ b/src/Pure/build-jars Sun Dec 09 00:08:59 2018 +0100
@@ -21,6 +21,7 @@
Admin/build_status.scala
Admin/check_sources.scala
Admin/ci_profile.scala
+ Admin/components.scala
Admin/isabelle_cronjob.scala
Admin/isabelle_devel.scala
Admin/jenkins.scala
@@ -112,7 +113,6 @@
ROOT.scala
System/bash.scala
System/command_line.scala
- System/components.scala
System/cygwin.scala
System/distribution.scala
System/getopts.scala