On Tue, 20 Oct 2015, Gerwin Klein wrote:
Under the account isatest in ~/afp/log and ~/log.
This cumulative information over more than a decade actually quite
interesting.
It is the lasting result of continous burning of CPU cycles for Isabelle
tests.
Makarius
__
Under the account isatest in ~/afp/log and ~/log.
Cheers,
Gerwin
> On 20.10.2015, at 19:09, Lars Hupel wrote:
>
> Dear developers,
>
> does anyone know where the isatest and afptest logs are stored? I'd like
> to do some performance analysis over the last, say, one month. (If you
> have them in
Dear developers,
does anyone know where the isatest and afptest logs are stored? I'd like
to do some performance analysis over the last, say, one month. (If you
have them in your mail inbox, you can also forward them to me.)
Cheers
Lars
___
isabelle-dev
On Thu, 28 Nov 2013, Makarius wrote:
Important note: isatest is presently testing
https://bitbucket.org/isabelle_project/isabelle-release again.
isatest is back testing http://isabelle.in.tum.de/repos/isabelle
isabelle-release is back at the merge point 748778ac0ab8
So we are mostly back to
Important note: isatest is presently testing
https://bitbucket.org/isabelle_project/isabelle-release again.
There have been a bit too many posthoc changes for Isabelle2013-1 to trust
blindly that the usual collection of isatest platforms still work. The
final Isabelle2013-2 release will probab
On Fri, 14 Dec 2012, Gerwin Klein wrote:
The development snapshot is only a byproduct and can be left out. The
main reason for generating a .tar.gz was to test if the release building
machinery works and to test something that is as close as possible to a
release that users work with, not the
On 15/12/2012, at 12:54 AM, Makarius wrote:
> The unusual isatest silence from today means that all tests finished
> successfully!
No news are good news :-)
> http://isabelle.in.tum.de/devel/ shows some development snapshot
> Isabelle_14-Dec-2012.tar.gz together with the vital statistics.
>
The unusual isatest silence from today means that all tests finished
successfully!
http://isabelle.in.tum.de/devel/ shows some development snapshot
Isabelle_14-Dec-2012.tar.gz together with the vital statistics.
Since "the" development snapshot has lost its purpose with the
introduction of t
On 27/11/2012, at 12:55 AM, Makarius wrote:
> On Mon, 26 Nov 2012, Gerwin Klein wrote:
>
>>> The reasoning (or rather hope) behind the above was that for doing real
>>> non-sense you would have to be on the local network at TUM. So it is
>>> basically a switch back towards the old-fashioned w
On Mon, 26 Nov 2012, Gerwin Klein wrote:
The reasoning (or rather hope) behind the above was that for doing real
non-sense you would have to be on the local network at TUM. So it is
basically a switch back towards the old-fashioned ways of rsh.
I'm fine with that part. I mainly don't want to
On 26/11/2012, at 9:01 PM, Makarius wrote:
> On Sun, 25 Nov 2012, Gerwin Klein wrote:
>
>> On 20/11/2012, at 11:23 PM, Makarius wrote:
>>
>>> There is this recurrent game to have the isatest user do many manual ssh
>>> logins to update known_hosts. Getting tired of it, I just did some reading
On Sun, 25 Nov 2012, Gerwin Klein wrote:
On 20/11/2012, at 11:23 PM, Makarius wrote:
There is this recurrent game to have the isatest user do many manual ssh logins
to update known_hosts. Getting tired of it, I just did some reading of man
ssh_config and some googling. This resulted the f
On Sun, 2012-11-25 at 00:00 +, Gerwin Klein wrote:
> On 20/11/2012, at 11:23 PM, Makarius wrote:
> > StrictHostKeyChecking no
> > UserKnownHostsFile=/dev/null
> >
> > Maybe it helps in other situations, too. Or maybe there is an ssh expert
> > saying that this is really really bad.
>
> ss
On 20/11/2012, at 11:23 PM, Makarius wrote:
> There is this recurrent game to have the isatest user do many manual ssh
> logins to update known_hosts. Getting tired of it, I just did some reading
> of man ssh_config and some googling. This resulted the following
> ~isatest/.ssh/config:
>
> H
There is this recurrent game to have the isatest user do many manual ssh
logins to update known_hosts. Getting tired of it, I just did some
reading of man ssh_config and some googling. This resulted the following
~isatest/.ssh/config:
Host *
#see
http://linuxcommando.blogspot.fr/2008/10/h
On Wed, 24 Oct 2012, Jasmin Christian Blanchette wrote:
So the last threee lines of the attachment are shown. Would it be possible to
increase that to four? That way, we'd get the much more instructive
Test for platform mac-poly64-M2 failed. Log file attached.
[...]
Unfinished session
Hi all,
This is probably a question to Makarius. Today the Isatest reports look like
this:
Test for platform mac-poly64-M2 failed. Log file attached.
[...]
Finished at Wed Oct 24 02:40:50 CEST 2012
2:12:57 elapsed time, 3:44:19 cpu time, factor 1.68
--- test F
We've seen routine isatest dropouts in the past few weeks. With
Isabelle/d1ecb3554b25 there is some hope that it will work better again.
There have been some actual issues with exceptions, interrupts and
parallel evaluation on the Isabelle side.
I still have the ambitition to return to routin
In an attempt to get rid of spurious "Host key verification failed" messages,
I've cleaned out the old ~/.ssh/known_hosts file of isatest and manually
re-added all hosts mentioned in Admin/isatest.
If there are other things running under this account (mira?) that may break
when ssh asks for hos
Dear all,
after more than 1 month, isatest is not quite dead yet, but getting
better. The main control is now on lxbroy2, which is a bit different due
to Gentoo Linux used there.
Hopefully we now get some meaningful results again, including the
important continous timings.
Makari
On 04/22/2012 03:04 PM, Florian Haftmann wrote:
I've managed to remove more than 5 GB of old heap files, but this might
be a bit pathethic due to this directory:
225G tmp/shared_results
Does anybody know what it is?
These are the results from the mira runs, which in theory are kept
eternall
> I've managed to remove more than 5 GB of old heap files, but this might
> be a bit pathethic due to this directory:
>
> 225G tmp/shared_results
>
> Does anybody know what it is?
These are the results from the mira runs, which in theory are kept
eternally. There is the mira command »purge« w
The home directory of isatest has reached its disk quote, which means that
recent tests were referring to an old clone of the repository, since the
hg update did not work.
I've managed to remove more than 5 GB of old heap files, but this might be
a bit pathethic due to this directory:
225G
On Thu, 29 Mar 2012, Gerwin Klein wrote:
On 29/03/2012, at 6:11 AM, Makarius wrote:
Who is the main responsible for isatest anyway? According to the
received customs it would be Gerwin, since he started the service many
years ago. (His shell scripts still mention SunOS.)
I still feel mildl
On Fri, 30 Mar 2012, Lukas Bulwahn wrote:
On 03/30/2012 11:24 AM, Makarius wrote:
On Fri, 30 Mar 2012, Lukas Bulwahn wrote:
The webpage on the Isabelle (community) wiki,
https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities,
summarizes the agreement of this thread. If
On Fri, 30 Mar 2012, Lukas Bulwahn wrote:
The webpage on the Isabelle (community) wiki,
https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities,
summarizes the agreement of this thread. If anyone wants to add or
modify the page, feel free to do so.
I am still not subscr
The webpage on the Isabelle (community) wiki,
https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities,
summarizes the agreement of this thread.
If anyone wants to add or modify the page, feel free to do so.
Lukas
On 03/29/2012 09:29 AM, Gerwin Klein wrote:
On 29/03/2012,
On 29/03/2012, at 4:31 PM, Tobias Nipkow wrote:
> Am 28/03/2012 23:30, schrieb Gerwin Klein:
>> On 29/03/2012, at 6:11 AM, Makarius wrote:
>>
>>> On Wed, 28 Mar 2012, Florian Haftmann wrote:
>>>
Once there has been the idea that everyone having commit access to the
Isabelle master rep
Am 28/03/2012 23:30, schrieb Gerwin Klein:
> On 29/03/2012, at 6:11 AM, Makarius wrote:
>
>> On Wed, 28 Mar 2012, Florian Haftmann wrote:
>>
>>> Once there has been the idea that everyone having commit access to the
>>> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a
>>> i
On 29/03/2012, at 6:11 AM, Makarius wrote:
> On Wed, 28 Mar 2012, Florian Haftmann wrote:
>
>> Once there has been the idea that everyone having commit access to the
>> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a
>> isatest subscriber.
>>
>> Maybe it would be helpful
On Wed, 28 Mar 2012, Florian Haftmann wrote:
Once there has been the idea that everyone having commit access to the
Isabelle master repository (POSIX group isabelle at nfsbroy) is also a
isatest subscriber.
Maybe it would be helpful to establish this as a rule (at least of
thumb). Isatest m
Sounds like a sensible idea to avoid test failures to go unnoticed.
Tobias
Am 28/03/2012 20:45, schrieb Florian Haftmann:
> Hi all,
>
> Once there has been the idea that everyone having commit access to the
> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a
> isatest subscr
Hi all,
Once there has been the idea that everyone having commit access to the
Isabelle master repository (POSIX group isabelle at nfsbroy) is also a
isatest subscriber.
Maybe it would be helpful to establish this as a rule (at least of
thumb). Isatest mails can still be sorted out by local emai
33 matches
Mail list logo
