tuned signature;

tuned structure;

clarified signature;

clarified signature;

clarified build process roles: "worker" vs. "build";

clarified database content; tuned signature;

tuned: prefer iterator.nextOption;

tuned whitespace and braces;

clarified signature: more uniform operations;

tuned signature: reduce boilerplate;

tuned signature;

proper clean_build of old data at start of new process --- allow to inspect remains of the last process;

more database content: formal end_build;

more operations;

clarified database content and prepare/init stages;

tuned signature;

tuned;

tuned;

less verbosity, amending 3bc49507bae5;

tuned comments; tuned structure;

tuned signature: avoid totally adhoc overriding;

separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;

enforce rebuild of Isabelle/ML, after various changes to build database management;

more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;

tuned output;

clarified database content: store actual value instead of index;

more robust: disallow override;

tuned messages;

more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;

clarified signature: manage "verbose" flag via "progress";

removed unused arguments: avoid ambiguity concerning progress/verbose;

clarified protocol for "verbose" messages;

clarified signature: manage "verbose" flag via "progress";

tuned;

tuned;

more operations;

tuned signature;

more robust: proper bound checks;

enforce rebuild of Isabelle/ML, after various changes to build database management;

clarified modules;

clarified signature: manage "verbose" flag via "progress";

clarified treatment of "verbose" messages, e.g. Progress.theory(); always store messages within database, with explicit "verbose" flag: client-side will decide about output;

proper "val verbose" (amending 2e2b2bd6b2d2);

tuned whitespace;

more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);

support progress backed by database; moved Build_Progress.Context.progress/log to class Build_Process: database is available here;

tuned;

tuned messages;

clarified signature: require just one "override def echo(message: Progress.Message): Unit";

tuned signature;

tuned signature;

clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";

proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;

merged

more database content; clarified signature; tuned comments;

tuned signature;

tuned whitespace;

tuned signature;

merged

More of Eberl's material

Some new lemmas. Some tidying up

detect duplicates in Sledgehammer output -- suggested by Larry Paulson

got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)

merged

clarified execution context: main work happens within Future.thread; clarified signature: only one "join" operation;

clarified timeout: closer to actual process;

tuned names;

clarified names;

tuned, following ML_Statistics.monitor;

unused (see also 0cebcbeac4c7);

tuned;

tuned;

tuned comments;

clarified modules; tuned signature; tuned comments;

clarified modules;

clarified modules;

clarified signature;

clarified modules;

clarified modules;

tuned;

clarified modules;

clarified modules;

tuned;

more robust: proper synchronization of transition from next_job to start_session;

more thorough synchronized_database for internal *and* external state;

simplified startup under "locked" condition (in contrast to f7e413e8d269);

more explicit session name, in anticipation of variants like "session.document", "session.browser_info";

tuned signature;

tuned signature;

tuned signature;

tuned signature: support general Build_Job instances;

tuned signature;

clarified signature: prefer static data;

tuned signature;

identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);

tuned signature;

tuned signature;

tuned signature;

tuned;

unused;

tuned signature (again);

tuned;

tuned;

proper deps from build_graph, not imports_graph (amending 0c704aba71e3);

misc tuning: more direct access to ancestors, without build_graph;

tuned signature (again);

clarified signature: reduce explicit access to static Sessions.Structure;

tuned signature;

clarified modules (again);

tuned;

tuned signature;

avoid premature Properties.uncompress: allow blob to be stored in another database;

more robust: synchronized access to database;

clarified signature: do not expose global state to object-oriented variants;

tuned comments and outline;

merged

Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed

A little bit more tidying up

tweaked Sledgehammer interaction

there won't be an E version 2.7

reverted 0506c3273814 -- the message is still useful

compile

adopt terminology suggested by Larry Paulson

more robust E proof parsing

avoid double 'Warning:' in Sledgehammer messages

tweaked abduction in Sledgehammer

slightly more documentation

renamed new Sledgehammer option

updated documentation

improve ad hoc abduction in Sledgehammer

tuning

don't apply abduction and consistency checking to goals of the form 'False'

implemented ad hoc abduction in Sledgehammer with E

tuned;

clarified scope of "serial" and "numa_index" within database;

clarified signature: allow more general init, e.g. from existing database;

clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;

tuned;

simplified somewhat pointless error message (see also 0189fe0f6452);

clafified signature: simplify object-oriented reuse;

revert pointless 375c6b9ce9ea: overall thread context is already uninterruptible (see 54ac957c53ec);

tuned whitespace;

merged

Fixed a presentation error

Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem

tuned whitespace;

tuned;

clarified signature, although "sql" argument is de-facto mandatory;

tuned;

proper SQL (amending 7ab9bac1ca96);

clarified signature: more explicit "synchronized" regions;

more robust interrupt handling, notably for Build_Job.terminate();

clarified signature: works for general Build_Job;

tuned;

clarified modules;

clarified signature;

proper log_lines, without protocol messages (amending cb3f5361fbca);

clarified signature;

tuned messages;

clarified error output vs. process_result stored in build_database (see also 13a0f537e232 and bff56eae3ec5);

clarified system option: guard for testing, until the database layout has stabilized;

merged

Simplified some proofs

clarified db content: avoid redundancy of historic ML_IDENTIFIER;

merged

proper filterNot, not filterNot-not;

option build_hostname allows to change hostname easily;

clarified permissions of build.db, following server.db;

enforce rebuild of Isabelle/ML, after various changes to build database management;

misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;

tuned: fewer warnings in IntelliJ IDEA;

clarified init_database vs. update_database: implicitly assume fresh "instance";

clarified Build_Process.Context: cover all static information;

tuned whitespace in generated SQL;

tuned: prefer typed operations;

clarified signature: more concise operations;

more robust options in "prefs" format: avoid odd control character;

proper settings for hostname: allow to adjust it in user space;

support for build database: still inactive; more detailed Build_Job.Node_Info;

tuned signature;

clarified signature: more robust operations;

tuned;

tuned;

more operations;

clarified signature: more operations;

clarified signature;

clarified signature: more robust (see also cf2ef4be3630);

unused (see also 7b318273a4aa and a1fb4d28e609);

tidying ugly proofs

brought back [...] maplet syntax

merged

has_sum now an infix operator!!

merged

New material contributed by Manuel

Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation

added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO

added lemma multpDM_plus_plusI[simp]

added lemmas multpDM_mono_strong and multpHO_mono_strong

merged

One new (necessary) theorem

merged

more operations to support management of jobs, e.g. from external database;

more uniform operations;

more operations;

clarified signature: more robust;

more operations;

allow arbitrary info, e.g. for custom scheduler;

clarified signature;

merged

Simplified some proofs

merged

tuned signature;

tuned signature: avoid warnings in IntelliJ IDEA;

tuned signature;

tuned signature;

tuned signature;

clarified state: more explicit type as plain value, which is also easier to sync with external db;

tuned signature;

tuned signature;

clarified signature: support meaningful subclasses for Build.Engine implementations;

support alternative build engines, via system option "build_engine";

misc tuning and clarification; support SSH.System;

proper test, following Platform.is_linux;

clarified signature;

clarified signature;

merged

Simplified some more proofs

merged

Replacing z powr of_int i by z powi i and adding new material from the AFP

merged

tuned: avoid redundant white space;

clarified signature: more robust operations, without assumption about node 0;

clarified signature: more concise operations;

clarified modules: NUMA is managed by Build_Process;

tuned signature;

clarified signature: move all parameters into Build_Process.Context;

clarified signature;

more elementary data structures, to fit better to SQL database;

clarified signature (see also 68a7ad1385bc);

clarified signature;