generalized

restructured

grouped lemmas for symbolic computations

sorted out lemma duplicates

more reactive headless server, in contrast to 15656ad28691 (when "isabelle dump" was important to export AFP content);

tuned whitespace;

clarified signature;

clarified modules;

clarified modules; clarified transactions;

clarified modules: Build_Log.private_data provides raw data access without transaction_lock;

more thorough transaction_lock;

obsolete, see also a5896fe040dd;

removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);

provide src/Tools/Demo as example for system component with Isabelle/Scala tool;

merged

more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);

clarified buffer_size;

merged

disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL-Analysis" on arm64_32-darwin (studio1);

workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;

tuned;

prefer Unix-domain socket on Unix;

support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;

tuned;

clarified signature: more general make_streams;

tuned;

more robust exception handling (amending 8cc1ae43e12e);

clarified signature: avoid deprecated URL constructors;

avoid deprecated URL constructors;

proper split;

properly sort entries;

tuned;

tuned;

better estimation for unknown jobs;

clarified and tuned timing estimation;

split actual approximation from data handling;

clarified timing data vs. timing entries: full top-level data view vs. dynamic partial data;

proper filter for approximations;

proper inflection point check;

tuned;

slightly more elementary characterization of unset_bit

more direct characterization of binary bit operations

tuned;

clarified timing data operations: proper estimation (instead of known points);

use proper max threads (limited by available hardware) in heuristics;

clarified time estimation: does not use config;

handle inflection point in interpolation with monotone prefix;

proper computation of sorted prefix;

better build time interpolation: model with Amdahl's law where applicable;

proper piecewise linear build time interpolation;

properly incorporate running tasks into timing heuristic;

clarified ready vs. next ready;

introduced path heuristic abstraction;

base abstract specification of NOT on recursive equation rather than bit projection

modernized, reordered, generalized

more correct type annotation

proper build with jdk-21 (amending 4fb5e6499da9);

NEWS;

update to jdk-21.0.1; enforce rebuild of Isabelle/Scala + Isabelle/ML;

rebuild jedit with minimal patch for jdk-21, following SVN 25690;

clarified modules;

suppress duplicate entries systematically using log_name: e.g. relevant for AFP;

clarified operation: pick current pull_date instead of previous one;

operations AND, OR, XOR are specified by characteristic recursive equation

clarified toml keys operations;

tuned;

clarified toml keys: more operations;

use toml key operations properly; clarified module;

clarified toml keys formatting vs. toString;

clarified keys module;

pull out toml keys module;

clarified toml parser interface;

prefer symbolic build_history_base_arm;

build_history: proper support for ISABELLE_APPLE_PLATFORM64;

clarified isabelle_hg (again, see b9d59669904a);

clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);

clarified signature: more operations and options concerning Isabelle hg;

performance tuning: cache graph;

tuned signature: fewer warnings in IntelliJ IDEA;

unused (see also 004b39bf06a5);

clarified signature and modules: more explicit Build_Log.History;

tuned: avoid recursion;

tuned;

avoid duplicate data;

output more data;

tuned whitespace;

clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;

proper ml_statistics (amending aeb511a520f4);

unify error messages;

add file information to toml parse context and error messages;

add position information to toml parser and error messages;

properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;

allow re-defining keys in toml object (already checked during parse time);

clarified toString for toml objects;

tuned

tuned message;

better invalidation for schedule cache (only on relevant changes);

tuned;

timing heuristic: parallelize more aggressively to utilize hosts fully;

proper parallel paths for timing heuristic;

scheduled build: allocate cpus more aggressively, to avoid idle threads;

finalize scheduled build only on master node;

finalize current sessions before generating schedule;

clarified signature: more operations;

NEWS

merged

tuned signature;

support for "cluster" table with "hosts" array, and params/options as for "host" table; support for "isabelle build -H cluster.name";

clarified signature: more operations, allow recursive get;

tuned signature;

tuned signature: more operations;

clarified signature;

