[isabelle-dev] Isabelle takes more time to be built on testboard

[Makarius]

On Mon, 13 May 2013, Johannes Hölzl wrote:

> My changes Ondřej mentions are between
>  Old: http://isabelle.in.tum.de/repos/isabelle/rev/7957d26c3334
> and
>  New: http://isabelle.in.tum.de/repos/isabelle/rev/f415febf4234
>
> Where I were mostly moving stuff around in HOL. This should be only visible
> in Complex_Main and not in Main. But the HOL-Proof and especially the
> ZF images also take more time.

I don't see anything suspicious in that range -- apart from theory names 
in plural, which potentially violate the usual naming conventions, unless 
there are reasons for that (i.e. multiple related concepts defined.)

When you define a theory of real vector spaces, it would be called 
Real_Vector_Space by default.  A counter-example is theory 
Numeral_Simprocs, which defines various numeral simprocs.


> Am Montag, den 13.05.2013, 15:01 +0200 schrieb Ondřej Kunčar:
>> 
>> I talked to Johannes and this slowdown doesn't seem to be related to his 
>> changes from 26.3.
>> One can also see here that almost all sessions started to take more time 
>> to be built around that time:
>> http://isabelle.in.tum.de/devel/stats/at-poly.html

at-poly is just one of many tests.  There is no change in most others, 
e.g. http://isabelle.in.tum.de/devel/stats/mac-poly-M2.html

So it could be just a fluctuation of local machine configuration (one of 
the many OS updates that the admins did recently or some changes of shared 
libraries), or changes of the concreye Poly/ML compilation being used.

Since the isatest settings are visible in Admin/isatest/settings within 
the repository, and there is no recent change to be seen, I would guess at 
some effect from OS or file-system / file-servers at TUM.


 	Makarius