Sun, 10 Dec 2023 12:54:52 +0100 wenzelm tuned;
Sun, 10 Dec 2023 12:54:31 +0100 wenzelm tuned;
Sun, 10 Dec 2023 12:18:22 +0100 wenzelm clarified modules;
Sun, 10 Dec 2023 11:56:56 +0100 wenzelm clarified ML;
Sun, 10 Dec 2023 11:42:57 +0100 wenzelm clarified signature;
Sun, 10 Dec 2023 11:24:42 +0100 wenzelm tuned signature;
Sat, 09 Dec 2023 21:48:50 +0100 wenzelm avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);
Sat, 09 Dec 2023 21:25:26 +0100 wenzelm tuned;
Sat, 09 Dec 2023 21:15:12 +0100 wenzelm more robust: proper Proofterm.get_proofs_level with bound check;
Sat, 09 Dec 2023 20:50:21 +0100 wenzelm tuned;
Sat, 09 Dec 2023 20:37:36 +0100 wenzelm clarified signature: fewer tuples;
Sat, 09 Dec 2023 20:05:13 +0100 wenzelm clarified signature: fewer tuples;
Sat, 09 Dec 2023 17:31:10 +0100 wenzelm clarified signature: more explicit get_proofs_level with bounds check;
Fri, 08 Dec 2023 20:56:21 +0100 wenzelm merged
Fri, 08 Dec 2023 20:47:03 +0100 wenzelm misc tuning and clarification: more standard Same.commit discipline;
Fri, 08 Dec 2023 20:08:52 +0100 wenzelm tuned;
Fri, 08 Dec 2023 19:52:24 +0100 wenzelm tuned names;
Fri, 08 Dec 2023 19:29:05 +0100 wenzelm more operations;
Fri, 08 Dec 2023 19:00:46 +0100 wenzelm minor performance tuning: more careful treatment of empty environment;
Fri, 08 Dec 2023 18:51:18 +0100 wenzelm clarified signature;
Fri, 08 Dec 2023 18:40:31 +0100 wenzelm more zproofs;
Fri, 08 Dec 2023 18:39:58 +0100 wenzelm clarified signature: support shared cache;
Fri, 08 Dec 2023 16:01:42 +0100 wenzelm tuned;
Fri, 08 Dec 2023 15:58:08 +0100 wenzelm tuned: avoid shadowing;
Fri, 08 Dec 2023 15:37:46 +0100 wenzelm more zproofs;
Fri, 08 Dec 2023 15:30:53 +0100 wenzelm tuned;
Fri, 08 Dec 2023 15:13:18 +0100 wenzelm more operations;
Fri, 08 Dec 2023 14:59:22 +0100 wenzelm tuned signature;
Fri, 08 Dec 2023 14:55:43 +0100 wenzelm tuned names;
Fri, 08 Dec 2023 14:48:17 +0100 wenzelm tuned -- eliminate clones;
Fri, 08 Dec 2023 14:35:24 +0100 wenzelm tuned;
Fri, 08 Dec 2023 14:27:42 +0100 wenzelm more operations;
Fri, 08 Dec 2023 13:36:47 +0100 wenzelm more operations;
Fri, 08 Dec 2023 13:09:39 +0100 wenzelm tuned;
Fri, 08 Dec 2023 12:10:53 +0100 wenzelm clarified signature;
Fri, 08 Dec 2023 12:05:56 +0100 wenzelm tuned;
Fri, 08 Dec 2023 11:46:42 +0100 wenzelm tuned;
Fri, 08 Dec 2023 19:36:27 +0100 Fabian Huch consider schedule calculation time in estimation;
Fri, 08 Dec 2023 18:56:19 +0100 Fabian Huch compare previous build schedule with new one, to prevent regressions;
Fri, 08 Dec 2023 17:16:41 +0100 Fabian Huch clarified: build schedules may be outdated when empty, after some time, or due to build progress;
Fri, 08 Dec 2023 17:00:13 +0100 Fabian Huch store previous build jobs in graph so schedules can be used later in the build process;
Fri, 08 Dec 2023 15:21:51 +0100 Fabian Huch add serial for build schedule to avoid unnecessary db read/writes;
Thu, 07 Dec 2023 13:57:48 +0100 Fabian Huch tuned;
Thu, 07 Dec 2023 13:53:54 +0100 Fabian Huch clarified;
Fri, 08 Dec 2023 12:11:22 +0100 Fabian Huch tuned;
Thu, 07 Dec 2023 11:34:01 +0100 Fabian Huch use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent);
Thu, 07 Dec 2023 11:28:12 +0100 Fabian Huch add build uuid to schedule;
Wed, 06 Dec 2023 21:24:00 +0100 Fabian Huch tuned;
Wed, 06 Dec 2023 20:04:47 +0100 Fabian Huch use schedule directly instead of extra cache;
Wed, 06 Dec 2023 18:28:15 +0100 Fabian Huch added build schedule command-line wrapper;
Wed, 06 Dec 2023 18:18:56 +0100 Fabian Huch added graphical representation of build schedules;
Wed, 06 Dec 2023 17:55:30 +0100 Fabian Huch clarified build heuristics parameters;
Wed, 06 Dec 2023 17:44:51 +0100 Fabian Huch proper parallel paths: factor in elapsed time;
Wed, 06 Dec 2023 17:42:04 +0100 Fabian Huch performance tuning: cache estimates;
Thu, 07 Dec 2023 15:56:54 +0100 wenzelm misc tuning and clarification;
Thu, 07 Dec 2023 15:25:29 +0100 wenzelm tuned;
Thu, 07 Dec 2023 14:48:58 +0100 wenzelm misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars;
Thu, 07 Dec 2023 13:05:34 +0100 wenzelm tuned;
Thu, 07 Dec 2023 13:04:48 +0100 wenzelm tuned;
Thu, 07 Dec 2023 12:12:13 +0100 wenzelm minor performance tuning: regular Same.operation;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 tip