Re: [isabelle-dev] Small repository accident
On Fri, 24 Feb 2012, Alexander Krauss wrote: The practical issues it adresses: It gives you convenient and fast feedback about whether Isabelle_makeall on your changeset(s) succeeds. In particular, it is useful if you do not have a fast machine for yourself. It also makes the results persistent -- at least that was one of the initial motivations. Did that work out in retrospective? Concerning "a fast machine for yourself", I do it the old-fashioned way via rsync and then test remotely in batch mode before committing. Another old-fashioned mode of operation is to make a remote shell session for the front-end, so one could test such things interactively. Proof General used to have some rsh feature, before ssh even existed, but it seems now out-of-use or discontinued. When doing the local socket connection for Scala <-> ML for Windows/Cygwin (where a plain named pipe is unreliable), I realized again that one could somehow make non-local sockets part of the game by default. This is particularly relevant for Swing applications, because X11 display forwarding does not really work here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
On 02/24/2012 04:23 PM, Makarius wrote: Where do I have to look for explanations about testboard? It would help to understand the practical issues that it addresses, so that the emerging renovations of the build and test process of Isabelle/Scala move in the same general direction. I posted some basic instructions to the list a while ago, which we could update and move to the Wiki now: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-May/001506.html The practical issues it adresses: It gives you convenient and fast feedback about whether Isabelle_makeall on your changeset(s) succeeds. In particular, it is useful if you do not have a fast machine for yourself. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On Fri, 24 Feb 2012, Lukas Bulwahn wrote: Maybe we could also get performance measurements for the new session? See now 1258eab48270. I have also updated the IsaMakefile itself in 2190af0ef263. All this redundancy in the session management is well-known and waiting to be eliminated for many years. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
On Fri, 24 Feb 2012, Florian Haftmann wrote: A nice client-side solution is also: [paths] testboard = ssh://haftmann@macbroy//mnt/tmp/isatest/repositories/isabelle [alias] push_to_testboard = push -f testboard in .hg/hgrc Very nice indeed; these Mercurial guys know what is needed. This should also work well for central $HOME/.hgrc -- it assumes that the meaning of the "testboard" path is somehow uniform, independently of clones. Is there a way to pull the .hgrc also on hg clone? Then this could be a default .hgrc for the Isabelle repository. According to the pure concepts of Mercurial the hgrc is a local thing, which is never cloned. (Never versions might have introduced other solutions more recently.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
On Fri, 24 Feb 2012, Florian Haftmann wrote: I would also prefer a server-side solution in the testboard repositories This usually means hooks, but hooks are not very useful with the direct user access model that we have, via the local file-system and possibly indirected via ssh. It requires users to permit such hooks explicitly in their hgrc, so we are back to the client. Moreover, after some initial experimentation with hooks when we've done the CVS -> Migration some years ago have left an odd impression to me. Too many things can go wrong in the hook. It is better to work in a way that big mistakes don't happen (which we managed very well in recent years). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
> Indeed. I would also prefer a server-side solution in the testboard > repositories (is there any way to permit a push generating new heads in > .hg/hgrc?) A nice client-side solution is also: > [paths] > testboard = ssh://haftmann@macbroy//mnt/tmp/isatest/repositories/isabelle > [alias] > push_to_testboard = push -f testboard in .hg/hgrc Is there a way to pull the .hgrc also on hg clone? Then this could be a default .hgrc for the Isabelle repository. 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] Small repository accident
Hi all, >> It is also possible to have .hg/hgrc specific to individual repository >> clones. So if testboard users are instructed to augment only that >> hgrc with the evil option once and for all, the problem of getting >> used to evil command lines in a different context is avoided. > > This thread shows that I am not using testboard myself. Isn't it used > mainly by pushing the same clone to a different target? So the above > does not work that way. Indeed. I would also prefer a server-side solution in the testboard repositories (is there any way to permit a push generating new heads in .hg/hgrc?) > Where do I have to look for explanations about testboard? It would help > to understand the practical issues that it addresses, so that the > emerging renovations of the build and test process of Isabelle/Scala > move in the same general direction. Neither the generic mira nor the specific testboard so far have any public prominence; there are some documentation snippets in the doc directory of the mira sources, e.g. http://isabelle.in.tum.de/repos/mira/file/16f40e322e50/doc/tum_guide.txt (this is surely outdated, e.g. cf. ll. 52/52: »NOTE: This is at least the idea; the current infrastructure does not yet make this very feasible in practice.«) 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] Quickcheck Examples
Hi Lukas, Am 24.02.2012 09:09, schrieb Lukas Bulwahn: > On 02/18/2012 10:18 AM, Florian Haftmann wrote: >>> How much relative time do the quickcheck examples in HOL-ex take? >>> According to my feeling time could be high to separate these into a >>> separate session, to facilitate maintenance. >>> > I separated the Quickcheck-Examples from HOL-ex into an own session (cf. > http://isabelle.in.tum.de/repos/isabelle/rev/f462e49eaf11) thanks a lot. > The latest performance numbers do not show that the run time reduced, so > either there is really another bottleneck or my own change has not had > any effect on the measurements yet? > (cf. http://isabelle.in.tum.de/devel/stats/at-poly/HOL-ex.png) Now it had. > If Library-Codegenerator-Test works, you only know that you get source > code that compiles correctly. > With the Quickcheck-Examples session, you know that the source code also > runs correctly. On the other hand, Library-Codegenerator-Test is more pervasive. Cheers, 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] Small repository accident
On Fri, 24 Feb 2012, Makarius wrote: It is also possible to have .hg/hgrc specific to individual repository clones. So if testboard users are instructed to augment only that hgrc with the evil option once and for all, the problem of getting used to evil command lines in a different context is avoided. This thread shows that I am not using testboard myself. Isn't it used mainly by pushing the same clone to a different target? So the above does not work that way. Where do I have to look for explanations about testboard? It would help to understand the practical issues that it addresses, so that the emerging renovations of the build and test process of Isabelle/Scala move in the same general direction. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
On Fri, 24 Feb 2012, Lukas Bulwahn wrote: On 02/24/2012 09:01 AM, Florian Haftmann wrote: Accidentally I have pushed something into the main repository which was still supposed to be tested. PLEASE IGNORE HEAD REVISION 0bd7c16a4200 and continue with the other head. Sorry for this, Florian I was close to this mistake myself a couple of times already. It is the "evil" -f option with is now standard when pushing to the testboard -- accidently pushing to the public repository (with -f) is then done without checking as well. Isn't there a easy way to allow pushing to the testboard without writing "-f" but still allowing to create new heads? Then we would never use the -f option and cannot get into this trouble. The hgrc file allows to specify default command line options for each command. For example, I have harmless things like this in ~/.hgrc: [defaults] status = --color=always diff = --color=always log = -l 7 -v It is also possible to have .hg/hgrc specific to individual repository clones. So if testboard users are instructed to augment only that hgrc with the evil option once and for all, the problem of getting used to evil command lines in a different context is avoided. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
Am 24.02.2012 um 09:16 schrieb Lukas Bulwahn: > I was close to this mistake myself a couple of times already. > > It is the "evil" -f option with is now standard when pushing to the testboard > -- accidently pushing to the public repository (with -f) is then done without > checking as well. > > Isn't there a easy way to allow pushing to the testboard without writing "-f" > but still allowing to create new heads? > Then we would never use the -f option and cannot get into this trouble. There's a much easier solution. Write a little script called "tb" that looks like this: (cd ~/isabelle; hg push -f testboard) Then you'll never need to pass "-f" again in your life. No need for fancy hooks or anything. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
On 24.02.2012 09:16, Lukas Bulwahn wrote: On 02/24/2012 09:01 AM, Florian Haftmann wrote: Accidentally I have pushed something into the main repository which was still supposed to be tested. PLEASE IGNORE HEAD REVISION 0bd7c16a4200 and continue with the other head. Sorry for this, Florian I was close to this mistake myself a couple of times already. It is the "evil" -f option with is now standard when pushing to the testboard -- accidently pushing to the public repository (with -f) is then done without checking as well. Isn't there a easy way to allow pushing to the testboard without writing "-f" but still allowing to create new heads? Then we would never use the -f option and cannot get into this trouble. One could instead install a hook in the main repository which prevents multiple heads via push: http://mercurial.selenic.com/wiki/TipsAndTricks#Prevent_a_push_that_would_create_multiple_heads -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Small repository accident
On 02/24/2012 09:01 AM, Florian Haftmann wrote: Accidentally I have pushed something into the main repository which was still supposed to be tested. PLEASE IGNORE HEAD REVISION 0bd7c16a4200 and continue with the other head. Sorry for this, Florian I was close to this mistake myself a couple of times already. It is the "evil" -f option with is now standard when pushing to the testboard -- accidently pushing to the public repository (with -f) is then done without checking as well. Isn't there a easy way to allow pushing to the testboard without writing "-f" but still allowing to create new heads? Then we would never use the -f option and cannot get into this trouble. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On 02/18/2012 10:18 AM, Florian Haftmann wrote: How much relative time do the quickcheck examples in HOL-ex take? According to my feeling time could be high to separate these into a separate session, to facilitate maintenance. I separated the Quickcheck-Examples from HOL-ex into an own session (cf. http://isabelle.in.tum.de/repos/isabelle/rev/f462e49eaf11) The latest performance numbers do not show that the run time reduced, so either there is really another bottleneck or my own change has not had any effect on the measurements yet? (cf. http://isabelle.in.tum.de/devel/stats/at-poly/HOL-ex.png) Maybe we could also get performance measurements for the new session? I hope it facilitates maintenance nevertheless. Although if Quickcheck fails (or does not terminate) after some changes, this usually indicates that there is some flaw in the code generation setup. If Library-Codegenerator-Test works, you only know that you get source code that compiles correctly. With the Quickcheck-Examples session, you know that the source code also runs correctly. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Small repository accident
Accidentally I have pushed something into the main repository which was still supposed to be tested. PLEASE IGNORE HEAD REVISION 0bd7c16a4200 and continue with the other head. Sorry for this, 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
