tuned signature: more operations;

avoid excessive accumulation of garbage, for profiling of huge sessions;

clarified signature: systematic use of Properties.make_string;

tuned;

support for let in Alethe name bindings;

merged

A few more cosmetic changes to proofs

merged

tidying a few proofs a bit more

partly tidied some truly horrible proofs

update for release;

back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool;

performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);

clarified statistics;

show more build history for AFP;

more statistics;

proper base_thys;

more thorough context tracing;

proper check;

proper symbolic hostname, as provided via Build_Cluster.Host;

unused;

clarified signature: Build_Cluster.Session.build_context; proper implementation of Build_Cluster.Session.start() based on Build.build_worker_command();

clarified exception handling and return_code;

tuned signature: more operations;

more robust;

support for Build_Cluster.Session.init (rsync + Admin/init); clarified Build.Results and overall return code;

prefer Process_Result.RC.merge: strict treatment of interrupt;

clarified signature: more operations;

proper afp_root;

clarified signature: more "object-oriented" style;

more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process;

clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;

tuned signature;

tuned signature; more operations;

clarified option (see also b66b6cc1eb8c);

more build_cluster management: open SSH connections in parallel, but synchronously;

tuned signature: more options;

clarified signature: more operations;

tuned signature;

more accurate print vs. parse;

clarified signature; tuned output;

clarified signature (again); more explicit "local" name;

tuned output;

tuned output;

clarified modules;

more pro-forma support for afp_root;

tuned NEWS: emphasize "isabelle build" add-ons;

added option -A for AFP root, following "isabelle sync";

clarified signature: more operations;

tuned signature;

clarified file location: to be used by regular Isabelle/Scala tools;

update headers;

more pro-forma support for Build_Cluster;

tuned;

tuned;

clarified options;

clarified options;

proper Build_Cluster.Host.parse for parameters and system options; clarified Build_Cluster.Host: empty "host" means local;

more operations for independent "inline" options;

clarified options: accommodate potentially slow database connection;

minor performance tuning;

add option "build_context" in anticipation of AFP entries that require special tricks in Isabelle/ML (NB: system component settings are unavailable in AFP);

proper build_options (amending 822ddccda899);

clarified options;

proforma support for remote build hosts;

more options for performance tuning;

more operations;

support for management of build cluster;

clarified modules;

renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);

more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;

proper running limit, based on this worker process; prefer bulk jobs: much faster cancellation;

more robust: implicit locking of tables in standard order;

more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked;

removed unused "create_index": implicit index from primary_key is usually sufficient;

clarified "vacuum" (again, reverting 0bd366fad888);

clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);

update for release;

merged

more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610);

tuned signature;

proper check (amending 234f2ff9afe6);

more robust: exclude accidental nesting (synchronized block is re-entrant);

clarified errors;

removed junk (amending f8e3b228670c);

tuned output;

reuse SSH.Server connection for database server;

tuned source structure;

clarified check: uniform session_info_exists;

more complete check;

clarified signature: more specific exists_table --- avoid retrieving full list beforehand;

reuse database_server connection;

more informative trace;

reuse SSH.Server connection database server;

tuned output;

make double-sure that this is a transaction context, notably for LOCK TABLE;