update to scala-3.3.3; enforce rebuild of Isabelle/Scala + Isabelle/ML;

provide e-3.0.03 on all platforms, including arm64-linux and arm64-darwin --- still inactive;

update NEWS, following 0d7c7fe65638;

provide cvc5-1.1.1 for testing --- still inactive;

rebuild bash_process executables on current reference platforms, including native arm64-darwin; enforce rebuild of Isabelle/Scala + Isabelle/ML;

tuned NEWS, see also c62003e05e46;

update NEWS, following ea1913c953ef;

tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";

more explicit NEWS (see 3648e9c88d0c);

NEWS for a53287d9add3, 3e30ca77ccfe;

add option for unify trace (now disabled by default as printing is excessive and rarely used);

tuned unify trace option names;

more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche;

updated to stack-2.15.1, lts-22.6, ghc-9.6.3;

merged

tuned name

new simplifier trace_op for tracing simproc calls

merged

Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers

support Zipperposition's skolemization in generated Isar proofs

improved output in simps_case_conv;

improved output in inductive module;

simplifier: no trace info from simprocs unless simp_debug = true.

deal with new-style Vampire skolemization in reconstructed Isar proofs

database performance tuning: prefer light-weight IPC over heavy-duty transactions;

tuned signature; tuned output;

tuned signature: follow PostgreSQL syntax instead of JDBC API;

more robust shutdown: interruptible database connection;

clarified signature: more convenient send/receive operations;

clarified versions for documentation;

merged

clarified signature: avoid hardwired values;

clarified IPC via database server: receive notifications quasi-spontaneously via auxiliary thread;

minor performance tuning: just 1 transaction for slices <= 1;

tuned;

tuned whitespace;

tuned signature;

clarified signature: fewer warnings in IntelliJ IDEA;

removed unused database_server (amending 32ca3d1283de);

timing function generation bug fix by Jonas Stahl

tuned signature: more types, fewer warnings in IntelliJ IDEA;

new less ad hoc implementation of the 'moura' tactic for skolemization

more thorough Store.clean_output (amending 1fa1b32b0379);

clarified signature: Build_Process tells how to clean sessions;

clarified signature;

tuned;

tuned;

minor performance tuning;

tuned;

tuned signature;

tuned, following 7a1153c95bf9;

merged

tuned signature: fewer warnings in IntelliJ IDEA;

proper usage;

recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;

clarified signature;

more robust: make double-sure that heap digest is present;

tuned;

minor performance tuning: just one transaction for log_db without heap;

tuned;

proper store.cache.compress;

tuned whitespace;

clarified store_session: heap requires process_result.ok, but log_db is always stored; clarified ML_Heap.clean_entry vs. ML_Heap.init_entry;

unused;

tuned;

tuned names;

tuned names;

clarified database layout;

tuned signature; tuned messages;

clarified signature;

more accurate types;

build local log_db, with store/restore via optional database server; tuned messages;

propagate property "isabelle.debug", notably for Java/Scala exception trace;

tuned;

proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);

clarified signature; more robust slice_size;

clarified names;

more explicit build_cluster flag to guard open_build_database server;

tuned;

clarified signature;

simplified specification of type class semiring_bits

New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl

merged

A small collection of new and useful facts, including the AM-GM inequality

remove selected occurrences of 'moura' tactic

added lemmas relpowp_left_unique and relpow_left_unique

added lemmas relpowp_right_unique and relpow_right_unique

use define_time_fun

time funs: +1 instead of 1+

minor performance tuning;

clarified signature: more comprehensive operations;

clarified signature: more explicit types;

clarified signature: emphasize physical db files;

tuned: afford untyped/unscoped update;

clarified signature: avoid ill-defined type java.net.URL;

unused;

tuned: afford untyped/unscoped update;

more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;

clarified signature: more explicit types/scopes;

tuned names;

tuned;

tuned documentation;

more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;

clarified modules: centralize default policy;

more explicit types --- fewer warnings in IntelliJ IDEA;

tuned: avoid shadowing of names;

clarified default "isabelle build -j0 -H";

tuned whitespace;

clarifier worker vs. master, which may coincide for local build;

clarified signature: more standard defaults;

clarified signature;

clarified signature;

tuned;

prefer static object, while class is required for "services";

