# HG changeset patch # User wenzelm # Date 1612876383 -3600 # Node ID 3e963d68d394aca8ba91d3fa71ab9dae4c4bf07c # Parent 27dc8f8991478b5c3dc4cb9d9ce7b3b477ac3858 more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history; diff -r 27dc8f899147 -r 3e963d68d394 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Tue Feb 09 14:03:05 2021 +0100 +++ b/src/Pure/Admin/build_history.scala Tue Feb 09 14:13:03 2021 +0100 @@ -107,6 +107,7 @@ afp_partition: Int = 0, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, + component_repository: String = Components.default_component_repository, components_base: Path = Components.default_components_base, fresh: Boolean = false, hostname: String = "", @@ -187,7 +188,9 @@ val component_settings = other_isabelle.init_components( - components_base = components_base, catalogs = List("main", "optional")) + component_repository = component_repository, + components_base = components_base, + catalogs = List("main", "optional")) other_isabelle.init_settings(component_settings ::: init_settings) other_isabelle.resolve_components(verbose) val ml_platform = @@ -407,6 +410,7 @@ var multicore_list = List(default_multicore) var isabelle_identifier = default_isabelle_identifier var afp_partition = 0 + var component_repository = Components.default_component_repository var more_settings: List[String] = Nil var more_preferences: List[String] = Nil var fresh = false @@ -434,6 +438,8 @@ -M MULTICORE multicore configurations (see below) -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """) -P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted) + -R URL remote repository for Isabelle components (default: """ + + Components.default_component_repository + """) -U SIZE maximal ML heap in MB (default: unbounded) -e TEXT additional text for generated etc/settings -f fresh build of Isabelle/Scala components (recommended) @@ -462,6 +468,7 @@ "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)), "N:" -> (arg => isabelle_identifier = arg), "P:" -> (arg => afp_partition = Value.Int.parse(arg)), + "R:" -> (arg => component_repository = arg), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), @@ -495,8 +502,9 @@ build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev, afp_rev = afp_rev, afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, - components_base = components_base, fresh = fresh, hostname = hostname, - multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, + component_repository = component_repository, components_base = components_base, + fresh = fresh, hostname = hostname, multicore_base = multicore_base, + multicore_list = multicore_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, init_settings = init_settings, more_settings = more_settings, more_preferences = more_preferences, verbose = verbose, build_tags = build_tags, diff -r 27dc8f899147 -r 3e963d68d394 src/Pure/Admin/components.scala --- a/src/Pure/Admin/components.scala Tue Feb 09 14:03:05 2021 +0100 +++ b/src/Pure/Admin/components.scala Tue Feb 09 14:13:03 2021 +0100 @@ -38,6 +38,9 @@ /* component collections */ + def default_component_repository: String = + Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") def admin(dir: Path): Path = dir + Path.explode("Admin/components") @@ -63,7 +66,7 @@ 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 + val remote = Components.default_component_repository + "/" + archive_name progress.echo("Getting " + remote) Bytes.write(archive, Url.read_bytes(Url(remote))) } diff -r 27dc8f899147 -r 3e963d68d394 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue Feb 09 14:03:05 2021 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Feb 09 14:13:03 2021 +0100 @@ -93,6 +93,7 @@ /* integrity test of build_history vs. build_history_base */ def build_history_options0: String = + " -R " + Bash.string(Components.default_component_repository) + " -C '$USER_HOME/.isabelle/contrib' -f " val build_history_base: Logger_Task = diff -r 27dc8f899147 -r 3e963d68d394 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Tue Feb 09 14:03:05 2021 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Tue Feb 09 14:13:03 2021 +0100 @@ -69,11 +69,14 @@ /* components */ def init_components( + component_repository: String = Components.default_component_repository, components_base: Path = Components.default_components_base, catalogs: List[String] = Nil, components: List[String] = Nil): List[String] = { val dir = Components.admin(isabelle_home) + + ("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) :: catalogs.map(name => "init_components " + File.bash_path(components_base) + " " + File.bash_path(dir + Path.basic(name))) :::