--- a/Admin/Windows/Cygwin/setup_server Mon Jan 23 14:34:07 2023 +0100
+++ b/Admin/Windows/Cygwin/setup_server Mon Jan 23 22:33:25 2023 +0100
@@ -15,7 +15,7 @@
local DIR="${2:-.}"
mkdir -p "$DIR" || fail "Cannot create directory: \"$DIR\""
echo "Downloading $URL ..."
- curl --fail --silent "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
+ curl --fail --silent --location "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
}
download "$CYGWIN_MAIN/setup-x86_64.exe"
--- a/lib/Tools/components Mon Jan 23 14:34:07 2023 +0100
+++ b/lib/Tools/components Mon Jan 23 22:33:25 2023 +0100
@@ -130,6 +130,7 @@
isabelle scala_build || exit $?
exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
else
+ source "$ISABELLE_HOME/lib/scripts/download_file"
for NAME in "${SELECTED_COMPONENTS[@]}"
do
BASE_NAME="$(basename "$NAME")"
@@ -144,30 +145,11 @@
echo "Skipping existing component \"$FULL_NAME\""
else
if [ ! -e "${FULL_NAME}.tar.gz" ]; then
- REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
- type -p curl > /dev/null || fail "Cannot download files: missing curl"
- echo "Getting \"$REMOTE\""
- mkdir -p "$(dirname "$FULL_NAME")"
-
- CURL_OPTIONS="--fail --silent --location"
- if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
- case $(sw_vers -productVersion) in
- 10.*)
- CURL_OPTIONS="$CURL_OPTIONS --insecure"
- ;;
- esac
- fi
- if curl $CURL_OPTIONS "$REMOTE" > "${FULL_NAME}.tar.gz.part"
- then
- mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
- else
- rm -f "${FULL_NAME}.tar.gz.part"
- fail "Failed to download \"$REMOTE\""
- fi
+ download_file "$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" "${FULL_NAME}.tar.gz" || exit $?
fi
if [ -e "${FULL_NAME}.tar.gz" ]; then
echo "Unpacking \"${FULL_NAME}.tar.gz\""
- tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
+ tar -C "$(dirname "$FULL_NAME")" -x -z -f "${FULL_NAME}.tar.gz" || exit 2
fi
fi
done
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/download_file Mon Jan 23 22:33:25 2023 +0100
@@ -0,0 +1,40 @@
+# -*- shell-script -*- :mode=shellscript:
+#
+# Bash function to download file via "curl".
+
+function download_file ()
+{
+ [ "$#" -ne 2 ] && {
+ echo "Bad arguments for download_file" >&2
+ return 2
+ }
+ local REMOTE="$1"
+ local LOCAL="$2"
+
+ type -p curl > /dev/null || {
+ echo "Require \"curl\" to download files" >&2
+ return 2
+ }
+
+ local CURL_OPTIONS="--fail --silent --location"
+ if [ "$(uname -s)" = "Darwin" ]
+ then
+ case $(sw_vers -productVersion) in
+ 10.*)
+ CURL_OPTIONS="$CURL_OPTIONS --insecure"
+ ;;
+ esac
+ fi
+
+ echo "Getting \"$REMOTE\""
+ mkdir -p "$(dirname "$LOCAL")"
+
+ if curl $CURL_OPTIONS "$REMOTE" > "${LOCAL}.part"
+ then
+ mv -f "${LOCAL}.part" "$LOCAL"
+ else
+ rm -f "${LOCAL}.part"
+ echo "Failed to download \"$REMOTE\"" >&2
+ return 2
+ fi
+}
--- a/src/Pure/Admin/build_history.scala Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Admin/build_history.scala Mon Jan 23 22:33:25 2023 +0100
@@ -191,7 +191,7 @@
other_isabelle.init_components(
component_repository = component_repository,
components_base = components_base,
- catalogs = List("main", "optional"))
+ catalogs = Components.optional_catalogs)
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
val ml_platform =
@@ -212,7 +212,7 @@
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
}
other_isabelle.bash(
- "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
+ "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty")) + ":$PATH\" " +
"bin/isabelle jedit -b", redirect = true, echo = verbose).check
for {
--- a/src/Pure/Admin/build_release.scala Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Admin/build_release.scala Mon Jan 23 22:33:25 2023 +0100
@@ -467,8 +467,7 @@
val other_isabelle = context.other_isabelle(context.dist_dir)
other_isabelle.init_settings(
- other_isabelle.init_components(
- components_base = context.components_base, catalogs = List("main")))
+ other_isabelle.init_components(components_base = context.components_base))
other_isabelle.resolve_components(echo = true)
try {
--- a/src/Pure/Admin/other_isabelle.scala Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Mon Jan 23 22:33:25 2023 +0100
@@ -8,11 +8,14 @@
object Other_Isabelle {
- def apply(isabelle_home: Path,
- isabelle_identifier: String = "",
- user_home: Path = Path.USER_HOME,
- progress: Progress = new Progress): Other_Isabelle =
+ def apply(
+ isabelle_home: Path,
+ isabelle_identifier: String = "",
+ user_home: Path = Path.USER_HOME,
+ progress: Progress = new Progress
+ ): Other_Isabelle = {
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
+ }
}
final class Other_Isabelle private(
@@ -65,7 +68,7 @@
def init_components(
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
- catalogs: List[String] = Nil,
+ catalogs: List[String] = Components.default_catalogs,
components: List[String] = Nil
): List[String] = {
val dir = Components.admin(isabelle_home)
--- a/src/Pure/General/ssh.scala Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/General/ssh.scala Mon Jan 23 22:33:25 2023 +0100
@@ -190,6 +190,19 @@
progress_stderr = progress_stderr, strict = strict)
}
+ override def download_file(
+ url_name: String,
+ file: Path,
+ progress: Progress = new Progress
+ ): Unit = {
+ val cmd_line =
+ File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
+ "download_file " + Bash.string(url_name) + " " + bash_path(file)
+ execute(cmd_line,
+ progress_stdout = progress.echo,
+ progress_stderr = progress.echo).check
+ }
+
override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
@@ -213,6 +226,14 @@
path
}
+ override def copy_file(src: Path, dst: Path): Unit = {
+ val direct = if (is_dir(dst)) "/." else ""
+ if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) {
+ error("Failed to copy file " + expand_path(src) + " to " +
+ expand_path(dst) + " (ssh " + toString + ")")
+ }
+ }
+
def read_dir(path: Path): List[String] =
run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s =>
if (s == "." || s == "..") None
@@ -339,6 +360,7 @@
def is_file(path: Path): Boolean = path.is_file
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
+ def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
def read_bytes(path: Path): Bytes = Bytes.read(path)
@@ -355,6 +377,9 @@
env = if (settings) Isabelle_System.settings() else null,
strict = strict)
+ def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+ Isabelle_System.download_file(url_name, file, progress = progress)
+
def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
}
--- a/src/Pure/System/components.scala Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/System/components.scala Mon Jan 23 22:33:25 2023 +0100
@@ -40,36 +40,51 @@
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+ val default_catalogs: List[String] = List("main")
+ val optional_catalogs: List[String] = List("main", "optional")
+
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 = new Progress): String = {
+ def unpack(
+ dir: Path,
+ archive: Path,
+ ssh: SSH.System = SSH.Local,
+ progress: Progress = new Progress
+ ): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
- Isabelle_System.extract(archive, dir)
+ ssh.execute(
+ "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive),
+ progress_stdout = progress.echo,
+ progress_stderr = progress.echo).check
name
}
- def resolve(base_dir: Path, names: List[String],
+ def resolve(
+ base_dir: Path,
+ names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
+ component_repository: String = Components.default_component_repository,
+ ssh: SSH.System = SSH.Local,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.make_directory(base_dir)
+ ssh.make_directory(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
- if (!archive.is_file) {
- val remote = Components.default_component_repository + "/" + archive_name
- Isabelle_System.download_file(remote, archive, progress = progress)
+ if (!ssh.is_file(archive)) {
+ val remote = Url.append_path(component_repository, archive_name)
+ ssh.download_file(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
- Isabelle_System.make_directory(dir)
- Isabelle_System.copy_file(archive, dir)
+ ssh.make_directory(dir)
+ ssh.copy_file(archive, dir)
}
- unpack(target_dir getOrElse base_dir, archive, progress = progress)
+ unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
}
}
--- a/src/Pure/Tools/build_docker.scala Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Tools/build_docker.scala Mon Jan 23 22:33:25 2023 +0100
@@ -68,7 +68,7 @@
# Isabelle
WORKDIR /home/isabelle
""" + (if (is_remote)
- "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
+ "RUN curl --fail --silent --location " + Bash.string(app_archive) + " > Isabelle.tar.gz"
else "COPY Isabelle.tar.gz .") + """
RUN tar xzf Isabelle.tar.gz && \
mv """ + isabelle_name + """ Isabelle && \