Re: [isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

On 10/05/18 00:10, Makarius wrote:
> 
> In the past couple of weeks I have sporadically tried to work around
> this resource problem, but failed so far.
> 
> The latest attempt is Isabelle/f6a22490cca8. As usual, it "works for me
> on my usual test machines", but there is a remaining chance of problems
> coming back on other configurations.

So far this change looks good on various test machines with only 2 cores.

In Isabelle/a8f40dd73c61 I have made the parallelism a little bit more
ambitious, and keep watching resulting performance charts at
https://isabelle.sketis.net/devel/build_status

All this are just workarounds to get back into a situation where all
sessions work routinely most of the time.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

[Makarius]

On 11/05/18 14:12, Lars Hupel wrote:
>> Last known good state is:
>>
>> Isabelle/7e349d1e3c95
>> AFP/c3cfeceda7a0
> 
> We're back to normal now, as of
> 
> Isabelle/58c9231c2937
> AFP/79f64c92d5ae

Great. I had already started some experiments, but they were inconclusive.

Just for the record, the relevant point seems to be

changeset:   9230:b0febe244fbc
user:paulson 
date:Fri May 11 12:12:01 2018 +0100
files:
thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics.thy
description:
fix to nonterminating proof


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Algebra

[Makarius]

On 08/05/18 13:49, Lawrence Paulson wrote:
> I have two interns from École Polytechnique. They have been going over 
> HOL-Algebra and Group-Ring-Module, providing new proofs of the best results 
> in the latter and tidying up some messy proofs in the former, as well. They 
> are also systematising the chaotic naming conventions that they found there. 
> So there will be big changes to HOL-Algebra in the coming weeks. This is an 
> early warning in case anybody else wants to work on this directory.

Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to
my information, Clemens Ballarin has taken great care about HOL-Algebra
over many years (even with contributions by students).

Beyond that, I am just hoping that we are not sliding into the "best
practices" of the average Github project, with huge commits / merges
coming out of the blue, which are hard to understand later.

Both the sources and their history need to be readable, in order to sort
out subtle problems. These days I read history even more often than the
latest version of the sources.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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
session_name,chapter,pull_date,afp_pull_date,isabelle_version,afp_version,timing_elapsed,timing_cpu,timing_gc,ml_timing_elapsed,ml_timing_cpu,ml_timing_gc,maximum_heap,average_heap,stored_heap,status
JinjaThreads,AFP,2018-05-11 00:18:11,2018-05-11 00:39:55,53b4e204755e,2d77f99edaa7,3811000,15245000,0,3808303,15174304,2981372,29998,23800,0,finished
JinjaThreads,AFP,2018-05-10 00:18:13,2018-05-10 00:39:50,f6a22490cca8,c3cfeceda7a0,3881000,15261000,0,3878227,15190920,2981832,29998,23891,0,finished
JinjaThreads,AFP,2018-05-09 00:40:12,2018-05-09 00:40:12,2b18a770911f,f0b5c34b4a85,0,0,0,0,0,0,0,0,0,failed
JinjaThreads,AFP,2018-05-08 00:18:06,2018-05-08 00:40:17,2277fe496d78,4a788844049b,0,0,0,0,0,0,0,0,0,failed
JinjaThreads,AFP,2018-05-07 00:18:09,2018-05-07 00:39:33,0b66aca9c965,ba558fdf522c,0,0,0,0,0,0,0,0,0,failed
JinjaThreads,AFP,2018-05-05 00:18:07,2018-05-05 00:39:54,b25ccd85b1fd,ad1d95d5ace6,0,0,0,0,0,0,0,0,0,failed
JinjaThreads,AFP,2018-05-05 00:18:07,2018-05-05 00:18:07,b25ccd85b1fd,ba558fdf522c,0,0,0,0,0,0,0,0,0,failed
JinjaThreads,AFP,2018-05-04 00:18:04,2018-05-04 00:39:39,262b42b59151,8527935d1eed,0,0,0,0,0,0,0,0,0,failed
JinjaThreads,AFP,2018-05-03 00:40:00,2018-05-03 00:40:00,b91c4acc1aaf,8c085909633b,3165000,12646000,0,3162156,12574516,2801764,29998,21509,0,finished
JinjaThreads,AFP,2018-05-02 00:18:06,2018-05-02 00:18:06,3931ed905e93,8c085909633b,3128000,12563000,0,3124754,12491468,2732000,29998,22012,0,finished
JinjaThreads,AFP,2018-05-01 00:39:45,2018-05-01 00:39:45,7811d8828775,83c48344a96f,3243000,12827000,0,3239810,12754096,2889224,3,20947,0,finished
JinjaThreads,AFP,2018-04-30 00:18:26,2018-04-30 00:40:00,9e077a905209,d2059b336ac3,317,12667000,0,3167328,12594812,2825924,29998,20967,0,finished
JinjaThreads,AFP,2018-04-29 00:18:24,2018-04-29 00:40:00,ebd179b82e20,5d888a880328,3055000,12456000,0,3051605,12385484,2721852,29998,21528,0,finished
JinjaThreads,AFP,2018-04-28 00:18:28,2018-04-28 00:39:53,e98988801fa9,f0759507c46c,3119000,12532000,0,3116529,12458624,2758092,29998,21543,0,finished
JinjaThreads,AFP,2018-04-27 00:18:31,2018-04-27 00:40:52,f76e8180c498,6dacb8b19575,3076000,12474000,0,3073260,12403568,2764588,2,21361,0,finished
JinjaThreads,AFP,2018-04-26 00:18:14,2018-04-26 00:40:14,d45b78cb86cf,ba5034372e45,316,12671000,0,3157443,12598864,2815876,29998,21567,0,finished
JinjaThreads,AFP,2018-04-24 00:18:31,2018-04-24 00:18:31,75130777ece4,efd58f8b1659,3143000,12634000,0,3140387,12558468,2761616,2,21852,0,finished
JinjaThreads,AFP,2018-04-23 00:18:24,2018-04-23 00:18:24,c8a506be83bd,efd58f8b1659,3149000,12548000,0,3146387,12476560,2641532,29998,22324,0,finished
JinjaThreads,AFP,2018-04-22 

[isabelle-dev] Slowdown of ConcurrentGC

[Makarius]

The Isabelle/AFP timing charts show a recent slowdown of ConcurrentGC:

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

See also the attached copies of the chart and data file (the web version
updates itself dynamically). At the transition of Isabelle/75130777ece4
to d45b78cb86cf there is a notable change of string type representation
in HOL (by Florian Haftmann).

My impression is that the overall slowness of ConcurrentGC is due to its
rather aggressive use of string literals (and disjunctions over them).
So a small change in the representation can have a big impact here, and
there might be not proper way around it.

I am posting this observation here nonetheless, in the hope that it
could be still improved.


Makarius
session_name,chapter,pull_date,afp_pull_date,isabelle_version,afp_version,timing_elapsed,timing_cpu,timing_gc,ml_timing_elapsed,ml_timing_cpu,ml_timing_gc,maximum_heap,average_heap,stored_heap,status
ConcurrentGC,AFP,2018-05-11 00:18:11,2018-05-11 00:39:55,53b4e204755e,2d77f99edaa7,9419000,30025000,0,9415959,30023100,1907620,10933,7817,0,finished
ConcurrentGC,AFP,2018-05-10 00:18:13,2018-05-10 00:39:50,f6a22490cca8,c3cfeceda7a0,9505000,30094000,0,9502443,30091596,2149764,10649,7342,0,finished
ConcurrentGC,AFP,2018-05-09 00:40:12,2018-05-09 00:40:12,2b18a770911f,f0b5c34b4a85,9655000,30126000,0,9652887,30123908,2133668,9412,5266,0,finished
ConcurrentGC,AFP,2018-05-08 00:18:06,2018-05-08 00:40:17,2277fe496d78,4a788844049b,9491000,29751000,0,9488339,29749640,2028628,10380,5722,0,finished
ConcurrentGC,AFP,2018-05-07 00:18:09,2018-05-07 00:39:33,0b66aca9c965,ba558fdf522c,959,30077000,0,9587001,30074596,2088648,9111,5544,0,finished
ConcurrentGC,AFP,2018-05-05 00:18:07,2018-05-05 00:39:54,b25ccd85b1fd,ad1d95d5ace6,993,30837000,0,9927226,30835360,2350904,9053,5058,0,finished
ConcurrentGC,AFP,2018-05-05 00:18:07,2018-05-05 00:18:07,b25ccd85b1fd,ba558fdf522c,9733000,30766000,0,9730146,30763944,2195328,9579,6815,0,finished
ConcurrentGC,AFP,2018-05-04 00:18:04,2018-05-04 00:39:39,262b42b59151,8527935d1eed,9473000,29794000,0,9470880,29792080,2049904,9119,5590,0,finished
ConcurrentGC,AFP,2018-05-03 00:40:00,2018-05-03 00:40:00,b91c4acc1aaf,8c085909633b,9635000,3004,0,9632922,30037860,2216072,9042,5140,0,finished
ConcurrentGC,AFP,2018-05-02 00:18:06,2018-05-02 00:18:06,3931ed905e93,8c085909633b,955,30187000,0,9547094,30184516,2077948,9875,7086,0,finished
ConcurrentGC,AFP,2018-05-01 00:39:45,2018-05-01 00:39:45,7811d8828775,83c48344a96f,938,29263000,0,9377459,29261500,1923772,10412,6441,0,finished
ConcurrentGC,AFP,2018-04-30 00:18:26,2018-04-30 00:40:00,9e077a905209,d2059b336ac3,9597000,29982000,0,9594967,29979888,2119664,10292,5485,0,finished
ConcurrentGC,AFP,2018-04-29 00:18:24,2018-04-29 00:40:00,ebd179b82e20,5d888a880328,9622000,29991000,0,9619983,29989176,2178860,9115,5230,0,finished
ConcurrentGC,AFP,2018-04-28 00:18:28,2018-04-28 00:39:53,e98988801fa9,f0759507c46c,9318000,29461000,0,9315451,29459256,1890596,11199,8016,0,finished
ConcurrentGC,AFP,2018-04-27 00:18:31,2018-04-27 00:40:52,f76e8180c498,6dacb8b19575,918,29103000,0,9177587,29101188,1867552,10893,7873,0,finished
ConcurrentGC,AFP,2018-04-26 00:18:14,2018-04-26 00:40:14,d45b78cb86cf,ba5034372e45,9336000,2953,0,914,29527536,1824824,10972,8041,0,finished
ConcurrentGC,AFP,2018-04-24 00:18:31,2018-04-24 00:18:31,75130777ece4,efd58f8b1659,8515000,26414000,0,8512839,26412460,1702600,9317,6766,0,finished
ConcurrentGC,AFP,2018-04-23 00:18:24,2018-04-23 00:18:24,c8a506be83bd,efd58f8b1659,8463000,26393000,0,8460524,26391036,1774012,8780,6000,0,finished
ConcurrentGC,AFP,2018-04-22 00:18:27,2018-04-22 00:40:19,b91a043c0dcb,b6b5f48aa576,853,26929000,0,8527717,26926600,1786652,9153,6799,0,finished
ConcurrentGC,AFP,2018-04-21 00:18:17,2018-04-21 00:40:10,32d19862781b,4bf3efef63d6,8266000,25957000,0,8263230,25954752,1646084,8637,5570,0,finished
ConcurrentGC,AFP,2018-04-20 00:18:13,2018-04-20 00:40:19,72e1d5da30c6,715c7d15b226,8599000,27063000,0,8596321,27061196,1799108,10302,5560,0,finished
ConcurrentGC,AFP,2018-04-19 00:18:17,2018-04-19 00:40:51,0a2a1b6507c1,e97d5b6aa872,8277000,26169000,0,8274600,26166888,1680696,8782,5599,0,finished
ConcurrentGC,AFP,2018-04-18 00:18:13,2018-04-18 00:39:37,ae76012879c6,7c3ea015c632,8157000,25645000,0,8154626,25643008,1639424,10336,5667,0,finished
ConcurrentGC,AFP,2018-04-17 00:18:19,2018-04-17 00:40:12,c0ebecf6e3eb,7a9e13c52757,802,25273000,0,8017863,25271084,1585068,10194,5721,0,finished
ConcurrentGC,AFP,2018-04-16 00:18:15,2018-04-16 00:39:47,b65c4a6a015e,54e15e31c3ea,8233000,25828000,0,8230843,25826424,1705004,10176,5589,0,finished
ConcurrentGC,AFP,2018-04-15 00:18:06,2018-04-15 00:39:23,349c639e593c,d2f502a794b7,7988000,25242000,0,7985231,25239672,1713680,10287,7309,0,finished
ConcurrentGC,AFP,2018-04-14 00:18:09,2018-04-14 

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

[Lars Hupel]

> Last known good state is:
> 
> Isabelle/7e349d1e3c95
> AFP/c3cfeceda7a0

We're back to normal now, as of

Isabelle/58c9231c2937
AFP/79f64c92d5ae
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

[Lars Hupel]

(I meant "non-termination", of course, not "non-determinism".)

> Even if it'll terminate eventually (I'll keep it running for a bit
> longer), it surely is a sign of a performance degradation.

This run (threads=8) confirms that HOL-ODE-Numerics doesn't terminate
within 2 elapsed hours:

https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/754/consoleFull
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev