tuned;

tuned signature;

clarified signature -- do not expose socket;

Removed stray 'sledgehammer' invocation

Changes to NEWS regarding 2a6ef5ba4822

Changes to complete distributive lattices due to Viorel Preoteasa

eliminiated superfluous class semiring_bits

tuned;

tuned;

update XML cache for slightly modified messages;

more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);

more options;

clarified default server name;

more uniform output: this may be parsed by another program;

clarified argument formats: explicit Unit, allow XML.Elem as well; tuned messages: prefer single quotes for JSON output;

tuned comments;

convenience to represent XML.Body as single XML.Elem;

clarified AFP partitioning;

abstract algebraic bit operations

more balanced AFP partitioning;

workaround for occasional deadlock seen in HOL-Proofs with threads=2;

adapted to 3869b2400e22;

tuned output;

more options: client without implicit server startup;

console interaction with line-editor;

more flexible message formats;

clarified interrupt handling;

clarified signature;

option for console interaction;

more uniform Bytes.read_line/read_block operations;

auto update;

more comments;

more general TTY loop;

added Reply.NOTE for asynchronous notifications;

more operations;

more thorough init: purge inactive entries;

more generous timeout;

Entry.connection: proview password here; more robust checks;

clarified initial protocol;

ignore empty lines;

tuned;

more robust read_line after shutdown;

more implicit wire protocol;

tuned signature;

clarified server start, notably for invocation within regular Isabelle/Scala process;

tuned signature;

tuned signature;

clarified toString operations;

clarified socket connection;

server commands may access Server; Server.stop: proper shutdown; clarified signature;

tuned -- avoid regex matching on potentially large string; clarified message: command name could be malformed;

more robust build: prevent problems seen with Poly/ML eb94e2820013 on Mac OS X;

clarified notion of unknown files: ignore files outside of a Mercurial repository;

more balanced AFP partitioning;

more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

tuned -- more uniform;

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

Drop rewrite rule arguments of sublocale and interpretation implementations.

more balanced AFP partitioning;

clarified signature;

build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;

more robust: normalize potentially symbolic rev;

proxy setup for lrzcloud1;

tuned signature;

support for permissive connections, for odd situations where host keys are not accepted;

proper target directory;

eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);

document existing Apache2 configuration;

consolidated main cronjob server on virtual machine together with build_log database; eliminated special tricks for Gentoo; import plain_identify logs, export all logs for backup; run build_release, build_history_base in parallel to remote_build_history tasks;

identify closer to main cronjob -- avoid diverging changeset versions;

Drop rewrites after defines in interpretations.

proper remote_mac according to Admin/Release/CHECKLIST;

more Java heap, e.g. relevant for hg.graph on Isabelle repository;

more robust check -- do not rely on return code;

more compact ML_Statistics, to make build_status work with less than 2GB heap;

retain latest ml_stats (amending e76c6cb0d461);

accomodate smaller build machine;

clarified signature;

clarified self_update: imitate visible directory state on remote side;

more operations;

self_update implies push_isabelle_home (see also 4c253e84ae62);

uniform setup_repository (pull/clone without update); tuned signature;

clarified signature: facilitate interactive experimentation;

clarified tasks;

tuned signature;

proper order;

clarified README;

merged

more ssh options;

support for proxy connection, similar to ProxyCommand in ssh config;

prefer https;

avoid hardwired parameters; less ambitious defaults: low memory requirements;

Drop illegitimate optimisation from d5a7f2c54655.

Fall back to reading rewrite morphism first if activation fails without it.

Proper rewrite morphisms in locale instances.

clarified date for presentation vs. formal pull_date;

reveal raw data in CSV format;

support for CSV files;

tuned comment;

clarified syntax: reject formal comments explicitly, instead of ignoring them silently;

merged

generalized lemmas about orthogonal transformation

more explicit infixl (see initial 1edf0f223c6e); clarified name;

clarified use of vec type syntax;

new lemma

dedicated append function for string literals

generalized

moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

merged

prefer symbols;

tuned;

more abbrevs;