tuned output;

more robust: prefer strict operations;

tuned message;

tuned signature: more operations;

more specific name for type class

proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);

clarified signature;

clarified modules;

clarified signature: more operations;

tuned comments;

more NEWS;

more TODO;

prefer strict test of system options;

some build cluster resources at TUM;

build cluster host specifications are based on registry entries (table prefix "host");

more robust init;

clarified signature: more operations;

support interpreted/typed entries via Registry.Category and Registry.Table;

clarified signature: more operations;

clarified output;

support for global registry;

clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";

slightly less technical formulation of very specific type class

weakened dependency

explicit type class for discrete linordered semidoms

proper dummy timing entries;

use only finished sessions in timing data;

tuned;

performance tuning for build schedule: explicit schedule generation, without mixing heuristics;

performance tuning for build schedule: faster stopping;

performance tuning for timing heuristic: pre-calculate graph operations;

move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);

clarified signature: emphasize mutable instance;

clarified signature: more operations;

support for explicit SSH hostname;

proper local host (amending 62d7ef1da441);

merged

added lemma

proper default for disjunction (amending 9f7a94117666);

tuned;

more operations;

avoid option -C: free this latter for build-related configuration;

more direct indentation, using Symbol.spaces;

clarified signature;

more accurate treatment of surrounding whitespace;

obsolete (see also f627ab8c276c);

tuned signature;

clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;

clarified modules;

tuned signature;

tuned;

proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);

more tests;

clarified exploration of history: more uniform options;

tuned;

tuned;

enable multi-builds (again, see also 0c7419d3dd59);

explore history more thoroughly;

tuned signature;

clarified "recent" time: days <= 0 means infinity (no constraint);

tuned whitespace;

proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda);

clarified signature;

tuned output;

tuned;

tuned message;

proper option;

merged

proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1; ensure connection defaults required for string literals;

Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family

merged

prefer Time.scale(), following Isabelle/ML;

proper benchmark command;

merged

proper progress (see also 45d570945fe4);

improved build messages;

clarified;

merged

fixed the simplification of Suc n - 1

tuned whitespace;

tuned message;

just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);

more detailed progress for build_log_database, to see better what happens when;

clarified signature: explicit Progress date;

more uniform progress;

more robust: support concurrent output;

disable multi-builds (again): does not quite work yet;

clarified modules;

clarified signature;

clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);

tuned signature;

proper Compress.Cache;

clarified signature;

more parallelism via consumer thread: with mailbox limit to avoid ressource problems;

support for mailbox limit;

tuned signature;

discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;

clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);

afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb); proper history_base for ARM;

performance tuning: parallel and incremental update of build_log_database;

performance tuning: more careful database access;

clarified message;

tuned signature;

tuned;

prefer old-style import "=>";

merged

redundant (see also 3069da1743bc);

removed obsolete table (see also 6acd1a2bd146);

more robust init_database(); proper treatment of views, not tables (amending dd350a41594c);

proper private_data.transaction_lock; prefer execute_batch_statement;

clarified names;

proper support for SSH;

tuned signature;

tuned imports;

add module for faster scheduled builds;

always use host database and make protected;

read relative cpu from build log;

prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);

added start date to build jobs, e.g., for build time estimation;

added initial version of benchmark module, e.g., to compare performance of different hosts; added benchmark operation to build cluster;

generalized node infos: allow addressing of numa node segments via relative cpus; add more node options and process policy options using taskset as alternative to NUMA for more fine-grained cpu controls (e.g., for cpus with heterogeneous cores in the same NUMA segment);

add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);

added Range object to Host, e.g. to parse/unparse NUMA node ranges;

defined statically known tables of Build_Log; read hostname from build logs, store in Session_Entry (e.g., to track hosts in distributed build);

added lemma

added lemma

added lemma

NEWS and CONTRIBUTORS;

remove unused ci-extras component;

use mail module in CI build;

added mail module;

build javamail component and add to main components;

