I think you might have accidentally pushed to afp-2015 instead of afp-devel.
This is on afp-2015:
changeset: 5536:b0b40e683dbc
user:paulson
date:Thu Aug 20 17:31:45 2015 +0100
summary: fixed problems mostly connected with changes to tendsto_zero_powrI
I’ll have a looks at
The error is as follows:
> *** Undefined fact: "setsum_bounded" (line 286 of
> "/mnt/nfsbroy/home/isatest/afp/devel/thys/Girth_Chromatic/Ugraphs.thy")
> *** At command "using" (line 286 of
> "/mnt/nfsbroy/home/isatest/afp/devel/thys/Girth_Chromatic/Ugraphs.thy”)
Yes, I renamed this theorem to s
The problem seems to be HyperCTL. From the log:
Run out of store - interrupting threads
Failed to recover - exiting
/tmp/isabelle-isatest/isabelle_script3270098471353362986: line 8:
/mnt/nfsbroy/home/isatest/afp/isadist/Isabelle_04-May-2014/lib/scripts/timestop.bash:
No such file or directory
Hy
Am 05.05.2014 um 11:17 schrieb Johannes Hölzl :
> Has anybody an idea why the AFP test for Probabilistic_Noninterference
> fails?
>
> When I build it on my machine
Same on my machine, and same for Selection_Heap_Sort, Native_Word, and
Launchbury: All work fine on my machine.
(HyperCTL has been
I use "isabelle afp_build Probabilistic_Noninterference" to build it,
which includes the document generation. So it is possible that the
document generation on the macbroy2 is different from my setup.
Looking into the reports attached to the status email, I also see that
the log for Probabilistic_
Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?
When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a recent hg version
(AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems.
-
Could it be the document preparation?
Dmitriy
Am 05.05.2014 11:17, schrieb Johannes Hölzl:
Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?
When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a
> Florian also has an older attempt at some "testafp" tool in the AFP
> repository, which should be obsolete now.
This is obsolete now. Anyone still having stocks there?
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muen
On Thu, 4 Oct 2012, Gerwin Klein wrote:
This is now done, AFP_big has been retired, and afp_build updated
accordingly.
Great. I have removed one more letter in AFP/c9d12d55c3a6.
BTW, my afp_build was more like an example. Feel free to reshape the
standard build process in the way you see f
This is now done, AFP_big has been retired, and afp_build updated accordingly.
I've removed all occurrences of FLYSPEC_SKIP_PROOFS in isatest and afptest, but
I'm not sure if it is used in Mira anywhere. It should be fail safe, but should
be cleaned up.
Cheers,
Gerwin
On 29/09/2012, at 11:57
On 21/09/2012, at 9:31 PM, Makarius wrote:
> On Fri, 21 Sep 2012, Tobias Nipkow wrote:
>
>> This is just another reminder that people should watch the AFP when they
>> check in changes, and fix them. The testboard runs most of the AFP.
>
> Once the testboard recovers, one could make this a bit
On Wed, 27 Jun 2012, Gerwin Klein wrote:
On 27/06/2012, at 12:06 AM, Makarius wrote:
On Mon, 25 Jun 2012, Makarius wrote:
We have a new record in unavailability.
Where is the isatest crontab now? macbroy28 is still unavailable as we knew
already several weeks ago.
In any case Admin/isate
On 27/06/2012, at 12:06 AM, Makarius wrote:
> On Mon, 25 Jun 2012, Makarius wrote:
>
>> We have a new record in unavailability.
>>
>> Where is the isatest crontab now? macbroy28 is still unavailable as we knew
>> already several weeks ago.
>>
>> In any case Admin/isatest should reflect the c
On Mon, 25 Jun 2012, Makarius wrote:
We have a new record in unavailability.
Where is the isatest crontab now? macbroy28 is still unavailable as we
knew already several weeks ago.
In any case Admin/isatest should reflect the current state, both for the
Isabelle and AFP crontab.
In the me
On Wed, 20 Jun 2012, Gerwin Klein wrote:
According to the log, the test didn't run Jun 16-18 which are the days
with NFS trouble.
You probably mean ~isatest/afp/afp-test.log, because
~isatest/log/isatest.log and http://isabelle.in.tum.de/devel agree that
the last successful Isabelle isatest
Should be resolved now.
The problem was that ~/isatest/hg-isabelle couldn't pull and update, because
someone else than isatest owned some of the internal .hg files and isatest got
permission errors which it silently ignored.
I've set up a fresh clone under hg-isabelle. If there were any fancy s
According to the log, the test didn't run Jun 16-18 which are the days with NFS
trouble.
The test ran successfully on Jun 19 with afp 3acca130d67d and isabelle
72acba14c12b.
There is something fishy with the isabelle version, though: it's been showing
72acba14c12b since Jun 2. Will investigate
isatest home was not mounted on macbroy2 where the test runs. That explains the
last few days. It should have run yesterday.
Cheers,
Gerwin
On 19/06/2012, at 10:50 PM, Lukas Bulwahn wrote:
> Hi all,
>
> since 06/05/2012, I have not received any status (AFP) emails, although it
> should have b
Hi all,
since 06/05/2012, I have not received any status (AFP) emails, although
it should have been failing the last days.
(After Isabelle:e7e647949c95, the theory LinearQuantifierElim was
failing, and I just fixed with AFP:96f043cb412e.)
Is the AFP test script still working properly?
Maybe l
19 matches
Mail list logo
