merged

detect old log files (early 2016);

explicit support for multiple regexes;

some derived data fields, to facilitate queries;

tuned signature;

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.VldMQI

Simplification of some proofs. Also key lemmas using !! rather than ! in premises

more general pattern;

more timing;

proper quote (amending 546020a98a91): e.g. relevant for "ISABELLE_BUILD_OPTIONS";

suppress build_log_snapshot: too bulky;

more Jenkins logs for build_log database;

approximate repository identify job based on isabelle-nightly-slow; more Jenkins changeset patterns found in the wild;

tuned;

tuned signature;

clarified treatment of qualified names (amending 7ef438495a02);

create full view on build_log data, but avoid bombing sqlitebrowser;

support for views;

more operations; tuned;

slightly more compact file;

incremental download of Jenkins log files, which are also added to database;

more robust detection of Jenkins log;

detect Jenkins log files as well;

detect host name;

more parallelism;

tuned;

proper log_path check; report progress;

ensure canonical order: latest first;

tuned signature;

download Jenkins logs with inlined ml_statistics;

tuned;

clarified signature;

tuned signature;

read ml_statistics from session logs: .db or .gz files;

more informative log_filename;

retrieve more than just 100 builds;

clarified modules;

tuned signature;

tuned signature;

clarified database update: full ml_statistics on server, no ml_statistics on plain file;

parse ml_statistics only when required;

clarified database layout: bulky ml_statistics are stored/retrieved separately;

support for qualified names, which are not quoted (e.g. for SQLite); more operations;

clarified dummy Session_Entry;

clarified database update operations; more efficient log_file processing; tuned;

tuned message;

maintain build_log database;

exclude special log files;

tuned;

tuned;

ssh_close for proper termination after use of database;

some documentation;

merged

tuned;

tuned signature;

clarified database content;

more operations;

optional ml_statistics: much faster;

proper query (amending ce15da15f8e2);

put bulky data last;

tuned;

more log files;

clarified multi-line properties;

dummy session entry for empty build_info: relevant for filter_files;

tuned query, notably for isabelle_build_log_build_info;

operations to read database;

tuned signature: less overloading;

tuned signature;

tuned transaction granularity;

unused;

clarified database layout;

tuned signature: avoid null in regular Scala code;

clarified transaction boundaries: more robust incremental write operations;

clarified database layout;

allow null for primitive types;

more uniform storage of Meta_Info;

allow null;

clarified plain_name / log_name;

tuned comment;

tuned signature;

tuned;

separate small meta_info vs. big build_info;

tuned;

unused;

tuned signature;

more standard multi-line storage in database: Prop.separator is only required for single-line meta_info within log file;

clarified filter_files: sorted and unique;

database storage of Meta_Info and Build_Info;

allow null;

more encode/decode operations;

proper prefix;

support for database connection;

clarified treatment of default port;

tuned signature;

clarified modules;

more SQL operations;

more robust (see also 6688b9cd443b);

more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;

clarified signature;

New material (and some tidying) purely in the Analysis directory

Merge

Some fixes related to compactE_image

Merge

Further new material. The simprule status of some exp and ln identities was reverted.

tuned Approximation: separated general material from oracle

better code equation for binomial

meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;

Fixed LaTeX issue

New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

instance for polynomial rings with characteristic zero

recovered document from 0f3fdf689bf9;

tuned;

clarified parent session images, to avoid duplicate loading of theories; avoid name conflict with loaded theory src/HOL/Library/Parallel.thy;

clarified parent session images, to avoid duplicate loading of theories;

clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;

clarified modules;

actually use theory;

clarified parent session images, to avoid duplicate loading of theories;

merged

tuned documentation;