merged

back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;

vacuum everything in the database;

tuned;

proper vacuum of session_info tables: only once per build process;

tuned signature;

more thorough database checks;

more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;

clarified build options;

clarified ML option vs. Scala option (see also caa182bdab7a);

merge conflict

unified function update and map update syntaxes

removed accidental junk

map update syntax

proper sorting of result (amending f458547b4f0f);

merged

enforce rebuild of Isabelle/ML;

more operations;

more specific vacuum operation, which is also relevant to PostgreSQL;

tuned signature: removed redundant argument;

tuned signature;

proper build_uuid for Build_Process.Task: thus old entries are removed via prepare_database/clean_build;

more informative Build_Process.Snapshot;

more explicit snapshot of "_state" and "_database";

tuned;

removed redundant State.workers: directly maintained within the database, using with SQL update;

more thorough cleanup;

tuned signature;

tuned signature;

tuned signature;

more thorough synchronization of internal "_state" vs. external "_database";

more database content; clarified signature;