[isabelle-dev] Isabelle takes more time to be built on testboard
makarius at sketis.net
Thu May 16 17:38:51 CEST 2013
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
> 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:
at-poly is just one of many tests. There is no change in most others,
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.
More information about the isabelle-dev