467 override def toString: String = rc.toString |
467 override def toString: String = rc.toString |
468 } |
468 } |
469 |
469 |
470 def build( |
470 def build( |
471 options: Options, |
471 options: Options, |
|
472 selection: Sessions.Selection, |
472 progress: Progress = new Progress, |
473 progress: Progress = new Progress, |
473 check_unknown_files: Boolean = false, |
474 check_unknown_files: Boolean = false, |
474 build_heap: Boolean = false, |
475 build_heap: Boolean = false, |
475 clean_build: Boolean = false, |
476 clean_build: Boolean = false, |
476 dirs: List[Path] = Nil, |
477 dirs: List[Path] = Nil, |
482 check_keywords: Set[String] = Set.empty, |
483 check_keywords: Set[String] = Set.empty, |
483 fresh_build: Boolean = false, |
484 fresh_build: Boolean = false, |
484 no_build: Boolean = false, |
485 no_build: Boolean = false, |
485 soft_build: Boolean = false, |
486 soft_build: Boolean = false, |
486 verbose: Boolean = false, |
487 verbose: Boolean = false, |
487 export_files: Boolean = false, |
488 export_files: Boolean = false): Results = |
488 requirements: Boolean = false, |
|
489 all_sessions: Boolean = false, |
|
490 base_sessions: List[String] = Nil, |
|
491 exclude_session_groups: List[String] = Nil, |
|
492 exclude_sessions: List[String] = Nil, |
|
493 session_groups: List[String] = Nil, |
|
494 sessions: List[String] = Nil, |
|
495 selection: Sessions.Selection = Sessions.Selection.empty): Results = |
|
496 { |
489 { |
497 val build_options = |
490 val build_options = |
498 options + |
491 options + |
499 "ML_statistics" + |
492 "ML_statistics" + |
500 "completion_limit=0" + |
493 "completion_limit=0" + |
518 deps.sources(session_name) ::: |
511 deps.sources(session_name) ::: |
519 deps.imported_sources(session_name) |
512 deps.imported_sources(session_name) |
520 SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString |
513 SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString |
521 } |
514 } |
522 |
515 |
523 val selection1 = |
|
524 Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, |
|
525 exclude_sessions, session_groups, sessions) ++ selection |
|
526 |
|
527 val deps = |
516 val deps = |
528 { |
517 { |
529 val deps0 = |
518 val deps0 = |
530 Sessions.deps(full_sessions.selection(selection1), |
519 Sessions.deps(full_sessions.selection(selection), |
531 progress = progress, inlined_files = true, verbose = verbose, |
520 progress = progress, inlined_files = true, verbose = verbose, |
532 list_files = list_files, check_keywords = check_keywords).check_errors |
521 list_files = list_files, check_keywords = check_keywords).check_errors |
533 |
522 |
534 if (soft_build && !fresh_build) { |
523 if (soft_build && !fresh_build) { |
535 val outdated = |
524 val outdated = |
575 val queue = Queue(progress, deps.sessions_structure, store) |
564 val queue = Queue(progress, deps.sessions_structure, store) |
576 |
565 |
577 store.prepare_output_dir() |
566 store.prepare_output_dir() |
578 |
567 |
579 if (clean_build) { |
568 if (clean_build) { |
580 for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) { |
569 for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) { |
581 val (relevant, ok) = store.clean_output(name) |
570 val (relevant, ok) = store.clean_output(name) |
582 if (relevant) { |
571 if (relevant) { |
583 if (ok) progress.echo("Cleaned " + name) |
572 if (ok) progress.echo("Cleaned " + name) |
584 else progress.echo(name + " FAILED to clean") |
573 else progress.echo(name + " FAILED to clean") |
585 } |
574 } |
763 new Results( |
752 new Results( |
764 (for ((name, result) <- results0.iterator) |
753 (for ((name, result) <- results0.iterator) |
765 yield (name, (result.process, result.info))).toMap) |
754 yield (name, (result.process, result.info))).toMap) |
766 |
755 |
767 if (export_files) { |
756 if (export_files) { |
768 for (name <- full_sessions.imports_selection(selection1).iterator if results(name).ok) { |
757 for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) { |
769 val info = results.info(name) |
758 val info = results.info(name) |
770 if (info.export_files.nonEmpty) { |
759 if (info.export_files.nonEmpty) { |
771 progress.echo("Exporting " + info.name + " ...") |
760 progress.echo("Exporting " + info.name + " ...") |
772 for ((dir, prune, pats) <- info.export_files) { |
761 for ((dir, prune, pats) <- info.export_files) { |
773 Export.export_files(store, name, info.dir + dir, |
762 Export.export_files(store, name, info.dir + dir, |
901 } |
890 } |
902 |
891 |
903 val results = |
892 val results = |
904 progress.interrupt_handler { |
893 progress.interrupt_handler { |
905 build(options, |
894 build(options, |
|
895 Sessions.Selection( |
|
896 requirements = requirements, |
|
897 all_sessions = all_sessions, |
|
898 base_sessions = base_sessions, |
|
899 exclude_session_groups = exclude_session_groups, |
|
900 exclude_sessions = exclude_sessions, |
|
901 session_groups = session_groups, |
|
902 sessions = sessions), |
906 progress = progress, |
903 progress = progress, |
907 check_unknown_files = Mercurial.is_repository(Path.explode("~~")), |
904 check_unknown_files = Mercurial.is_repository(Path.explode("~~")), |
908 build_heap = build_heap, |
905 build_heap = build_heap, |
909 clean_build = clean_build, |
906 clean_build = clean_build, |
910 dirs = dirs, |
907 dirs = dirs, |
915 check_keywords = check_keywords, |
912 check_keywords = check_keywords, |
916 fresh_build = fresh_build, |
913 fresh_build = fresh_build, |
917 no_build = no_build, |
914 no_build = no_build, |
918 soft_build = soft_build, |
915 soft_build = soft_build, |
919 verbose = verbose, |
916 verbose = verbose, |
920 export_files = export_files, |
917 export_files = export_files) |
921 requirements = requirements, |
|
922 all_sessions = all_sessions, |
|
923 base_sessions = base_sessions, |
|
924 exclude_session_groups = exclude_session_groups, |
|
925 exclude_sessions = exclude_sessions, |
|
926 session_groups = session_groups, |
|
927 sessions = sessions) |
|
928 } |
918 } |
929 val end_date = Date.now() |
919 val end_date = Date.now() |
930 val elapsed_time = end_date.time - start_date.time |
920 val elapsed_time = end_date.time - start_date.time |
931 |
921 |
932 if (verbose) { |
922 if (verbose) { |
949 build_heap: Boolean = false, |
939 build_heap: Boolean = false, |
950 dirs: List[Path] = Nil, |
940 dirs: List[Path] = Nil, |
951 fresh: Boolean = false, |
941 fresh: Boolean = false, |
952 strict: Boolean = false): Int = |
942 strict: Boolean = false): Int = |
953 { |
943 { |
|
944 val selection = Sessions.Selection.session(logic) |
954 val rc = |
945 val rc = |
955 if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs, |
946 if (!fresh && |
956 sessions = List(logic)).ok) 0 |
947 build(options, selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 |
957 else { |
948 else { |
958 progress.echo("Build started for Isabelle/" + logic + " ...") |
949 progress.echo("Build started for Isabelle/" + logic + " ...") |
959 Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh, |
950 Build.build(options, selection, progress = progress, build_heap = build_heap, |
960 dirs = dirs, sessions = List(logic)).rc |
951 fresh_build = fresh, dirs = dirs).rc |
961 } |
952 } |
962 |
|
963 if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc |
953 if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc |
964 } |
954 } |
965 } |
955 } |