more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
--- 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,
--- 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)))
}
--- 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 =
--- 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))) :::