Re: [isabelle-dev] testboard
On 19.08.2015 22:45, Makarius wrote: On Wed, 19 Aug 2015, Larry Paulson wrote: I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical (I’m using SourceTree), so have I simultaneously pushed my changes to the main repository somehow? Maybe. The changeset 6a6f15d8fbc4 turned out broken -- I've repaired this already in e1159bd15982. Generally, we are running short of proper test machines -- isatest takes very long now. The fastest machine in reach is the one under my desk. Makarius I haven't seen the state of the testboard when Larry pushed, but I suspect that he pushed to the main repository exclusively (rather than simultaneously to the testboard). Note that the testboard requires a "push -f", otherwise Mercurial will refuse to create a new head. When I just pushed to the testboard a few minutes ago Mercurial replied with added 67 changesets with 204 changes to 134 files (+1 heads) (This is a quite normal response, even though I've added only one change, since the testboard is not automatically updated w.r.t. the main repository, and I am one of the few people who sometimes pushes to the testboard. In effect, I've pushed 67 changes (including Larry's changeset 6a6f15d8fbc4) that were pushed to the main repository but not to testboard.) Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] testboard
On Wed, 19 Aug 2015, Larry Paulson wrote: I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical (I’m using SourceTree), so have I simultaneously pushed my changes to the main repository somehow? Maybe. The changeset 6a6f15d8fbc4 turned out broken -- I've repaired this already in e1159bd15982. Generally, we are running short of proper test machines -- isatest takes very long now. The fastest machine in reach is the one under my desk. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] testboard
I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical (I’m using SourceTree), so have I simultaneously pushed my changes to the main repository somehow? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
On Mon, 7 Jul 2014, Lars Noschinski wrote: @Makarius: Does this use fit the intention of USER_HOME? Is this question still open? I have lost track of the various Mira configuration problems. I have implemented this approach (i.e., Mira sets $USER_HOME to some arbitrary place before starting Isabelle) and this seems to work. The only open question is whether you see any problems in $HOME /= $USER_HOME. It should work. The whole point of USER_HOME is to allow this to be different from HOME, which has slightly different meaning on Windows + Cygwin. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
On 04.07.2014 12:43, Makarius wrote: > On Wed, 4 Jun 2014, Lars Noschinski wrote: > >> On 04.06.2014 13:37, Johannes Hölzl wrote: >>> We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and >>> now it >>> works... >>> >>> I don't know why mira is accessing this file, it actually sets up the >>> settings file to _not_ look into the users heaps-directory. But it >>> looks >>> like there is a problem with this setup. >> After looking a bit closer: Mira changes ISABELLE_HOME_USER (by >> appending it to $ISABELLE_HOME/etc/settings). Of course, this is too >> late to affect ISABELLE_PATH, which still refers to >> $USER_HOME/.isabelle/heaps. >> >> So, we set $USER_HOME instead before starting Isabelle (see >> bcc6dc6c1d1c8a6). >> >> @Makarius: Does this use fit the intention of USER_HOME? > > Is this question still open? I have lost track of the various Mira > configuration problems. I have implemented this approach (i.e., Mira sets $USER_HOME to some arbitrary place before starting Isabelle) and this seems to work. The only open question is whether you see any problems in $HOME /= $USER_HOME. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
On Wed, 4 Jun 2014, Lars Noschinski wrote: On 04.06.2014 13:37, Johannes Hölzl wrote: We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it works... I don't know why mira is accessing this file, it actually sets up the settings file to _not_ look into the users heaps-directory. But it looks like there is a problem with this setup. After looking a bit closer: Mira changes ISABELLE_HOME_USER (by appending it to $ISABELLE_HOME/etc/settings). Of course, this is too late to affect ISABELLE_PATH, which still refers to $USER_HOME/.isabelle/heaps. So, we set $USER_HOME instead before starting Isabelle (see bcc6dc6c1d1c8a6). @Makarius: Does this use fit the intention of USER_HOME? Is this question still open? I have lost track of the various Mira configuration problems. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
On 04.06.2014 13:37, Johannes Hölzl wrote: > We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it > works... > > I don't know why mira is accessing this file, it actually sets up the > settings file to _not_ look into the users heaps-directory. But it looks > like there is a problem with this setup. After looking a bit closer: Mira changes ISABELLE_HOME_USER (by appending it to $ISABELLE_HOME/etc/settings). Of course, this is too late to affect ISABELLE_PATH, which still refers to $USER_HOME/.isabelle/heaps. So, we set $USER_HOME instead before starting Isabelle (see bcc6dc6c1d1c8a6). @Makarius: Does this use fit the intention of USER_HOME? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it works... I don't know why mira is accessing this file, it actually sets up the settings file to _not_ look into the users heaps-directory. But it looks like there is a problem with this setup. - Johannes Am Mittwoch, den 04.06.2014, 10:18 +0200 schrieb Johannes Hölzl: > Hi, > > a change of mine leads to a failure of the testboard, > HOL-Proofs-Extraction can not be build anymore. > > For example see: > > http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28 > > But when I run on this very changeset the commands > > isabelle build -b HOL-Proofs-Extraction > > or > > isabelle build -a > > on my machine, everything runs fine. > > Is there a special setup for the testboard when it runs Isabelle > makeall? > > - Johannes > > ___ > 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] Testboard problem
Hi, a change of mine leads to a failure of the testboard, HOL-Proofs-Extraction can not be build anymore. For example see: http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28 But when I run on this very changeset the commands isabelle build -b HOL-Proofs-Extraction or isabelle build -a on my machine, everything runs fine. Is there a special setup for the testboard when it runs Isabelle makeall? - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
On 02.10.2013 01:09, Alexander Krauss wrote: On 09/27/2013 11:49 AM, Lars Noschinski wrote: It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). Such a strategy is easy to implement for a single repository. But for multiple repositories (Isabelle+AFP) there is no useful notion of heads (The obvious lifting to products does work theoretically, but not practically, since there are just too many of them...) Hm, you are right. Another option would be to record the tip-tuples in a push-hook and work on these, if there is no tip to be processed. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
On 09/27/2013 11:49 AM, Lars Noschinski wrote: It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). Such a strategy is easy to implement for a single repository. But for multiple repositories (Isabelle+AFP) there is no useful notion of heads (The obvious lifting to products does work theoretically, but not practically, since there are just too many of them...) Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
Am 27.09.2013 um 12:29 schrieb Peter Lammich : > So here is my question: > If I have some changeset, and want to check whether it breaks AFP > before pushing it to the isabelle repository, how do I do it? Can I use > Testboard? I don't know if you're using queues, but what I typically do in such (rare) cases is to qpop all, then pull and update, then qpush back to where I was, and then push the resulting "new" patch to Testboard again. This gives you a second shot and if you're lucky, it will get tested thoroughly. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
I always thought that there are two use-cases of Testboard: 1. Whenever you push to the Isabelle repository, this is tested by testboard 2. You can push your changeset only to testboard, to check it before pushing it to the isabelle repo and perhaps breaking it. However, according to Lars' reply, the second use-case is almost not possible, as a particular changeset will quickly be hidden by a huge number of later pushes to the isabelle repository, and never be touched again. So here is my question: If I have some changeset, and want to check whether it breaks AFP before pushing it to the isabelle repository, how do I do it? Can I use Testboard? -- Peter On Fr, 2013-09-27 at 11:49 +0200, Lars Noschinski wrote: > On 27.09.2013 09:16, Peter Lammich wrote: > > I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently > > only shown as 1/3 processed. Now, testboard seems to have stopped > > processing it ... however, many later pushs have already run through > > completely. > > > > What's the strategy to get your push on testboard processed within > > reasonable time? > > Basically Mira is just watching the repository. If a test run finishes, > it looks at the repository, takes the "tip" and tests it (if it was not > already tested). In particular, this means that later pushes can take > the focus away from your pushes. > > It might be a good idea to implement a strategy which tests the existing > heads in reverse chronological order (commits pushed last get tested > first), but I am not sure whether this information is available in > Mercurial (we have the commit date, but this is not necessarily related > to the push-date). > >-- Lars > ___ > 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] Testboard
On 27.09.2013 09:16, Peter Lammich wrote: I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within reasonable time? Basically Mira is just watching the repository. If a test run finishes, it looks at the repository, takes the "tip" and tests it (if it was not already tested). In particular, this means that later pushes can take the focus away from your pushes. It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard
Hi, I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within reasonable time? -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard: qpopping patches after pushing to tb
Hi, after pushing patches to the testboard, I got the following error when trying to qpop these patches: abort: popping would remove an immutable revision I investigated the problem and it turns out the problem is caused by mercurial's new phases feature introduced in v2.1 (see http://mercurial.selenic.com/wiki/WhatsNew#Mercurial_2.1_.282012-02-01.29) The guys at Mozilla ran into the same problem and found two easy solutions. One possibility is to solve the problem on the client side. When using an alias for the testboard, the solution looks something like this (note the post-tb hook): [path] testboard = ssh://smol...@macbroy21.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard [alias] tb = push -f testboard [hooks] post-tb = hg phase --force --draft "mq()" (see https://wiki.mozilla.org/ReleaseEngineering/TryServer#hg_phases for more details) However, there is also a global, server side solution. This would solve the problem for everybody. One would simply have to add [phases] publish = False to the hgrc file of the Testboard (and upgrade the server to >= hg 2.1). (see https://bugzilla.mozilla.org/show_bug.cgi?id=725362 for details) Regards, Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard [was: typedef (open) legacy]
On 10/10/2012 12:51 PM, Florian Haftmann wrote: I cannot connect to testboard at the moment, it seems to be in bad shape again. The testboard should now be in a running state again. For the record: is there any diagnosis what went wrong? On the webserver, spidermonkey was updated on Monday evening, and some changes were incompatible for couchdb. This caused couchdb to fail silently. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard [was: typedef (open) legacy]
I cannot connect to testboard at the moment, it seems to be in bad shape again. The testboard should now be in a running state again. For the record: is there any diagnosis what went wrong? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard interrupt tomorrow Wed 11th in the morning
Hi all, tomorrow Wed 11th in the morning (GMT) there will be an interrupt in the testboard due to maintainance works on the macbroy15 machine hosting its database. (Wed 11th of course, *not* 10th) Sorry for any inconvenience, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard interrupt tomorrow Wed 10th in the morning
Hi all, tomorrow Wed10th in the morning (GMT) there will be an interrupt in the testboard due to maintainance works on the macbroy15 machine hosting its database. Sorry for any inconvenience, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard reset: Old Testboard changesets are removed
Hi Lukas, I reset the testboard repository to start with a clean clone from the development repository and now everything should work again. If anyone is eager to restore the old testboard's changesets, we are happy for any assistance, otherwise we will discard them within the next week, if no one objects. I've had the same issue (for the same reason :-) ) once or twice before. Usually, running hg verify on the repository will tell you the first corrupted revision (usually the one you were pulling when running out of space/quota), and you can then clone everything else, which gets you back where you started. While it may be a good idea to clean up testboard once in a while (I am not sure how well hg scales to thousands of heads), we should try to archive the changesets somewhere. Otherwise it will be impossible to read old threads on the list, which sometimes refer to them. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard reset: Old Testboard changesets are removed
Hello all, Lars and I have taken over the maintenance of the reports and testboard from Alex yesterday. Today, due to some storage issues, we did not learn early enough about, the testboard repository changed into an inconsistent state. I reset the testboard repository to start with a clean clone from the development repository and now everything should work again. If anyone is eager to restore the old testboard's changesets, we are happy for any assistance, otherwise we will discard them within the next week, if no one objects. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