added component for javax mail;

updated to vampire-4.8;

tuned README;

update Vampire version, following hints by Martin Desharnais;

removed junk;

tuned component_vampire script for Vampire 4.8 and added new flag to force version name

prefer Isabelle options for CI mail settings over ci.properties;

Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.

proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);

unused (see fe9e590ae52f);

clarified modules;

merged

update documentation on simproc_setup;

tuned;

proper morphism;

simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);

more compact ML source;

more robust read_simproc_spec: proper error positions;

tuned signature;

more standard simproc_setup using ML antiquotation;

more standard simproc_setup using ML antiquotation;

more standard simproc_setup using ML antiquotation;

added ML antiquotation "simproc_setup";

clarified signature;

clarified signature; clarified modules;

tuned signature;

tuned signature;

clarified signature;

clarified syntax and order of parameters;

clarified signature: Named_Target.setup works both for global and local theory;

clarified signature; clarified modules;

clarified signature: more concise simproc setup in ML;

clarified signature: more concise variations on implicit theory setup;

clarified simproc_setup (passive);

clarified 'simproc_setup';

support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);

more standard simproc_setup in Isar; recovered examples from dead comments;

more standard ML setup; proper tracing messages depending on context option, not Unsynchronized.ref; tuned whitespace;

proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0

added new portfolio for Vampire 4.8

tuned signature, following Isabelle/Scala;

more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;

tuned;

proper parallel build tasks;

more Haskell tests on macOS;

more NEWS;

disable naproche component for now: to be updated before the next Isabelle release;

updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell"); enforce rebuild of Isabelle/Pure and thus all Haskell applications;

more NEWS;

tuned structure;

update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;

updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur;

proper options for macOS 11 Big Sur;

support for official release of polyml-5.9.1;

updated Linux baseline to Ubuntu 18.04;

support for macOS 14 Sonoma (only for testing);

more platform tests: initial support for macOS 14 Sonoma;

updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;

merged

prefer Exn.result: avoid accidental capture of interrupts, similar to ML;

clarified user errors vs. failures, e.g. java.lang.StackOverflowError;

further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;

proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);

distinguish proper interrupts from Poly/ML RTS breakdown;

tuned;

tuned;

proper Isabelle_Thread.try_catch;

tuned;

proper Exn.capture / Isabelle_Thread.try_catch;

tuned;

clarified signature;

proper Exn.capture;

more robust: avoid race condition;

clarified name;

clarified signature;

clarified comments;

Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts

atin now an abbreviation for atin_within, which has been moved to Abstract_Limits

merged

New proofs also some slightly faster existing proofs

updated to hugo-0.119.0;

add component build tool for hugo from afp-devel;

removed test failing on some platform

mini2 is not active due to upgrade;

more PLATFORMS;

update documentation on Isabelle/ML exceptions;

misc tuning;

discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);

proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);

proper Scala version, e.g. for IntelliJ IDEA;

NEWS

used standard Time.compare in Sledgehammer's preplay

moved variable bindings to tighter scope

removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer

removed unused function parameter

merged

A couple of new lemmas

merged

more NEWS;

explicitly reject 'handle' with catch-all patterns;

avoid accidental 'handle' of interrupts;

tuned: prefer try-catch/finally over low-level 'handle';

clarified treatment of exceptions: avoid catch-all handlers;

clarified output vs. error: presence of error messages means error (see also cb7264721c91);

tuned;

more robust management of resources, using Thread_Attributes.uninterruptible;

tuned;

clarified signature;

more robust management of resources, using Thread_Attributes.uninterruptible;

tuned;

tuned;

tuned signature;

clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);

clarified signature;

clarified modules;

unused;

clarified order of modules: early access to interrupt management of Isabelle_Threads;

tuned: prefer antiquotation for try-catch;

tuned: prefer antiquotation for try-catch;

tuned: prefer antiquotation for try-finally;

omit pointless capture/release (see also 469a375212c1);

