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;