clarified defaults (see also b310b93563f6);
authorwenzelm
Tue, 24 Jan 2023 20:43:55 +0100
changeset 77083 092449efcb0e
parent 77082 4e724a439035
child 77084 f9a858060836
clarified defaults (see also b310b93563f6);
src/Pure/Admin/build_history.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/System/components.scala
--- a/src/Pure/Admin/build_history.scala	Tue Jan 24 20:39:11 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Tue Jan 24 20:43:55 2023 +0100
@@ -104,7 +104,6 @@
     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 = "",
     multicore_base: Boolean = false,
@@ -187,7 +186,7 @@
       val component_settings =
         other_isabelle.init_components(
           component_repository = component_repository,
-          components_base = components_base,
+          components_base = Components.standard_components_base,
           catalogs = Components.optional_catalogs)
       other_isabelle.init_settings(component_settings ::: init_settings)
       other_isabelle.resolve_components(echo = verbose)
@@ -394,7 +393,6 @@
     Command_Line.tool {
       var afp = false
       var multicore_base = false
-      var components_base: Path = Components.default_components_base
       var heap: Option[Int] = None
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
@@ -419,8 +417,6 @@
   Options are:
     -A           include $ISABELLE_HOME/AFP directory
     -B           first multicore build serves as base for scheduling information
-    -C DIR       base directory for Isabelle components (default: """ +
-      Components.default_components_base + """)
     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
       default_heap * 2 + """ for x86_64)
     -M MULTICORE multicore configurations (see below)
@@ -450,7 +446,6 @@
 """,
         "A" -> (_ => afp = true),
         "B" -> (_ => multicore_base = true),
-        "C:" -> (arg => components_base = Path.explode(arg)),
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
         "N:" -> (arg => isabelle_identifier = arg),
@@ -487,7 +482,7 @@
         local_build(Options.init(), root, progress = progress,
           afp = afp, afp_partition = afp_partition,
           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
-          component_repository = component_repository, components_base = components_base,
+          component_repository = component_repository,
           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),
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Jan 24 20:39:11 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Jan 24 20:43:55 2023 +0100
@@ -410,8 +410,7 @@
               options =
                 " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
                 " -R " + Bash.string(Components.default_component_repository) +
-                " -C '$USER_HOME/.isabelle/contrib' -f " +
-                r.build_history_options,
+                " -f " + r.build_history_options,
               args = "-o timeout=10800 " + r.args)
 
           for ((log_name, bytes) <- results) {
--- a/src/Pure/System/components.scala	Tue Jan 24 20:39:11 2023 +0100
+++ b/src/Pure/System/components.scala	Tue Jan 24 20:43:55 2023 +0100
@@ -39,6 +39,7 @@
     Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
 
   val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+  val standard_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib")
 
   val default_catalogs: List[String] = List("main")
   val optional_catalogs: List[String] = List("main", "optional")