merged

improved simp rule insert_Times_insert (following Dominique Unruh).

afford multiple tests for arm64_32-darwin on this fast machine;

proper history_base for AMR64;

tuned

more robust support for ARM64 platform;

proper support for Apple Silicon (ARM64);

merged

tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;

proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;

proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;

made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)

made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)

systematic testing of arm64_32-darwin;

more hardware details;

update to polyml-219e0a248f70, with more robust support for ARM64;

tuned generated README;

merged

Tidied up more messy proofs

hints on "hg bisect";

no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;

Removal of ugly old proofs

merged

More cosmetic changes

Cosmetic polishing of proofs

remove debug printing

merged

added mbox-like latex sugar

Added tag Isabelle2023-RC2 for changeset 53b59fa42696

prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);

revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);

output panel: don't discard already filtered messages

merged

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;