equal
deleted
inserted
replaced
57 results(session).timing |
57 results(session).timing |
58 } |
58 } |
59 (Timing.zero /: timings)(_ + _) |
59 (Timing.zero /: timings)(_ + _) |
60 } |
60 } |
61 |
61 |
|
62 private def with_documents(options: Options): Options = |
|
63 { |
|
64 if (documents) |
|
65 options |
|
66 .bool.update("browser_info", true) |
|
67 .string.update("document", "pdf") |
|
68 .string.update("document_variants", "document:outline=/proof,/ML") |
|
69 else |
|
70 options |
|
71 } |
|
72 |
62 |
73 |
63 final def hg_id(path: Path): String = |
74 final def hg_id(path: Path): String = |
64 Isabelle_System.hg("id -i", path.file).out |
75 Isabelle_System.hg("id -i", path.file).out |
65 |
76 |
66 final def print_section(title: String): Unit = |
77 final def print_section(title: String): Unit = |
78 Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt)))) |
89 Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt)))) |
79 val props = load_properties() |
90 val props = load_properties() |
80 System.getProperties().putAll(props) |
91 System.getProperties().putAll(props) |
81 |
92 |
82 val options = |
93 val options = |
83 Options.init() |
94 with_documents(Options.init()) |
84 .bool.update("browser_info", true) |
|
85 .string.update("document", "pdf") |
|
86 .string.update("document_variants", "document:outline=/proof,/ML") |
|
87 .int.update("parallel_proofs", 2) |
95 .int.update("parallel_proofs", 2) |
88 .int.update("threads", threads) |
96 .int.update("threads", threads) |
89 |
97 |
90 print_section("BUILD") |
98 print_section("BUILD") |
91 println(s"Build started at $start_time") |
99 println(s"Build started at $start_time") |
125 } |
133 } |
126 |
134 |
127 |
135 |
128 /* profile */ |
136 /* profile */ |
129 |
137 |
|
138 def documents: Boolean = true |
|
139 |
130 def threads: Int |
140 def threads: Int |
131 def jobs: Int |
141 def jobs: Int |
132 def include: List[Path] |
142 def include: List[Path] |
133 def select: List[Path] |
143 def select: List[Path] |
134 |
144 |