omit pointless capture/release (see also 26774ccb1c74);

clarified signature: avoid association with potentially dangerous Exn.capture;

more robust: catch/finally part is uninterruptible;

more position information, e.g. for warning about fn-pattern;

unused;

more general ML_Antiquotation.special_form; more general "try" forms: support 'finally' or 'catch';

Importing or moving a few more useful theorems

merged

A few new theorems

avoid legacy binding errors in Sledgehammer Isar proofs

parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition

added argo

allow (~) syntax in TPTP proofs for unapplied negation

reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs

use same associativity as Isabelle when parsing HOL proofs

improved Sledgehammer's HOL proof parser w.r.t. negation

clarified signature;

clarified signature;

clarified signature;

minor performance tuning;

merged

A few new or simplified proofs

tuned: more standard order;

clarified signature; update component;

proper fontenc for cartouches (amending d052d61da398);

clarified modules; clarified signature;

clarified signature;

clarified modules;

tuned;

more robust: prefer linear data flow;

added first proof reconstruction test for Sledgehammer

tuned;

clarified signature;

clarified signature (again): follow Isabelle/Java/Scala;

tuned (following 69c6d3e87660);

tuned --- avoid pointless indirection (see also a2df9de46060);

(pointlessly) get rid of some simp calls within "proof"

reduced prominence of lemma names

new formulation of an auxiliary lemma

A few more inclusion-exclusion theorems from HOL Light

Corrected type calculation.

some hints on managed installations

prefer cartouches over quotes for clarity of resulting document

A little reorganisation

post-release updates;

merged

Added tag Isabelle2023 for changeset b5f3d1051b13

tuned;

misc tuning;

documentation for the "Document" panel in Isabelle/jEdit;

Loads of new material related to porting the Euler Polyhedron Formula from HOL Light

merged

merged

tidying up old apply-style proofs

allow higher-order unification of open terms (reviewed by Larry Paulson)

merged

clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;

add ML_system_pp for type Isabelle_Thread.T;

more explicit type Isabelle_Thread.T; total operation Isabelle_Thread.self: upgrade raw ML threads implicitly;

discontinue somewhat pointless thread tracing/debugging: without PIDE command context, messages are not shown, and Exn.trace hardly works anyway (see also de20fccf6509 and 447972249785); prefer Isabelle_Thread.fork;

tuned whitespace;

tuned Sledgehammer messages

respect timeout better

merged

Added tag Isabelle2023-RC5 for changeset ffa417b5c913

tuned;

tuned messages;

proper stop of build_process shutdown, despite errors on workers;

prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;

support "isabelle build_worker -q";

support "isabelle build_process -r -f";

clarified signature;

clarified output;

clarified signature;

clarified signature: removed ununsed option;

tuned message;

updated to naproche-20230902: add examples/100_theorems.ftl.tex and some more text in Isabelle/Intro.thy;

more robust access to output file of external smt, notably for Windows 11, where transient ERROR_SHARING_VIOLATION has been seen;

more robust $ISABELLE_TMP_PREFIX on windows: avoid location within Cygwin root, i.e. inside the program directory (see also ff92d6edff2c and 1df53737c59b);

more robust $TMPDIR on windows, e.g. for repository snapshot: do not depend on $TEMP_WINDOWS provided by official distribution;a

more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;

more accurate documentation of record field update, following changes in Isabelle2007 and Isabelle2008;

tuned whitespace;

more robust: "hostname" command might be absent, notably on Arch Linux (and other systemd-based distributions);

tuned NEWS;

NEWS;

update to "scalac -source 3.3" (from 3.1); enforce rebuild of Isabelle/ML and Isabelle/Scala, e.g. for session HOL-Codegenerator_Test;

proper pattern (amending ff86f10e54cd);

discontinue odd AFP partitioning: let Build_Cluster / Build_Engine do the job;

discontinue special treatment of AFP: "isabelle dump" has been superseded by regular "isabelle build" databases;

