[isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

[Makarius]

Here is recent timing information for JinjaThreads, which indicates that
it has suffered recently:

https://isabelle.sketis.net/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_JinjaThreads

I.e. it stopped working, and came back to live much slower.


Here are some relevant changesets:

AFP/f0b5c34b4a85
user:        haftmann
date:        Mon May 07 22:07:07 2018 +0200
description:
accomodate changes in Isabelle rev. 493b818e8e10

Isabelle/493b818e8e10
user:        immler
parent:      68001:0a2a1b6507c1
date:        Wed May 02 13:49:38 2018 +0200
description:
added Johannes' generalizations Modules.thy and Vector_Spaces.thy;
adapted HOL and HOL-Analysis accordingly

Isabelle/fad29d2a17a5
parent:      68072:493b818e8e10
parent:      68070:8dc792d440b9
user:        immler
date:        Thu May 03 15:07:14 2018 +0200
merged; resolved conflicts manually (esp. lemmas that have been moved
from Linear_Algebra and Cartesian_Euclidean_Space)


That merge is a total mess -- as a consequence of disregarding long
established customs from README_REPOSITORY:

"""
Simple merges
-------------

[...]

To keep merges semantically trivial and prevent genuine merge
conflicts or lost updates, it is essential to observe to following
general discipline wrt. the public Isabelle push area:

  * Before editing, pull or fetch the latest version.

  * Accumulate private commits for a maximum of 1-3 days.

  * Start publishing again by pull or fetch, which normally produces
    local merges.

  * Test the merged result, e.g. like this:

      isabelle build -a

  * Push back in real time.

Piling private changes and public merges longer than 0.5-2 hours is
apt to produce some mess when pushing eventually!
"""


Here the private accumulation of commits has lasted approx. 2 weeks,
instead of the maximum of 3 days, on a rather hot spot in the repository.

I actually noticed that immediately, because I do check every single
merge routinely for well-formedness, to avoid merge desasters that
happen elsewhere, e.g. at Apple or the average Github project.

Now the above change in timing of JinjaThreads indicates that something
deeper might have gone wrong here -- or elsewhere -- the situation is
unclear.


Who is actually Johannes from 493b818e8e10? Maybe he can sort that out.


	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: JinjaThreads_timing.png
Type: image/png
Size: 6311 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180512/fa5470fa/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: JinjaThreads.csv
Type: text/csv
Size: 4297 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180512/fa5470fa/attachment-0001.csv>