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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
