more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
authorwenzelm
Tue, 09 Feb 2021 14:13:03 +0100
changeset 73486 3e963d68d394
parent 73485 27dc8f899147
child 73487 62b6bc153b84
child 73536 f6f1242ed367
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
src/Pure/Admin/build_history.scala
src/Pure/Admin/components.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/other_isabelle.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,
--- 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))) :::