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 persist
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 som
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
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
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 require
> 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]
> pus
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 t
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.
>>>
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
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,
Flori
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.
>
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
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 c
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 (
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_haftman
15 matches
Mail list logo
