wenzelm [Mon, 06 Mar 2023 16:20:12 +0100] rev 77545
clarified database content;
tuned signature;
wenzelm [Mon, 06 Mar 2023 16:06:24 +0100] rev 77544
tuned: prefer iterator.nextOption;
wenzelm [Mon, 06 Mar 2023 15:56:28 +0100] rev 77543
tuned whitespace and braces;
wenzelm [Mon, 06 Mar 2023 15:48:04 +0100] rev 77542
clarified signature: more uniform operations;
wenzelm [Mon, 06 Mar 2023 15:38:50 +0100] rev 77541
tuned signature: reduce boilerplate;
wenzelm [Mon, 06 Mar 2023 15:12:37 +0100] rev 77540
tuned signature;
wenzelm [Mon, 06 Mar 2023 15:01:44 +0100] rev 77539
proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm [Mon, 06 Mar 2023 12:08:33 +0100] rev 77538
more database content: formal end_build;
wenzelm [Mon, 06 Mar 2023 12:07:40 +0100] rev 77537
more operations;
wenzelm [Mon, 06 Mar 2023 11:39:40 +0100] rev 77536
clarified database content and prepare/init stages;
wenzelm [Mon, 06 Mar 2023 10:58:36 +0100] rev 77535
tuned signature;
wenzelm [Mon, 06 Mar 2023 10:16:40 +0100] rev 77534
tuned;
wenzelm [Mon, 06 Mar 2023 10:08:53 +0100] rev 77533
tuned;
wenzelm [Mon, 06 Mar 2023 09:50:48 +0100] rev 77532
less verbosity, amending 3bc49507bae5;
wenzelm [Mon, 06 Mar 2023 09:46:41 +0100] rev 77531
tuned comments;
tuned structure;
wenzelm [Mon, 06 Mar 2023 09:37:02 +0100] rev 77530
tuned signature: avoid totally adhoc overriding;
wenzelm [Mon, 06 Mar 2023 09:32:18 +0100] rev 77529
separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm [Sun, 05 Mar 2023 20:41:45 +0100] rev 77528
enforce rebuild of Isabelle/ML, after various changes to build database management;
wenzelm [Sun, 05 Mar 2023 20:41:14 +0100] rev 77527
more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
wenzelm [Sun, 05 Mar 2023 19:33:01 +0100] rev 77526
tuned output;
wenzelm [Sun, 05 Mar 2023 19:21:07 +0100] rev 77525
clarified database content: store actual value instead of index;
wenzelm [Sun, 05 Mar 2023 18:38:52 +0100] rev 77524
more robust: disallow override;
wenzelm [Sun, 05 Mar 2023 18:20:05 +0100] rev 77523
tuned messages;
wenzelm [Sun, 05 Mar 2023 18:18:09 +0100] rev 77522
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm [Sun, 05 Mar 2023 16:36:18 +0100] rev 77521
clarified signature: manage "verbose" flag via "progress";
wenzelm [Sun, 05 Mar 2023 16:26:59 +0100] rev 77520
removed unused arguments: avoid ambiguity concerning progress/verbose;
wenzelm [Sun, 05 Mar 2023 16:14:48 +0100] rev 77519
clarified protocol for "verbose" messages;
wenzelm [Sun, 05 Mar 2023 15:34:00 +0100] rev 77518
clarified signature: manage "verbose" flag via "progress";
wenzelm [Sun, 05 Mar 2023 15:25:02 +0100] rev 77517
tuned;
wenzelm [Sun, 05 Mar 2023 15:19:53 +0100] rev 77516
tuned;
wenzelm [Sun, 05 Mar 2023 15:19:17 +0100] rev 77515
more operations;
wenzelm [Sun, 05 Mar 2023 14:53:32 +0100] rev 77514
tuned signature;
wenzelm [Sun, 05 Mar 2023 13:42:10 +0100] rev 77513
more robust: proper bound checks;
wenzelm [Sun, 05 Mar 2023 12:52:04 +0100] rev 77512
enforce rebuild of Isabelle/ML, after various changes to build database management;
wenzelm [Sat, 04 Mar 2023 23:43:53 +0100] rev 77511
clarified modules;
wenzelm [Sat, 04 Mar 2023 23:25:30 +0100] rev 77510
clarified signature: manage "verbose" flag via "progress";
wenzelm [Sat, 04 Mar 2023 22:29:21 +0100] rev 77509
clarified treatment of "verbose" messages, e.g. Progress.theory();
always store messages within database, with explicit "verbose" flag: client-side will decide about output;
wenzelm [Sat, 04 Mar 2023 21:41:16 +0100] rev 77508
proper "val verbose" (amending 2e2b2bd6b2d2);
wenzelm [Sat, 04 Mar 2023 21:25:12 +0100] rev 77507
tuned whitespace;
wenzelm [Sat, 04 Mar 2023 17:36:29 +0100] rev 77506
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
wenzelm [Sat, 04 Mar 2023 16:45:21 +0100] rev 77505
support progress backed by database;
moved Build_Progress.Context.progress/log to class Build_Process: database is available here;
wenzelm [Sat, 04 Mar 2023 16:15:50 +0100] rev 77504
tuned;
wenzelm [Sat, 04 Mar 2023 12:59:22 +0100] rev 77503
tuned messages;
wenzelm [Sat, 04 Mar 2023 12:43:35 +0100] rev 77502
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm [Sat, 04 Mar 2023 12:16:58 +0100] rev 77501
tuned signature;
wenzelm [Sat, 04 Mar 2023 12:14:20 +0100] rev 77500
tuned signature;
wenzelm [Sat, 04 Mar 2023 12:05:51 +0100] rev 77499
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm [Sat, 04 Mar 2023 11:45:14 +0100] rev 77498
proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;
wenzelm [Fri, 03 Mar 2023 20:11:08 +0100] rev 77497
merged
wenzelm [Fri, 03 Mar 2023 20:10:47 +0100] rev 77496
more database content;
clarified signature;
tuned comments;
wenzelm [Fri, 03 Mar 2023 13:50:54 +0100] rev 77495
tuned signature;
wenzelm [Fri, 03 Mar 2023 13:50:39 +0100] rev 77494
tuned whitespace;
wenzelm [Fri, 03 Mar 2023 13:39:46 +0100] rev 77493
tuned signature;
paulson [Fri, 03 Mar 2023 12:22:07 +0000] rev 77492
merged
paulson <lp15@cam.ac.uk> [Fri, 03 Mar 2023 12:21:58 +0000] rev 77491
More of Eberl's material
paulson <lp15@cam.ac.uk> [Thu, 02 Mar 2023 17:17:18 +0000] rev 77490
Some new lemmas. Some tidying up
blanchet [Fri, 03 Mar 2023 11:25:29 +0100] rev 77489
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
blanchet [Fri, 03 Mar 2023 10:30:10 +0100] rev 77488
got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)
wenzelm [Thu, 02 Mar 2023 17:46:29 +0100] rev 77487
merged
wenzelm [Thu, 02 Mar 2023 17:05:24 +0100] rev 77486
clarified execution context: main work happens within Future.thread;
clarified signature: only one "join" operation;