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 |