src/Pure/Tools/build_schedule.scala
Wed, 22 Nov 2023 15:46:58 +0100 Fabian Huch properly incorporate running tasks into timing heuristic;
Wed, 22 Nov 2023 15:39:39 +0100 Fabian Huch clarified ready vs. next ready;
Wed, 22 Nov 2023 15:04:29 +0100 Fabian Huch introduced path heuristic abstraction;
Mon, 13 Nov 2023 18:08:05 +0100 Fabian Huch tuned message;
Mon, 13 Nov 2023 17:48:11 +0100 Fabian Huch better invalidation for schedule cache (only on relevant changes);
Mon, 13 Nov 2023 17:31:37 +0100 Fabian Huch tuned;
Mon, 13 Nov 2023 17:25:26 +0100 Fabian Huch timing heuristic: parallelize more aggressively to utilize hosts fully;
Mon, 13 Nov 2023 17:00:13 +0100 Fabian Huch proper parallel paths for timing heuristic;
Mon, 13 Nov 2023 16:16:52 +0100 Fabian Huch scheduled build: allocate cpus more aggressively, to avoid idle threads;
Fri, 10 Nov 2023 14:52:13 +0100 Fabian Huch finalize scheduled build only on master node;
Fri, 10 Nov 2023 14:42:07 +0100 Fabian Huch finalize current sessions before generating schedule;
Fri, 10 Nov 2023 14:07:36 +0100 Fabian Huch clarified signature: more operations;
Thu, 09 Nov 2023 19:06:50 +0100 Fabian Huch proper dummy timing entries;
Thu, 09 Nov 2023 17:58:21 +0100 Fabian Huch use only finished sessions in timing data;
Thu, 09 Nov 2023 16:39:36 +0100 Fabian Huch tuned;
Thu, 09 Nov 2023 15:45:51 +0100 Fabian Huch performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Thu, 09 Nov 2023 11:49:08 +0100 Fabian Huch performance tuning for build schedule: faster stopping;
Thu, 09 Nov 2023 11:41:19 +0100 Fabian Huch performance tuning for timing heuristic: pre-calculate graph operations;
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);
Fri, 03 Nov 2023 10:30:51 +0100 wenzelm prefer Time.scale(), following Isabelle/ML;
Fri, 03 Nov 2023 10:03:05 +0100 Fabian Huch improved build messages;
Thu, 26 Oct 2023 22:10:22 +0200 wenzelm more robust init_database();
Thu, 26 Oct 2023 15:38:27 +0200 wenzelm clarified names;
Thu, 26 Oct 2023 11:50:50 +0200 wenzelm tuned imports;
Wed, 18 Oct 2023 20:51:24 +0200 Fabian Huch add module for faster scheduled builds;
less more (0) tip