src/Pure/Admin/build_history.scala
changeset 69387 ff9095c91e87
parent 69366 b6dacf6eabe3
child 69388 fc58534bc475
equal deleted inserted replaced
69386:7bcad752857d 69387:ff9095c91e87
   113     isabelle_identifier: String = default_isabelle_identifier,
   113     isabelle_identifier: String = default_isabelle_identifier,
   114     ml_statistics_step: Int = 1,
   114     ml_statistics_step: Int = 1,
   115     components_base: String = "",
   115     components_base: String = "",
   116     fresh: Boolean = false,
   116     fresh: Boolean = false,
   117     hostname: String = "",
   117     hostname: String = "",
   118     nonfree: Boolean = false,
       
   119     multicore_base: Boolean = false,
   118     multicore_base: Boolean = false,
   120     multicore_list: List[(Int, Int)] = List(default_multicore),
   119     multicore_list: List[(Int, Int)] = List(default_multicore),
   121     arch_64: Boolean = false,
   120     arch_64: Boolean = false,
   122     heap: Int = default_heap,
   121     heap: Int = default_heap,
   123     max_heap: Option[Int] = None,
   122     max_heap: Option[Int] = None,
   184     var first_build = true
   183     var first_build = true
   185     for ((threads, processes) <- multicore_list) yield
   184     for ((threads, processes) <- multicore_list) yield
   186     {
   185     {
   187       /* init settings */
   186       /* init settings */
   188 
   187 
   189       other_isabelle.init_settings(components_base, nonfree, init_settings)
   188       other_isabelle.init_settings(components_base, init_settings)
   190       other_isabelle.resolve_components(verbose)
   189       other_isabelle.resolve_components(verbose)
   191       val ml_platform =
   190       val ml_platform =
   192         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
   191         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
   193 
   192 
   194       val isabelle_output =
   193       val isabelle_output =
   404       var more_settings: List[String] = Nil
   403       var more_settings: List[String] = Nil
   405       var fresh = false
   404       var fresh = false
   406       var hostname = ""
   405       var hostname = ""
   407       var init_settings: List[String] = Nil
   406       var init_settings: List[String] = Nil
   408       var arch_64 = false
   407       var arch_64 = false
   409       var nonfree = false
       
   410       var output_file = ""
   408       var output_file = ""
   411       var rev = default_rev
   409       var rev = default_rev
   412       var ml_statistics_step = 1
   410       var ml_statistics_step = 1
   413       var build_tags = List.empty[String]
   411       var build_tags = List.empty[String]
   414       var user_home = default_user_home
   412       var user_home = default_user_home
   431     -e TEXT      additional text for generated etc/settings
   429     -e TEXT      additional text for generated etc/settings
   432     -f           fresh build of Isabelle/Scala components (recommended)
   430     -f           fresh build of Isabelle/Scala components (recommended)
   433     -h NAME      override local hostname
   431     -h NAME      override local hostname
   434     -i TEXT      initial text for generated etc/settings
   432     -i TEXT      initial text for generated etc/settings
   435     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
   433     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
   436     -n           include nonfree components
       
   437     -o FILE      output file for log names (default: stdout)
   434     -o FILE      output file for log names (default: stdout)
   438     -r REV       update to revision (default: """ + default_rev + """)
   435     -r REV       update to revision (default: """ + default_rev + """)
   439     -s NUMBER    step size for ML statistics (0=none, 1=all, n=step, default: 1)
   436     -s NUMBER    step size for ML statistics (0=none, 1=all, n=step, default: 1)
   440     -t TAG       free-form build tag (multiple occurrences possible)
   437     -t TAG       free-form build tag (multiple occurrences possible)
   441     -u DIR       alternative USER_HOME directory
   438     -u DIR       alternative USER_HOME directory
   464           {
   461           {
   465             case "32" | "x86" => arch_64 = false
   462             case "32" | "x86" => arch_64 = false
   466             case "64" | "x86_64" => arch_64 = true
   463             case "64" | "x86_64" => arch_64 = true
   467             case bad => error("Bad processor architecture: " + quote(bad))
   464             case bad => error("Bad processor architecture: " + quote(bad))
   468           },
   465           },
   469         "n" -> (_ => nonfree = true),
       
   470         "o:" -> (arg => output_file = arg),
   466         "o:" -> (arg => output_file = arg),
   471         "r:" -> (arg => rev = arg),
   467         "r:" -> (arg => rev = arg),
   472         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
   468         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
   473         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
   469         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
   474         "u:" -> (arg => user_home = Path.explode(arg)),
   470         "u:" -> (arg => user_home = Path.explode(arg)),
   486 
   482 
   487       val results =
   483       val results =
   488         build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
   484         build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
   489           afp_rev = afp_rev, afp_partition = afp_partition,
   485           afp_rev = afp_rev, afp_partition = afp_partition,
   490           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
   486           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
   491           components_base = components_base, fresh = fresh, hostname = hostname, nonfree = nonfree,
   487           components_base = components_base, fresh = fresh, hostname = hostname,
   492           multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
   488           multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
   493           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   489           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   494           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
   490           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
   495           verbose = verbose, build_tags = build_tags, build_args = build_args)
   491           verbose = verbose, build_tags = build_tags, build_args = build_args)
   496 
   492