| Mon, 20 Nov 2023 13:08:50 +0100 |
wenzelm |
clarified operation: pick current pull_date instead of previous one;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 15:15:09 +0100 |
wenzelm |
clarified signature: more operations and options concerning Isabelle hg;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 12:51:47 +0100 |
wenzelm |
unused (see also 004b39bf06a5);
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 12:46:41 +0100 |
wenzelm |
clarified signature and modules: more explicit Build_Log.History;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 16:58:14 +0100 |
wenzelm |
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 15:44:46 +0100 |
wenzelm |
proper ml_statistics (amending aeb511a520f4);
|
file |
diff |
annotate
|
| Wed, 08 Nov 2023 20:31:29 +0100 |
wenzelm |
proper default for disjunction (amending 9f7a94117666);
|
file |
diff |
annotate
|
| Sat, 04 Nov 2023 17:29:49 +0100 |
wenzelm |
clarified "recent" time: days <= 0 means infinity (no constraint);
|
file |
diff |
annotate
|
| Sat, 04 Nov 2023 16:07:22 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 14:31:01 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 13:16:06 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 13:05:29 +0100 |
wenzelm |
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 12:03:30 +0100 |
wenzelm |
more detailed progress for build_log_database, to see better what happens when;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 10:29:24 +0100 |
wenzelm |
more uniform progress;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 16:45:39 +0100 |
wenzelm |
proper Compress.Cache;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 16:24:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 16:15:59 +0100 |
wenzelm |
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 14:35:51 +0100 |
wenzelm |
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 14:26:19 +0100 |
wenzelm |
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 18:49:42 +0100 |
wenzelm |
performance tuning: more careful database access;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 11:57:01 +0100 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 11:49:33 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 11:39:17 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 22:44:31 +0200 |
wenzelm |
redundant (see also 3069da1743bc);
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 22:20:22 +0200 |
wenzelm |
removed obsolete table (see also 6acd1a2bd146);
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 22:10:22 +0200 |
wenzelm |
more robust init_database();
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 16:04:48 +0200 |
wenzelm |
proper private_data.transaction_lock;
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 15:38:27 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 20:12:07 +0200 |
Fabian Huch |
read relative cpu from build log;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 18:48:49 +0200 |
Fabian Huch |
defined statically known tables of Build_Log;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 21:11:59 +0200 |
wenzelm |
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 21:54:35 +0200 |
wenzelm |
proper pattern (amending ff86f10e54cd);
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 17:17:12 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 12:53:28 +0200 |
wenzelm |
misc tuning: support "scalac -source 3.3";
|
file |
diff |
annotate
|
| Tue, 18 Jul 2023 23:03:39 +0200 |
wenzelm |
more options for performance tuning;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2023 12:19:12 +0200 |
wenzelm |
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
|
file |
diff |
annotate
|
| Sun, 16 Jul 2023 09:50:42 +0200 |
wenzelm |
proper close() operation;
|
file |
diff |
annotate
|
| Sat, 15 Jul 2023 19:34:48 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Fri, 14 Jul 2023 14:56:48 +0200 |
wenzelm |
clarified signature: follow Store.open_database;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2023 13:13:10 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 21 Jun 2023 14:27:51 +0200 |
wenzelm |
clarified signature: more explicit class SQL.Data;
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 11:47:43 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2023 19:10:01 +0200 |
wenzelm |
proper stmt.execute() within loop (amending 9d9b30741fc4);
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 21:28:48 +0200 |
wenzelm |
more informative errors;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 21:23:56 +0200 |
wenzelm |
clarified options;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 21:16:14 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 20:56:43 +0200 |
wenzelm |
provide Isabelle tool wrapper;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 20:41:54 +0200 |
wenzelm |
more robust errors: proceed updating database;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 15:02:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 14:59:55 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 14:52:54 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 14:22:01 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 15:58:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2023 20:25:48 +0100 |
wenzelm |
more specific vacuum operation, which is also relevant to PostgreSQL;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2023 21:12:47 +0100 |
wenzelm |
clarified signature: reduce boilerplate;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2023 19:37:32 +0100 |
wenzelm |
clarified messages;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2023 16:06:24 +0100 |
wenzelm |
tuned: prefer iterator.nextOption;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2023 15:56:28 +0100 |
wenzelm |
tuned whitespace and braces;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2023 15:38:50 +0100 |
wenzelm |
tuned signature: reduce boilerplate;
|
file |
diff |
annotate
|
| Fri, 03 Mar 2023 13:50:39 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|