merged

misc tuning and clarification;

more compact representation;

more compact representation of theory_id -- via consecutive thread-local ids;

more compact representation;

tuned signature;

more compact representation of theory_id;

tuned signature;

compact representation of sets of integers;

generated build schedule explicitly (e.g., for further analysis);

de-duplicated specification of class ring_bit_operations

de-duplicated specification of class ring_bit_operations

adjusted T_sift_down: all primitives take 0 time.

added missing file following 2702f2046afa

documented change in VeriComp

added framework-independent lemma to lift simulation to bisimulation

generalized

restructured

grouped lemmas for symbolic computations

sorted out lemma duplicates

more reactive headless server, in contrast to 15656ad28691 (when "isabelle…

tuned whitespace;

clarified modules;

clarified signature;

clarified modules;

clarified modules: Build_Log.private_data provides raw data access without…

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

clarified buffer_size;

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

merged

disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL…

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

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;

tuned

properly sort entries;

tuned;

tuned;

added publication

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…

proper filter for approximations;

proper inflection point check;

tuned;

slightly more elementary characterization of unset_bit

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;

properly incorporate running tasks into timing heuristic;

proper piecewise linear build time interpolation;

clarified ready vs. next ready;

introduced path heuristic abstraction;

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

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

more realistic timeouts for lrzcloud2:threads=1;

Remove regression test. It doesn't work if int is arbitrary precision and it…

Fix two warnings. Remove unused static definition for Real_Conv and remove…

Implement Ryu code to convert decimal representation to reals. Remove explicit…

Use word shifts for IntInf.<< if the argument is short and the highest set bit…

Remove RTS function to convert a string to a real since it's now implemented in…

Fold constant expressions involving shifts and Log2Word.

Remove PolyRealBoxedToLongInt from RTS since it's now implemented in ML.

Implement conversion to arbitrary precision within ML. There is a separate…

modernized, reordered, generalized

more correct type annotation

tuned proof

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

more realistic timeouts for lrzcloud2:threads=1;

NEWS;

update to jdk-21.0.1;

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

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

clarified toml keys operations;

tuned;

clarified toml keys: more operations;