drop unused Task.info field;

proper guard_time (amending 752806151432);

proper dynamic access (amending c3f07c950116);

more robust, notably for remote process (via SSH);

prefer dynamic objects, following a5fda30edae2;

proper dynamic access (amending 52b5c7c8e6d9);

clarified signature: incorporate guard into Logger;

merged

added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp

Moving valuable library material from Martingales into the distribution

clarified signature; sleep unconditionally: avoid aggressive database access;

clarified module signature and state;

tuned messages;

omit somewhat pointless message, following b7187d4cdf68;

more robust handling of uninitialized value, notably Build_Process.progress;

tuned

partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;

clarified module signature and state;

tuned signature: more protected operations;

database performance tuning: just one synchronized_database for main loop body;

tuned;

more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);

more robust: imitate Isabelle/ML operation more closely (after 26a43785590b); logical_cores is e.g. relevant for server-arm.sketis.net, where /proc/cpuinfo looks quite different;

tuned;

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

official support for arm64-linux, despite a few missing tools;

discontinue unstable z3-4.4.1 for arm64-linux from Debian (in contrast to 796ae338eb9d and 87718883c8b9);

proper platform_name/platform_dir for native arm64-darwin: already published in 788f11af9822 after manual adjustment;

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;