clarified signature: prefer default;

merged

tuned;

more robust: check subclasses as well;

more robust;

support for alternative user home, e.g. to avoid slow NFS shares;

support explicit USER_HOME within SSH session;

tuned;

merged

Further adjustments to the syntax for Lebesgue integration

tuned comments;

more robust: always close, despite failure;

clarified signature;

tuned signature;

tuned comments;

clarified signature;

Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury

tuned whitespace;

prefer static object, while class is required for "services" (see 47eb96592aa2);

clarified directories; clarified names;

tuned signature;

tuned: prefer explicit update operation for immutable options;

tuned message;

more robust type, with explicit default;

tuned usage message;

clarified signature;

more robust defaults;

merged

added lemmas relpow_trans[trans] and relpowp_trans[trans]

more on disjunctive addition/subtraction

merged

prefer physical processors (see also 4b014e6c1dfe and 26a43785590b);

more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");

more robust default;

more accurate, notably on lxbroy10 and vmnipkow9;

clarified num_processors: follow Poly/ML (with its inaccuracies);

clarified modules, following Isabelle/ML;

clarified signature;

tuned comments;

merged

the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses

merged

A few lemmas brought in from AFP entries

merged

made destructor-view tactic more robust (by Jan van Brügge)

performance optimization;

clarified names;

clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);

proper "linux_arm", amending 76ad72736e9e;

more lemmas

new lemmas involving Ramsey numbers, infinite sets

simplified class specification

Removal of duplicate code

Two new theorems

more lemmas and more correct lemma names

NEWS: corrected the definition of convexity of functions

Further lemmas concerning complexity and measures

Correct the definition of a convex function, and updated the proofs

merged;

update to windows_app-20240205, with executables for linux, linux_arm, macos;

omit redundant options;

tuned README;

uniform build of binutils for linux, linux_arm, macos;

fix reconstruction of Alethe's and_pos rule

added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult

proper target option, following package binutils-mingw-w64-x86-64 from Debian/Ubuntu;

updated windows_app based on launch4j-3.50-linux-x64, without rebuilding GNU binutils (missing COFF target pe-i386);

proper sfx_archive_name;

clarified options;

more robust;

build Isabelle windows_app component from GNU binutils and launch4j;

proper windows_app/launch4j-linux_arm;

merged

A small number of new lemmas

explicit reference to code_dt

made lift_bnf more robust for abstract types with 'phantom' type variables

rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO"; uniform baseline for "linux" and "linux_arm";

proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);

proper bash syntax (amending 0631dfc0db07);

tuned proof: avoid z3;

tuned proof: avoid z3 to make it work on arm64-linux;

tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;

merged

more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);

strengthened class parity

proper accessible paths for web server;

more informative message (amending b8a6b2ec85a2);

merged

more robust: do not affect "$ISABELLE_HOME_USER/contrib" on master node;

avoid excessive ML heap on this 16GB node;

more robust (amending c9774306a879);

proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;

clarified symbolic host name;

allow remote_build on this host (server-arm), without conflicts of this "isabelle_self";

more robust message;

A few more new theorems taken from AFP entries

merged

define_time_function: avoid unused let's

common type class for trivial properties on div/mod

more robust (amending 1600fb749c54), to support the following corner case: schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))" apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>) oops

proper test options;

proper history_base for linux_arm;

updated to PostgreSQL 12 on Ubuntu 20.04; more accurate command-line;

routine build + test for linux_arm;

disable test on "augsburg1": machine will be dismantled;

add approximation factors in build schedule to estimate build times more conservatively;

merged

Type class patch suggested by Achim Brucker, plus tidied lemma

rearranged and reformulated abstract classes for bit structures and operations

Three new lemmas

tuned proof: avoid z3 to make it work on arm64-linux;

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

make build process state protected to avoid copying in subclasses (e.g. for database connections);

add build_sync tag to sync certain options (e.g., build_engine) across build processes;

clarified Mercurial version: presumably the last version that supports both python2 and python3;

more robust: avoid crash on non-Linux systems;

clarified webserver names;

proper Apache.php_name;

proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);

tuned source structure;

more robust systemd configuration;

more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";

tuned whitespace in generated file;

tuned;

clarified modules;

recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);