clarified signature: prefer enum types;

proper type, following Bus.event;

clarified signature;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

tuned indentation;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified signature: prefer enum types;

clarified generated Scala, for the sake of "scalac -source 3.3";

discontinue old Java 11 LTS;

misc tuning: support "scalac -source 3.3";

obsolete (see b4e6b82fdb9e);

merged

update for release;

Added tag Isabelle2023-RC4 for changeset 12aac1489f3b

minimal documentation for build cluster support;

more robust access to local variables;

tuned messages: avoid duplicates;

removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);

tuned error;

tuned messages (again);

tuned: prefer explicit types;

support for Host.dirs;

tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;

support multiple host names;

clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;

avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer

tuned message;

tuned;

more accurate treatment of state vs. serial vs. db;

more explicit check;

proper numa_nodes for build_worker;

tuned message;

tuned;

tuned signature;

support hosts with shared directory (e.g. NFS);

tuned message: failure may stem from build_cluster init;

proper sync_database for receive timeout;

clarified source structure;

tuned whitespace;

clarified command-line tools;

tuned output;

clarified signature;

tuned signature;

tuned signature;

proper sequential evaluation;

more robust command options;

performance tuning: avoid redundant db access;

clarified signature: proper treatment of implicit state (amending d0c9d277620e);

performance tuning: avoid redundant db access;

performance tuning: avoid multiple db roundtrips;

clarified signature: more robust treatment of implicit state;

proper sync_database for Database_Progress consumer; more efficient (but less reactive) Database_Progress.stopped;

tuned message;

tuned;

tuned messages;

tuned signature: removed unused arguments;

minor performance tuning: avoid multiple db roundtrips;

more operations;

tuned;

limit size and complexity of bulk transactions;

more scalable write_entries and Export.consumer via db.execute_batch_statement;

clarified signature: filter batch;

more scalable write_messages via db.execute_batch_statement;

support for execute_batch: multiple statements in one round-trip;

more robust;

restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;

more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;

clarified main_loop: support timeout, which results in consume(Nil);

tuned;

clarified signature;

tuned signature;

tuned signature;

build_worker is stopped independently from master build_process;

clarified command arguments: optionally restrict to given theories (from theory loader);

tuned signature: more operations for formal theory context vs. theory loader;

added Isar command 'print_context_tracing';

avoid confusion: this is merely about "isabelle dotnet_setup", no codegen yet;

avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer

merged

some refinements in Algebra and Number_Theory

provide Go component

merged

A subtle fix involving the "measurable" attribute

merged

Numerous minor tweaks and simplifications

substantial tidy-up, shortening many proofs

add Go component

backed out changeset 2a26d423d9fb: build_log_database not run yet, so this tests the same changesets again;

back to post-release mode -- after fork point;

Added tag Isabelle2023-RC3 for changeset f5fb5bb2533f

clarified option name (see also ff43a524aa5d);

more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;

more robust: atomic file-system result via tmp file;

removed junk (amending 8cd399b25dac);

more robust wrt. undefined state;

more informative error;

more robust;

tuned signature;

clarified signature: more explicit types;

more informative shasum: show differences explicitly;

tuned messages;

more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere;

clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;

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;

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;

more robust Java/Scala multithreading: transaction is always connection.synchronized;

clarified signature: proper Scala function for command-line tool;

tuned signature;

clarified signature: more operations;

more standard time unit;

clarified options;

tuned output;

global transaction_count;

tuned output;

tuned output;

prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job");

clarified isabelle.transaction_log: support time_min (in ms);

more operations;

more informative trace;

support trace of transaction_lock via property "isabelle.transaction_log";

proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67);

tuned;

proper close() operation;

tuned comments;

more robust: avoid nested transactions (on disjoint tables);

potentially more robust: long-running operation only for build master, not workers;

less ambitions transactions (amending 3f3dcf9f53f1): TRANSACTION_SERIALIZABLE may lead to spurious rollback exceptions;