measurability prover: removed app splitting, replaced by more powerful destruction rules

tuned warnings: observe Context_Position.is_visible;

removed unused/non-portable with_tmp_fifo;

discontinued fifo channel, always use portable socket;

tuned -- more Sidekick-friendly layout;

do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);

more explicit errors;

proper latex;

tuned -- less redundant;

proper Session.save with shutdown, which is relevant to avoid persistent threads;

tuned latex;

merged

always use socket to test performance and stability;

explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

tuned;

discontinued worker_trend: prefer constant number of active + reserve threads; tuned exceptional situations;

tuned;

added lemma

typo

avoid writing into source

clarified active_job: take dependencies into account (e.g. future based on promise);

tuned;

non-strict print_state: display old proof state on failure, e.g. unfinished command;

permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;