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

[Makarius]

On 12/05/18 00:27, Makarius wrote:
> 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 further results from looking through AFP build_status (the
relevant interval is b91c4acc1aaf:b25ccd85b1fd):

  * faster: Gauss_Jordan, Vickrey_Clarke_Groves, Card_Partitions,
ArrowImpossibilityGS, Category

  * slower: Stone_Relation_Algebras

It means that the "Generalizations in the formalization of linear
algebra" make things much faster in many situations.

The slowdown of the small session Stone_Relation_Algebras might help to
figure out what is actually going on.


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

Re: [isabelle-dev] Slowdown of ConcurrentGC

[Makarius]

On 12/05/18 00:01, Makarius wrote:
> 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.

I have studied this a bit further. The interval
75130777ece4:d45b78cb86cf contains more than just the string type
change, but it is still the main thing. Here are also other sessions in
similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498:

  * faster: HOL-IMP, HOL-Quickcheck_Examples,
Network_Security_Policy_Verification, Pre_Perron_Frobenius,
JiveDataStoreModel, Partial_Function_MR

  * slower: Tarskis_Geometry, XML, Cauchy

In particular, I am glad that Network_Security_Policy_Verification is
now back to its fairly good timing from some months ago (see attachments
and this thread:
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07717.html).

Many other sessions have become much faster, without becoming slow
before. Very good.

>From the (few) ones that become slower, small sessions like XML or
Cauchy might help to see clearly what are the reasons for it.


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
Network_Security_Policy_Verification,AFP,2018-05-12 00:18:16,2018-05-12 00:40:11,42d63ea39161,92ec39882136,114,1137000,0,1137526,1135707,68343,0,0,0,finished
Network_Security_Policy_Verification,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
Network_Security_Policy_Verification,AFP,2018-05-08 00:18:06,2018-05-08 00:40:17,2277fe496d78,4a788844049b,1136000,1134000,0,1134349,1132316,66615,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-05-07 00:18:09,2018-05-07 00:39:33,0b66aca9c965,ba558fdf522c,1143000,114,0,1140346,1138024,68710,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-05-05 00:18:07,2018-05-05 00:39:54,b25ccd85b1fd,ad1d95d5ace6,1147000,1144000,0,1145196,1142685,66892,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-05-05 00:18:07,2018-05-05 00:18:07,b25ccd85b1fd,ba558fdf522c,1139000,1135000,0,1136775,1134010,65072,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-05-03 00:40:00,2018-05-03 00:40:00,b91c4acc1aaf,8c085909633b,1135000,1132000,0,1132392,1130552,66562,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-05-02 00:18:06,2018-05-02 00:18:06,3931ed905e93,8c085909633b,1147000,1144000,0,1145221,1142700,68684,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-05-01 00:39:45,2018-05-01 00:39:45,7811d8828775,83c48344a96f,1141000,1138000,0,1138705,1136855,64598,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-30 00:18:26,2018-04-30 00:40:00,9e077a905209,d2059b336ac3,1147000,1144000,0,1145257,1142771,71377,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-29 00:18:24,2018-04-29 00:40:00,ebd179b82e20,5d888a880328,1153000,115,0,1150513,1148483,66650,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-28 00:18:28,2018-04-28 00:39:53,e98988801fa9,f0759507c46c,1136000,1133000,0,1134476,1131261,63513,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-27 00:18:31,2018-04-27 00:40:52,f76e8180c498,6dacb8b19575,1153000,1151000,0,1150874,1149165,73225,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-24 00:18:31,2018-04-24 00:18:31,75130777ece4,efd58f8b1659,2863000,2861000,0,2861387,2859236,69096,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-23 00:18:24,2018-04-23 00:18:24,c8a506be83bd,efd58f8b1659,2877000,2874000,0,2875073,2872755,66381,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-22 00:18:27,2018-04-22 00:40:19,b91a043c0dcb,b6b5f48aa576,2944000,2941000,0,2941441,2939396,67053,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-21 00:18:17,2018-04-21 00:40:10,32d19862781b,4bf3efef63d6,2938000,2935000,0,2935833,2933481,63102,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-20 00:18:13,2018-04-20 00:40:19,72e1d5da30c6,715c7d15b226,2884000,2881000,0,2881937,2879495,64859,0,0,0,finished
Network_Security_Policy_Verification,AFP,2018-04-19 00:18:17,2018-04-19 

Re: [isabelle-dev] NEWS: Isabelle server

[Christian Sternagel]

Just for the record: Makarius' reply resolved the issue for me (see also
below).

On 05/09/2018 11:57 PM, Makarius wrote:
> On 26/03/18 13:48, Christian Sternagel wrote:
>>
>> Thanks, I forgot about that option.
>>
>> With "isabelle latex" in the specified directory the error boils down to:
>>
>> ./root.tex:31: Package pdftex.def Error: File
>> `isabelle-eps-converted-to.pdf' n
>> ot found.
>>
>> See the pdftex.def package documentation for explanation.
>> Type  H   for immediate help.
>>  ...
>>
>> Should isabelle-eps-converted-to.pdf exist on my system?
> 
> I guess that the "epstopdf" tool is missing: there should be some Fedora
> package for it.

That is correct. Thanks for pointing it out, it was not clear to me from
the error message.

> 
> Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into
> user output -- this is required for hard errors of missing executables
> and style files.
> 
> With that I have managed to do "isabelle build -o document=pdf -g doc"
> or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome
> saturation of the texlive installation, where almost every style file
> has its own package.

This kind of saturation is indeed cumbersome, but at least its possible
as long as you know which packages are missing ;)

cheers

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

Re: [isabelle-dev] HOL-Algebra

[Lawrence Paulson]

I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are 
ancient. They desperately need updating and streamlining.

We’ve decided that Group-Ring-Module is irremediable, and are using it only as 
a list of useful results that need to be done again.

Larry

> On 11 May 2018, at 23:40, Makarius  wrote:
> 
> 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).
> 

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