Re: [isabelle-dev] status (AFP)
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 moving the changeset over. Cheers, Gerwin > On 22.08.2015, at 21:46, Larry Paulson wrote: > > 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 setsum_bounded_above, but I fixed it in > afp/devel in the afternoon of 20 August. And committed and pushed my changes. > Why this error still occurs, I have no idea. > > Larry > >> On 21 Aug 2015, at 12:31, Isabelle >> wrote: >> >> > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 setsum_bounded_above, but I fixed it in afp/devel in the afternoon of 20 August. And committed and pushed my changes. Why this error still occurs, I have no idea. Larry > On 21 Aug 2015, at 12:31, Isabelle > wrote: > > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 HyperCTL FAILED [..] Running Launchbury ... *** I/O error: Cannot run program "/mnt/nfsbroy/home/isatest/afp/isadist/Isabelle_04-May-2014/lib/scripts/process" (in directory "/home/isatest/afp/devel/thys/Launchbury"): error=2, No such file or directory It looks like the test for HyperCTL is running so long before it fails that half the execution environment has disappeared (possibly because it is being deleted for the test on the next day). I have added a time out to the session now so the other ones at least get a chance to run. We should introduce a more systematic check that all AFP sessions have a time out set. Cheers, Gerwin On 05.05.2014, at 7:49 pm, Jasmin Christian Blanchette wrote: > 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 broken since it has been introduced. We need Andrei to > look at it.) > > Jasmin > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 broken since it has been introduced. We need Andrei to look at it.) Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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_Noninterference is missing! - Johannes Am Montag, den 05.05.2014, 11:18 +0200 schrieb Dmitriy Traytel: > 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 recent hg version > > (AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems. > > > > - Johannes > > > > Am Montag, den 05.05.2014, 07:50 +0200 schrieb Isabelle : > >> The status of the following AFP entries changed or remains FAIL: > >> [Selection_Heap_Sort] is still on FAIL. > >> [Native_Word] is still on FAIL. > >> [HyperCTL] is still on FAIL. > >> [Launchbury] is still on FAIL. > >> [Probabilistic_Noninterference] is still on FAIL. > >> > >> Full entry status at http://afp.sourceforge.net/status.shtml > >> > >> AFP version: development -- hg id acd2cc051b4f > >> Isabelle version: devel -- hg id 52e5bf245b2a > >> Test ended on: macbroy2, Mon May 5 07:50:12 CEST 2014. > >> > >> Have a nice day, > >>isatest > >> > > > > ___ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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. - Johannes Am Montag, den 05.05.2014, 07:50 +0200 schrieb Isabelle : > The status of the following AFP entries changed or remains FAIL: > [Selection_Heap_Sort] is still on FAIL. > [Native_Word] is still on FAIL. > [HyperCTL] is still on FAIL. > [Launchbury] is still on FAIL. > [Probabilistic_Noninterference] is still on FAIL. > > Full entry status at http://afp.sourceforge.net/status.shtml > > AFP version: development -- hg id acd2cc051b4f > Isabelle version: devel -- hg id 52e5bf245b2a > Test ended on: macbroy2, Mon May 5 07:50:12 CEST 2014. > > Have a nice day, > isatest > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 recent hg version (AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems. - Johannes Am Montag, den 05.05.2014, 07:50 +0200 schrieb Isabelle : The status of the following AFP entries changed or remains FAIL: [Selection_Heap_Sort] is still on FAIL. [Native_Word] is still on FAIL. [HyperCTL] is still on FAIL. [Launchbury] is still on FAIL. [Probabilistic_Noninterference] is still on FAIL. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id acd2cc051b4f Isabelle version: devel -- hg id 52e5bf245b2a Test ended on: macbroy2, Mon May 5 07:50:12 CEST 2014. Have a nice day, isatest ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
> 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_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 fit as AFP administrator. There is not much functionality left in the script anyway: it just strings together $AFP_BUILD_OPTIONS with "-d '$AFP' -g AFP" and passes on to regular isabelle build. Florian also has an older attempt at some "testafp" tool in the AFP repository, which should be obsolete now. 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. Independently of the AFP configuration, Mira is still in bad shape (for 1-2 weeks already). E.g. see http://isabelle.in.tum.de/reports/Isabelle/report/3b4b73890515487a97a26dc8f4c56370 The "### Missing Isabelle component: ..." warnings indicate that the local copy of the standard components are outdated. I still wonder why /home/isabelle/contrib cannot be used directly in the Mira setup. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 AM, Gerwin Klein wrote: > 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 more complete. I >> usually have FLYSPECK_SKIP_PROOFS=true in my settings and then run *all* of >> AFP in 35min on a plain-old 8-core workstation. >> >> The new Isabelle build configuration has the "condition" option to formalize >> the omission of theories, depending on given environment variables. >> ISABELLE_FULL_TEST (undefined by default) is already used as a convention to >> guard extra tests that take unusually long time. >> >> If ISABELLE_FULL_TEST would be checked instead of FLYSPECK_SKIP_PROOFS in >> afp/thys/Flyspeck-Tame/ArchComp.thy with the inverted meaning, then one >> could discontinue the AFP vs. AFP_big distinction. It would work for >> everyone by default within the range of 0.5 .. 2h total. >> >> The full test would then be run infrequently by one of the standard test >> frameworks in the background. > > I managed to miss this email until Tobias pointed me to it. > > I think this is a good idea and will have a look at rejigging the AFP build > accordingly in the next few days. > > Cheers, > Gerwin > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 more complete. I > usually have FLYSPECK_SKIP_PROOFS=true in my settings and then run *all* of > AFP in 35min on a plain-old 8-core workstation. > > The new Isabelle build configuration has the "condition" option to formalize > the omission of theories, depending on given environment variables. > ISABELLE_FULL_TEST (undefined by default) is already used as a convention to > guard extra tests that take unusually long time. > > If ISABELLE_FULL_TEST would be checked instead of FLYSPECK_SKIP_PROOFS in > afp/thys/Flyspeck-Tame/ArchComp.thy with the inverted meaning, then one could > discontinue the AFP vs. AFP_big distinction. It would work for everyone by > default within the range of 0.5 .. 2h total. > > The full test would then be run infrequently by one of the standard test > frameworks in the background. I managed to miss this email until Tobias pointed me to it. I think this is a good idea and will have a look at rejigging the AFP build accordingly in the next few days. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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/isatest should reflect the current state, both for the Isabelle and AFP crontab. In the meantime I have started some attempts to reactivate isatest, see Isabelle/a29f3f44e198. Sorry my fault, this totally went under. Thanks for reactivating it. At the moment it is sufficiently active to produce again some NFS dropouts. I have moved further jobs away from macbroy2[0-9] to lxbroy[234], which seem to be relatively new server class machines. See also Isabelle/68a32e12b999 and before. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 current state, both for the >> Isabelle and AFP crontab. > > In the meantime I have started some attempts to reactivate isatest, see > Isabelle/a29f3f44e198. Sorry my fault, this totally went under. Thanks for reactivating it. macbroy27 seems to be fine for now. The MTA's were suggesting we use a server machine. Does anyone know a suitable one? Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 meantime I have started some attempts to reactivate isatest, see Isabelle/a29f3f44e198. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 was at the end of May. 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 symlinks or other changes in the old one, things might break (hg st came back clean, though). Cheers, Gerwin On 20/06/2012, at 11:12 AM, Gerwin Klein wrote: > 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. > > Cheers, > Gerwin > > On 20/06/2012, at 10:30 AM, Gerwin Klein wrote: > >> 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 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 latest changes to the contrib directories broke the test script? >>> >>> Lukas >>> >>> On 06/05/2012 09:51 AM, Isabelle wrote: The status of the following AFP entries changed or remains FAIL: [JinjaThreads] changed from FAIL to ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id 4c44fdeca962 Isabelle version: devel -- hg id 72acba14c12b Test ended on: macbroy2, Tue Jun 5 09:51:34 CEST 2012. Have a nice day, isatest >>> >>> ___ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> >> >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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. Cheers, Gerwin On 20/06/2012, at 10:30 AM, Gerwin Klein wrote: > 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 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 latest changes to the contrib directories broke the test script? >> >> Lukas >> >> On 06/05/2012 09:51 AM, Isabelle wrote: >>> The status of the following AFP entries changed or remains FAIL: >>> [JinjaThreads] changed from FAIL to ok. >>> >>> Full entry status at http://afp.sourceforge.net/status.shtml >>> >>> AFP version: development -- hg id 4c44fdeca962 >>> Isabelle version: devel -- hg id 72acba14c12b >>> Test ended on: macbroy2, Tue Jun 5 09:51:34 CEST 2012. >>> >>> Have a nice day, >>> isatest >>> >> >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 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 latest changes to the contrib directories broke the test script? > > Lukas > > On 06/05/2012 09:51 AM, Isabelle wrote: >> The status of the following AFP entries changed or remains FAIL: >> [JinjaThreads] changed from FAIL to ok. >> >> Full entry status at http://afp.sourceforge.net/status.shtml >> >> AFP version: development -- hg id 4c44fdeca962 >> Isabelle version: devel -- hg id 72acba14c12b >> Test ended on: macbroy2, Tue Jun 5 09:51:34 CEST 2012. >> >> Have a nice day, >> isatest >> > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
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 latest changes to the contrib directories broke the test script? Lukas On 06/05/2012 09:51 AM, Isabelle wrote: The status of the following AFP entries changed or remains FAIL: [JinjaThreads] changed from FAIL to ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id 4c44fdeca962 Isabelle version: devel -- hg id 72acba14c12b Test ended on: macbroy2, Tue Jun 5 09:51:34 CEST 2012. Have a nice day, isatest ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
