Thu, 09 Nov 2023 17:58:21 +0100 |
Fabian Huch |
use only finished sessions in timing data;
|
file |
diff |
annotate
|
Thu, 09 Nov 2023 16:39:36 +0100 |
Fabian Huch |
tuned;
|
file |
diff |
annotate
|
Thu, 09 Nov 2023 15:45:51 +0100 |
Fabian Huch |
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
|
file |
diff |
annotate
|
Thu, 09 Nov 2023 11:49:08 +0100 |
Fabian Huch |
performance tuning for build schedule: faster stopping;
|
file |
diff |
annotate
|
Thu, 09 Nov 2023 11:41:19 +0100 |
Fabian Huch |
performance tuning for timing heuristic: pre-calculate graph operations;
|
file |
diff |
annotate
|
Wed, 08 Nov 2023 11:08:03 +0100 |
Fabian Huch |
move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
|
file |
diff |
annotate
|
Fri, 03 Nov 2023 10:30:51 +0100 |
wenzelm |
prefer Time.scale(), following Isabelle/ML;
|
file |
diff |
annotate
|
Fri, 03 Nov 2023 10:03:05 +0100 |
Fabian Huch |
improved build messages;
|
file |
diff |
annotate
|
Thu, 26 Oct 2023 22:10:22 +0200 |
wenzelm |
more robust init_database();
|
file |
diff |
annotate
|
Thu, 26 Oct 2023 15:38:27 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
Thu, 26 Oct 2023 11:50:50 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
Wed, 18 Oct 2023 20:51:24 +0200 |
Fabian Huch |
add module for faster scheduled builds;
|
file |
diff |
annotate
|