| Fri, 24 Nov 2023 11:31:15 +0100 |
wenzelm |
clarified signature: more general make_streams;
|
changeset |
files
|
| Fri, 24 Nov 2023 11:33:53 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 24 Nov 2023 11:10:31 +0100 |
wenzelm |
more robust exception handling (amending 8cc1ae43e12e);
|
changeset |
files
|
| Thu, 23 Nov 2023 11:40:49 +0100 |
wenzelm |
clarified signature: avoid deprecated URL constructors;
|
changeset |
files
|
| Thu, 23 Nov 2023 11:36:38 +0100 |
wenzelm |
avoid deprecated URL constructors;
|
changeset |
files
|
| Fri, 24 Nov 2023 21:49:52 +0100 |
Fabian Huch |
proper split;
|
changeset |
files
|
| Fri, 24 Nov 2023 17:52:04 +0100 |
Fabian Huch |
properly sort entries;
|
changeset |
files
|
| Fri, 24 Nov 2023 17:24:35 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Fri, 24 Nov 2023 17:24:22 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Fri, 24 Nov 2023 17:06:32 +0100 |
Fabian Huch |
better estimation for unknown jobs;
|
changeset |
files
|
| Fri, 24 Nov 2023 17:05:49 +0100 |
Fabian Huch |
clarified and tuned timing estimation;
|
changeset |
files
|
| Fri, 24 Nov 2023 14:01:16 +0100 |
Fabian Huch |
split actual approximation from data handling;
|
changeset |
files
|
| Fri, 24 Nov 2023 13:43:25 +0100 |
Fabian Huch |
clarified timing data vs. timing entries: full top-level data view vs. dynamic partial data;
|
changeset |
files
|
| Fri, 24 Nov 2023 12:35:00 +0100 |
Fabian Huch |
proper filter for approximations;
|
changeset |
files
|
| Fri, 24 Nov 2023 10:36:23 +0100 |
Fabian Huch |
proper inflection point check;
|
changeset |
files
|
| Fri, 24 Nov 2023 10:34:10 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 23 Nov 2023 16:49:39 +0000 |
haftmann |
slightly more elementary characterization of unset_bit
|
changeset |
files
|
| Thu, 23 Nov 2023 16:49:39 +0000 |
haftmann |
more direct characterization of binary bit operations
|
changeset |
files
|
| Thu, 23 Nov 2023 20:58:19 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 23 Nov 2023 20:53:58 +0100 |
Fabian Huch |
clarified timing data operations: proper estimation (instead of known points);
|
changeset |
files
|
| Thu, 23 Nov 2023 20:30:45 +0100 |
Fabian Huch |
use proper max threads (limited by available hardware) in heuristics;
|
changeset |
files
|
| Thu, 23 Nov 2023 20:26:43 +0100 |
Fabian Huch |
clarified time estimation: does not use config;
|
changeset |
files
|
| Thu, 23 Nov 2023 19:56:27 +0100 |
Fabian Huch |
handle inflection point in interpolation with monotone prefix;
|
changeset |
files
|
| Thu, 23 Nov 2023 18:04:04 +0100 |
Fabian Huch |
proper computation of sorted prefix;
|
changeset |
files
|
| Thu, 23 Nov 2023 11:30:43 +0100 |
Fabian Huch |
better build time interpolation: model with Amdahl's law where applicable;
|
changeset |
files
|
| Wed, 22 Nov 2023 18:10:21 +0100 |
Fabian Huch |
proper piecewise linear build time interpolation;
|
changeset |
files
|
| Wed, 22 Nov 2023 15:46:58 +0100 |
Fabian Huch |
properly incorporate running tasks into timing heuristic;
|
changeset |
files
|
| Wed, 22 Nov 2023 15:39:39 +0100 |
Fabian Huch |
clarified ready vs. next ready;
|
changeset |
files
|
| Wed, 22 Nov 2023 15:04:29 +0100 |
Fabian Huch |
introduced path heuristic abstraction;
|
changeset |
files
|
| Wed, 22 Nov 2023 17:50:36 +0000 |
haftmann |
base abstract specification of NOT on recursive equation rather than bit projection
|
changeset |
files
|
| Tue, 21 Nov 2023 19:19:16 +0000 |
haftmann |
modernized, reordered, generalized
|
changeset |
files
|
| Tue, 21 Nov 2023 19:19:16 +0000 |
haftmann |
more correct type annotation
|
changeset |
files
|
| Tue, 21 Nov 2023 23:35:22 +0100 |
wenzelm |
proper build with jdk-21 (amending 4fb5e6499da9);
|
changeset |
files
|
| Mon, 20 Nov 2023 22:17:42 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Mon, 20 Nov 2023 19:52:46 +0100 |
wenzelm |
update to jdk-21.0.1;
|
changeset |
files
|
| Mon, 20 Nov 2023 15:55:10 +0100 |
wenzelm |
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
|
changeset |
files
|
| Mon, 20 Nov 2023 14:23:11 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 20 Nov 2023 14:11:34 +0100 |
wenzelm |
suppress duplicate entries systematically using log_name: e.g. relevant for AFP;
|
changeset |
files
|
| Mon, 20 Nov 2023 13:08:50 +0100 |
wenzelm |
clarified operation: pick current pull_date instead of previous one;
|
changeset |
files
|
| Sun, 19 Nov 2023 15:45:22 +0000 |
haftmann |
operations AND, OR, XOR are specified by characteristic recursive equation
|
changeset |
files
|
| Sat, 18 Nov 2023 19:23:56 +0100 |
Fabian Huch |
clarified toml keys operations;
|
changeset |
files
|
| Sat, 18 Nov 2023 19:22:30 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Sat, 18 Nov 2023 19:16:16 +0100 |
Fabian Huch |
clarified toml keys: more operations;
|
changeset |
files
|
| Sat, 18 Nov 2023 12:34:10 +0100 |
Fabian Huch |
use toml key operations properly;
|
changeset |
files
|
| Sat, 18 Nov 2023 12:25:16 +0100 |
Fabian Huch |
clarified toml keys formatting vs. toString;
|
changeset |
files
|
| Sat, 18 Nov 2023 12:18:44 +0100 |
Fabian Huch |
clarified keys module;
|
changeset |
files
|
| Sat, 18 Nov 2023 12:08:16 +0100 |
Fabian Huch |
pull out toml keys module;
|
changeset |
files
|
| Fri, 17 Nov 2023 14:38:35 +0100 |
Fabian Huch |
clarified toml parser interface;
|
changeset |
files
|
| Sun, 19 Nov 2023 20:45:09 +0100 |
wenzelm |
prefer symbolic build_history_base_arm;
|
changeset |
files
|
| Sun, 19 Nov 2023 20:41:34 +0100 |
wenzelm |
build_history: proper support for ISABELLE_APPLE_PLATFORM64;
|
changeset |
files
|
| Sun, 19 Nov 2023 19:41:17 +0100 |
wenzelm |
clarified isabelle_hg (again, see b9d59669904a);
|
changeset |
files
|
| Sun, 19 Nov 2023 19:29:19 +0100 |
wenzelm |
clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
|
changeset |
files
|
| Sun, 19 Nov 2023 15:15:09 +0100 |
wenzelm |
clarified signature: more operations and options concerning Isabelle hg;
|
changeset |
files
|
| Sun, 19 Nov 2023 14:48:11 +0100 |
wenzelm |
performance tuning: cache graph;
|
changeset |
files
|
| Sun, 19 Nov 2023 12:52:14 +0100 |
wenzelm |
tuned signature: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Sun, 19 Nov 2023 12:51:47 +0100 |
wenzelm |
unused (see also 004b39bf06a5);
|
changeset |
files
|
| Sun, 19 Nov 2023 12:46:41 +0100 |
wenzelm |
clarified signature and modules: more explicit Build_Log.History;
|
changeset |
files
|
| Sat, 18 Nov 2023 21:14:34 +0100 |
wenzelm |
tuned: avoid recursion;
|
changeset |
files
|
| Sat, 18 Nov 2023 20:51:44 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 18 Nov 2023 19:31:22 +0100 |
wenzelm |
avoid duplicate data;
|
changeset |
files
|
| Sat, 18 Nov 2023 19:14:59 +0100 |
wenzelm |
output more data;
|
changeset |
files
|
| Sat, 18 Nov 2023 18:52:34 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 18 Nov 2023 16:58:14 +0100 |
wenzelm |
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
|
changeset |
files
|
| Sat, 18 Nov 2023 15:44:46 +0100 |
wenzelm |
proper ml_statistics (amending aeb511a520f4);
|
changeset |
files
|
| Fri, 17 Nov 2023 10:11:15 +0100 |
Fabian Huch |
unify error messages;
|
changeset |
files
|
| Fri, 17 Nov 2023 09:38:15 +0100 |
Fabian Huch |
add file information to toml parse context and error messages;
|
changeset |
files
|
| Fri, 17 Nov 2023 09:23:28 +0100 |
Fabian Huch |
add position information to toml parser and error messages;
|
changeset |
files
|
| Thu, 16 Nov 2023 15:36:34 +0100 |
Fabian Huch |
properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;
|
changeset |
files
|
| Thu, 16 Nov 2023 15:23:41 +0100 |
Fabian Huch |
allow re-defining keys in toml object (already checked during parse time);
|
changeset |
files
|
| Thu, 16 Nov 2023 15:19:24 +0100 |
Fabian Huch |
clarified toString for toml objects;
|
changeset |
files
|
| Thu, 16 Nov 2023 14:33:45 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 13 Nov 2023 18:08:05 +0100 |
Fabian Huch |
tuned message;
|
changeset |
files
|
| Mon, 13 Nov 2023 17:48:11 +0100 |
Fabian Huch |
better invalidation for schedule cache (only on relevant changes);
|
changeset |
files
|
| Mon, 13 Nov 2023 17:31:37 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Mon, 13 Nov 2023 17:25:26 +0100 |
Fabian Huch |
timing heuristic: parallelize more aggressively to utilize hosts fully;
|
changeset |
files
|
| Mon, 13 Nov 2023 17:00:13 +0100 |
Fabian Huch |
proper parallel paths for timing heuristic;
|
changeset |
files
|
| Mon, 13 Nov 2023 16:16:52 +0100 |
Fabian Huch |
scheduled build: allocate cpus more aggressively, to avoid idle threads;
|
changeset |
files
|
| Fri, 10 Nov 2023 14:52:13 +0100 |
Fabian Huch |
finalize scheduled build only on master node;
|
changeset |
files
|
| Fri, 10 Nov 2023 14:42:07 +0100 |
Fabian Huch |
finalize current sessions before generating schedule;
|
changeset |
files
|
| Fri, 10 Nov 2023 14:07:36 +0100 |
Fabian Huch |
clarified signature: more operations;
|
changeset |
files
|
| Mon, 13 Nov 2023 09:02:56 +0100 |
desharna |
NEWS
|
changeset |
files
|
| Sun, 12 Nov 2023 22:34:08 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 12 Nov 2023 22:34:03 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 12 Nov 2023 22:18:12 +0100 |
wenzelm |
support for "cluster" table with "hosts" array, and params/options as for "host" table;
|
changeset |
files
|
| Sun, 12 Nov 2023 22:05:59 +0100 |
wenzelm |
clarified signature: more operations, allow recursive get;
|
changeset |
files
|
| Sun, 12 Nov 2023 20:59:23 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 12 Nov 2023 20:19:51 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sun, 12 Nov 2023 19:58:45 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 12 Nov 2023 12:54:26 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sun, 12 Nov 2023 12:34:04 +0100 |
wenzelm |
more robust: prefer strict operations;
|
changeset |
files
|
| Sun, 12 Nov 2023 12:33:22 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sun, 12 Nov 2023 12:26:08 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 11 Nov 2023 17:44:03 +0000 |
haftmann |
more specific name for type class
|
changeset |
files
|
| Sat, 11 Nov 2023 22:17:14 +0100 |
wenzelm |
proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);
|
changeset |
files
|
| Sat, 11 Nov 2023 22:14:38 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 11 Nov 2023 22:05:37 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 11 Nov 2023 21:25:20 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Sat, 11 Nov 2023 21:17:45 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 11 Nov 2023 21:08:21 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Sat, 11 Nov 2023 21:06:54 +0100 |
wenzelm |
more TODO;
|
changeset |
files
|
| Sat, 11 Nov 2023 21:05:41 +0100 |
wenzelm |
prefer strict test of system options;
|
changeset |
files
|
| Sat, 11 Nov 2023 20:43:20 +0100 |
wenzelm |
some build cluster resources at TUM;
|
changeset |
files
|
| Sat, 11 Nov 2023 20:13:23 +0100 |
wenzelm |
build cluster host specifications are based on registry entries (table prefix "host");
|
changeset |
files
|
| Sat, 11 Nov 2023 20:08:20 +0100 |
wenzelm |
more robust init;
|
changeset |
files
|
| Sat, 11 Nov 2023 20:01:14 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Sat, 11 Nov 2023 19:36:59 +0100 |
wenzelm |
support interpreted/typed entries via Registry.Category and Registry.Table;
|
changeset |
files
|
| Sat, 11 Nov 2023 18:39:57 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Sat, 11 Nov 2023 16:01:57 +0100 |
wenzelm |
clarified output;
|
changeset |
files
|
| Sat, 11 Nov 2023 13:31:14 +0100 |
wenzelm |
support for global registry;
|
changeset |
files
|
| Fri, 10 Nov 2023 16:03:52 +0100 |
wenzelm |
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";
|
changeset |
files
|
| Thu, 09 Nov 2023 15:11:52 +0000 |
haftmann |
slightly less technical formulation of very specific type class
|
changeset |
files
|
| Thu, 09 Nov 2023 15:11:51 +0000 |
haftmann |
weakened dependency
|
changeset |
files
|
| Thu, 09 Nov 2023 15:11:51 +0000 |
haftmann |
explicit type class for discrete linordered semidoms
|
changeset |
files
|
| Thu, 09 Nov 2023 19:06:50 +0100 |
Fabian Huch |
proper dummy timing entries;
|
changeset |
files
|
| Thu, 09 Nov 2023 17:58:21 +0100 |
Fabian Huch |
use only finished sessions in timing data;
|
changeset |
files
|
| Thu, 09 Nov 2023 16:39:36 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 09 Nov 2023 15:45:51 +0100 |
Fabian Huch |
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
|
changeset |
files
|
| Thu, 09 Nov 2023 11:49:08 +0100 |
Fabian Huch |
performance tuning for build schedule: faster stopping;
|
changeset |
files
|
| Thu, 09 Nov 2023 11:41:19 +0100 |
Fabian Huch |
performance tuning for timing heuristic: pre-calculate graph operations;
|
changeset |
files
|
| 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);
|
changeset |
files
|
| Thu, 09 Nov 2023 14:28:17 +0100 |
wenzelm |
clarified signature: emphasize mutable instance;
|
changeset |
files
|
| Thu, 09 Nov 2023 14:22:19 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Thu, 09 Nov 2023 13:31:09 +0100 |
wenzelm |
support for explicit SSH hostname;
|
changeset |
files
|
| Thu, 09 Nov 2023 11:30:33 +0100 |
wenzelm |
proper local host (amending 62d7ef1da441);
|
changeset |
files
|
| Wed, 08 Nov 2023 21:45:02 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 08 Nov 2023 21:44:44 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 08 Nov 2023 20:31:29 +0100 |
wenzelm |
proper default for disjunction (amending 9f7a94117666);
|
changeset |
files
|
| Wed, 08 Nov 2023 19:04:44 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 08 Nov 2023 16:05:22 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Wed, 08 Nov 2023 15:37:15 +0100 |
wenzelm |
avoid option -C: free this latter for build-related configuration;
|
changeset |
files
|
| Wed, 08 Nov 2023 15:10:19 +0100 |
wenzelm |
more direct indentation, using Symbol.spaces;
|
changeset |
files
|
| Wed, 08 Nov 2023 13:14:59 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 08 Nov 2023 13:00:24 +0100 |
wenzelm |
more accurate treatment of surrounding whitespace;
|
changeset |
files
|
| Wed, 08 Nov 2023 12:41:41 +0100 |
wenzelm |
obsolete (see also f627ab8c276c);
|
changeset |
files
|
| Wed, 08 Nov 2023 12:00:29 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 08 Nov 2023 11:53:38 +0100 |
wenzelm |
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
|
changeset |
files
|
| Tue, 07 Nov 2023 15:59:02 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Tue, 07 Nov 2023 12:06:59 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 07 Nov 2023 12:06:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 07 Nov 2023 12:02:34 +0100 |
wenzelm |
proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);
|
changeset |
files
|
| Sun, 05 Nov 2023 19:55:18 +0100 |
wenzelm |
more tests;
|
changeset |
files
|
| Sun, 05 Nov 2023 19:40:39 +0100 |
wenzelm |
clarified exploration of history: more uniform options;
|
changeset |
files
|
| Sun, 05 Nov 2023 19:32:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 05 Nov 2023 19:28:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 04 Nov 2023 20:28:07 +0100 |
wenzelm |
enable multi-builds (again, see also 0c7419d3dd59);
|
changeset |
files
|
| Sat, 04 Nov 2023 20:10:17 +0100 |
wenzelm |
explore history more thoroughly;
|
changeset |
files
|
| Sat, 04 Nov 2023 17:19:22 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 04 Nov 2023 17:29:49 +0100 |
wenzelm |
clarified "recent" time: days <= 0 means infinity (no constraint);
|
changeset |
files
|
| Sat, 04 Nov 2023 16:56:54 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 04 Nov 2023 16:48:51 +0100 |
wenzelm |
proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda);
|
changeset |
files
|
| Sat, 04 Nov 2023 16:45:16 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 04 Nov 2023 16:31:02 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sat, 04 Nov 2023 16:30:24 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 04 Nov 2023 16:07:22 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Fri, 03 Nov 2023 19:10:21 +0100 |
wenzelm |
proper option;
|
changeset |
files
|
| Fri, 03 Nov 2023 19:00:00 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 03 Nov 2023 18:58:53 +0100 |
wenzelm |
proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1;
|
changeset |
files
|
| Fri, 03 Nov 2023 16:20:06 +0000 |
paulson |
Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
|
changeset |
files
|
| Fri, 03 Nov 2023 10:55:15 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 03 Nov 2023 10:30:51 +0100 |
wenzelm |
prefer Time.scale(), following Isabelle/ML;
|
changeset |
files
|
| Fri, 03 Nov 2023 10:21:21 +0100 |
Fabian Huch |
proper benchmark command;
|
changeset |
files
|
| Fri, 03 Nov 2023 10:13:41 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 03 Nov 2023 10:12:34 +0100 |
wenzelm |
proper progress (see also 45d570945fe4);
|
changeset |
files
|
| Fri, 03 Nov 2023 10:03:05 +0100 |
Fabian Huch |
improved build messages;
|
changeset |
files
|
| Thu, 02 Nov 2023 21:35:04 +0100 |
Lukas Stevens |
clarified;
|
changeset |
files
|
| Thu, 02 Nov 2023 14:10:16 +0000 |
paulson |
merged
|
changeset |
files
|
| Thu, 02 Nov 2023 14:10:08 +0000 |
paulson |
fixed the simplification of Suc n - 1
|
changeset |
files
|
| Thu, 02 Nov 2023 14:31:01 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 02 Nov 2023 13:16:06 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 02 Nov 2023 13:05:29 +0100 |
wenzelm |
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
|
changeset |
files
|
| Thu, 02 Nov 2023 12:03:30 +0100 |
wenzelm |
more detailed progress for build_log_database, to see better what happens when;
|
changeset |
files
|
| Thu, 02 Nov 2023 11:57:40 +0100 |
wenzelm |
clarified signature: explicit Progress date;
|
changeset |
files
|
| Thu, 02 Nov 2023 10:29:24 +0100 |
wenzelm |
more uniform progress;
|
changeset |
files
|
| Thu, 02 Nov 2023 10:23:28 +0100 |
wenzelm |
more robust: support concurrent output;
|
changeset |
files
|
| Thu, 02 Nov 2023 10:12:12 +0100 |
wenzelm |
disable multi-builds (again): does not quite work yet;
|
changeset |
files
|
| Tue, 31 Oct 2023 17:32:56 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Tue, 31 Oct 2023 17:24:19 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 31 Oct 2023 17:01:19 +0100 |
wenzelm |
clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
|
changeset |
files
|
| Tue, 31 Oct 2023 16:49:03 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 31 Oct 2023 16:45:39 +0100 |
wenzelm |
proper Compress.Cache;
|
changeset |
files
|
| Tue, 31 Oct 2023 16:24:07 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 31 Oct 2023 16:15:59 +0100 |
wenzelm |
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
|
changeset |
files
|
| Tue, 31 Oct 2023 16:11:26 +0100 |
wenzelm |
support for mailbox limit;
|
changeset |
files
|
| Tue, 31 Oct 2023 15:40:46 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 31 Oct 2023 14:35:51 +0100 |
wenzelm |
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
|
changeset |
files
|
| Tue, 31 Oct 2023 14:26:19 +0100 |
wenzelm |
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
|
changeset |
files
|
| Sun, 29 Oct 2023 20:14:46 +0100 |
wenzelm |
afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb);
|
changeset |
files
|
| Sun, 29 Oct 2023 19:42:46 +0100 |
wenzelm |
performance tuning: parallel and incremental update of build_log_database;
|
changeset |
files
|
| Sun, 29 Oct 2023 18:49:42 +0100 |
wenzelm |
performance tuning: more careful database access;
|
changeset |
files
|
| Sun, 29 Oct 2023 11:57:01 +0100 |
wenzelm |
clarified message;
|
changeset |
files
|
| Sun, 29 Oct 2023 11:49:33 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 29 Oct 2023 11:39:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Oct 2023 19:13:02 +0200 |
wenzelm |
prefer old-style import "=>";
|
changeset |
files
|
| Sat, 28 Oct 2023 17:35:26 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 26 Oct 2023 22:44:31 +0200 |
wenzelm |
redundant (see also 3069da1743bc);
|
changeset |
files
|
| Thu, 26 Oct 2023 22:20:22 +0200 |
wenzelm |
removed obsolete table (see also 6acd1a2bd146);
|
changeset |
files
|
| Thu, 26 Oct 2023 22:10:22 +0200 |
wenzelm |
more robust init_database();
|
changeset |
files
|
| Thu, 26 Oct 2023 16:04:48 +0200 |
wenzelm |
proper private_data.transaction_lock;
|
changeset |
files
|
| Thu, 26 Oct 2023 15:38:27 +0200 |
wenzelm |
clarified names;
|
changeset |
files
|
| Thu, 26 Oct 2023 12:36:19 +0200 |
wenzelm |
proper support for SSH;
|
changeset |
files
|
| Thu, 26 Oct 2023 12:27:10 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 26 Oct 2023 11:50:50 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Wed, 18 Oct 2023 20:51:24 +0200 |
Fabian Huch |
add module for faster scheduled builds;
|
changeset |
files
|
| Wed, 18 Oct 2023 20:26:02 +0200 |
Fabian Huch |
always use host database and make protected;
|
changeset |
files
|
| Wed, 18 Oct 2023 20:12:07 +0200 |
Fabian Huch |
read relative cpu from build log;
|
changeset |
files
|
| Wed, 18 Oct 2023 20:07:54 +0200 |
Fabian Huch |
prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);
|
changeset |
files
|
| Wed, 18 Oct 2023 19:53:39 +0200 |
Fabian Huch |
added start date to build jobs, e.g., for build time estimation;
|
changeset |
files
|
| Wed, 18 Oct 2023 19:49:08 +0200 |
Fabian Huch |
added initial version of benchmark module, e.g., to compare performance of different hosts;
|
changeset |
files
|
| Wed, 18 Oct 2023 19:26:37 +0200 |
Fabian Huch |
generalized node infos: allow addressing of numa node segments via relative cpus;
|
changeset |
files
|
| Wed, 18 Oct 2023 19:05:06 +0200 |
Fabian Huch |
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
|
changeset |
files
|
| Wed, 18 Oct 2023 18:53:26 +0200 |
Fabian Huch |
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
|
changeset |
files
|
| Wed, 18 Oct 2023 18:48:49 +0200 |
Fabian Huch |
defined statically known tables of Build_Log;
|
changeset |
files
|
| Fri, 27 Oct 2023 18:27:06 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Fri, 27 Oct 2023 08:16:16 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Thu, 26 Oct 2023 20:41:42 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Thu, 26 Oct 2023 17:53:22 +0200 |
Fabian Huch |
NEWS and CONTRIBUTORS;
|
changeset |
files
|
| Thu, 26 Oct 2023 11:39:45 +0200 |
Fabian Huch |
remove unused ci-extras component;
|
changeset |
files
|
| Thu, 26 Oct 2023 10:53:51 +0200 |
Fabian Huch |
use mail module in CI build;
|
changeset |
files
|
| Tue, 24 Oct 2023 19:17:46 +0200 |
Fabian Huch |
added mail module;
|
changeset |
files
|
| Thu, 26 Oct 2023 11:29:00 +0200 |
Fabian Huch |
build javamail component and add to main components;
|
changeset |
files
|
| Thu, 26 Oct 2023 11:23:53 +0200 |
Fabian Huch |
added component for javax mail;
|
changeset |
files
|
| Wed, 25 Oct 2023 17:06:21 +0200 |
wenzelm |
updated to vampire-4.8;
|
changeset |
files
|
| Wed, 25 Oct 2023 13:51:51 +0200 |
wenzelm |
tuned README;
|
changeset |
files
|
| Wed, 25 Oct 2023 13:01:47 +0200 |
wenzelm |
update Vampire version, following hints by Martin Desharnais;
|
changeset |
files
|
| Wed, 25 Oct 2023 11:52:40 +0200 |
wenzelm |
removed junk;
|
changeset |
files
|
| Fri, 20 Oct 2023 12:26:56 +0200 |
desharna |
tuned component_vampire script for Vampire 4.8 and added new flag to force version name
|
changeset |
files
|
| Tue, 24 Oct 2023 18:29:53 +0200 |
Fabian Huch |
prefer Isabelle options for CI mail settings over ci.properties;
|
changeset |
files
|
| Mon, 23 Oct 2023 16:19:19 +0100 |
paulson |
Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.
|
changeset |
files
|
| Mon, 23 Oct 2023 12:52:56 +0200 |
wenzelm |
proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);
|
changeset |
files
|
| Mon, 23 Oct 2023 12:11:39 +0200 |
wenzelm |
unused (see fe9e590ae52f);
|
changeset |
files
|
| Mon, 23 Oct 2023 12:08:38 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 22 Oct 2023 19:40:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 22 Oct 2023 15:25:08 +0200 |
wenzelm |
update documentation on simproc_setup;
|
changeset |
files
|
| Sun, 22 Oct 2023 13:56:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 22 Oct 2023 12:18:23 +0200 |
wenzelm |
proper morphism;
|
changeset |
files
|
| Sat, 21 Oct 2023 21:19:02 +0200 |
wenzelm |
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
|
changeset |
files
|
| Sat, 21 Oct 2023 14:36:47 +0200 |
wenzelm |
more compact ML source;
|
changeset |
files
|
| Sat, 21 Oct 2023 12:02:23 +0200 |
wenzelm |
more robust read_simproc_spec: proper error positions;
|
changeset |
files
|
| Sat, 21 Oct 2023 11:34:37 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 21 Oct 2023 11:24:34 +0200 |
wenzelm |
more standard simproc_setup using ML antiquotation;
|
changeset |
files
|