Re: [isabelle-dev] Distro broken

[Makarius]

On 20/10/16 10:19, Tobias Nipkow wrote:
> We never promised that the new test infrastructure would guarantee that
> nobody will break the repository anymore. You are perfectly aware of
> this. So stop trolling.

> On 19/10/2016 13:52, Makarius wrote:
>> On 19/10/16 13:38, Lars Hupel wrote:
>>> Oh, nothing went wrong: Jenkins sent an email immediately after the
>>> push, and the status page also indicated the failure. Automation working
>>> as expected.

>> The open question is if the massive use of CPU resources by Jenkins is
>> justified to deliver its service. It is still unclear to me what this
>> service is in the first place.

Anybody wants to start a proper discussion on that?

When I asked Lars Hupel some months ago, he said I should open a thread
on the mailing list.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Distro broken

[Tobias Nipkow]

We never promised that the new test infrastructure would guarantee that nobody 
will break the repository anymore. You are perfectly aware of this. So stop 
trolling.


Tobias


On 19/10/2016 13:52, Makarius wrote:

On 19/10/16 13:38, Lars Hupel wrote:

Oh, nothing went wrong: Jenkins sent an email immediately after the
push, and the status page also indicated the failure. Automation working
as expected.


But that did not help. Florian experienced the broken repository just in
the way it occasionally happens.

The open question is if the massive use of CPU resources by Jenkins is
justified to deliver its service. It is still unclear to me what this
service is in the first place.

So far there were only axioms about Jenkins, but no proofs.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Distro broken

[Makarius]

On 19/10/16 13:38, Lars Hupel wrote:
> Oh, nothing went wrong: Jenkins sent an email immediately after the
> push, and the status page also indicated the failure. Automation working
> as expected.

But that did not help. Florian experienced the broken repository just in
the way it occasionally happens.

The open question is if the massive use of CPU resources by Jenkins is
justified to deliver its service. It is still unclear to me what this
service is in the first place.

So far there were only axioms about Jenkins, but no proofs.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Distro broken

[Lars Hupel]

Oh, nothing went wrong: Jenkins sent an email immediately after the push, and 
the status page also indicated the failure. Automation working as expected.

Cheers
Lars

On 19 October 2016 11:11:21 CEST, Makarius  wrote:
>> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
 *** No such file:
 "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess
 ential_Supremum.thy"
>
>On 19/10/16 00:19, Johannes Hölzl wrote:
>> My bad, should be fixed now.
>
>That is the traditional situation that someone pulling from the
>repository sees a total existence failure and reports it manually on
>the
>mailing list.
>
>So far, the main argument for the massive waste of CPU resources by
>Jenkins was to make that report automatic.
>
>What happened that it did not work here?
>
>
>BTW, isabelle could easily detect the situation of missing files in the
>repository and emit a warning. I will add that in the next round of
>refinement (after the release).
>
>
>   Makarius
>
>___
>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] Distro broken

[Johannes Hölzl]

My bad, should be fixed now.

 - Jo

Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
> > 
> > isabelle: fb5c74a58796 tip
> > afp: c03838321f2a tip
> > *** No such file:
> > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess
> > ential_Supremum.thy"
> > *** The error(s) above occurred for theory "Essential_Supremum"
> > *** (required by "Probability") (line 15 of
> > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Pro
> > bability.thy")
> > *** The error(s) above occurred in session "HOL-Probability" (line
> > 716 of "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/ROOT")
>   Florian
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Distro broken

[Florian Haftmann]

> isabelle: fb5c74a58796 tip
> afp: c03838321f2a tip
> *** No such file: 
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Essential_Supremum.thy"
> *** The error(s) above occurred for theory "Essential_Supremum"
> *** (required by "Probability") (line 15 of 
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Probability.thy")
> *** The error(s) above occurred in session "HOL-Probability" (line 716 of 
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/ROOT")

Florian

-- 

PGP available:
http://isabelle.in.tum.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