Re: [isabelle-dev] Uses of Jenkins at TUM

[Makarius]

On 25/04/17 09:41, Mathias Fleury wrote:
>  
>> What is good about it?
> (I don't remember enough of the previous system to compare it to Jenkins.)

Lets go back to some points on this thread, now that I have finished
more implementation work.


>   * automatic testing (I have forgotten to add files a couple of times).

Forgetting to add files in a commit was one of the few cases where the
remote test actually had a benefit. The start of this thread was such an
incident, see Isabelle/006a274cdbc2.

Thinking once more about the problem, it is clear that the standard
"isabelle build" tool can do that check on the spot.  See now:

changeset:   65829:2fb85623c386
user:wenzelm
date:Sun May 14 20:16:13 2017 +0200
files:   src/Pure/General/mercurial.scala src/Pure/Tools/build.scala
description:
implicitly check for unknown files (not part of a Mercurial repository);

 src/Pure/General/mercurial.scala |  31 +++
 src/Pure/Tools/build.scala   |  15 +++
 2 files changed, 46 insertions(+), 0 deletions(-)



>   * timings
> 
> (https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html).
> It is useful to see how it evolves over time.

I actually made this myself in reminiscence of the old isatest
statistics, see also various mails in the vicinity of
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-August/007070.html

In that discussion it also became clear that Jenkins lacks scalable test
data management: queries via its API are very slow. This ultimately
motivated the PostgreSQL database server that is now behind
http://isabelle.in.tum.de/devel/build_status/index.html (PostgreSQL is a
great product that does its job very well without much ado.)


To reintegrate the old data source, I have added a function to download
Jenkins logs into the same log directory as the other build_status
information, see:

http://isabelle.in.tum.de/repos/isabelle/rev/2773b6859c55
http://isabelle.in.tum.de/devel/build_status/jenkins_isabelle-nightly-benchmark_64bit_6_threads/index.html
http://isabelle.in.tum.de/devel/build_status/jenkins_isabelle-nightly-slow_64bit_8_threads/index.html

This replaces the former chart plotting directly from Jenkins, so Lars
can now dismantle https://ci.isabelle.systems/statistics (which still
says "Generated at Tue, 18 Apr 2017 00:02:04 GMT").


Makarius

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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Makarius]

On 24/04/17 14:46, Makarius wrote:
> This is another attempt to open a discussion about Jenkins at TUM.

Thanks to everyone who participated on this thread. I have learned a few
new things, which I will pick up again soon.


Makarius

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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Simon Wimmer]

Hi Makarius,

I think everyone involved with this issue is interested in coming back to a
situation where we have a solution that works for everyone.
Can we try to find a proposal for a change of the current infrastructure
that accommodates for yours and others' missing requirements?

On Mon, Apr 24, 2017 at 6:12 PM Makarius  wrote:

> On 24/04/17 14:46, Makarius wrote:
> >
> > Are there users of it outside the TUM group?
> >
> > What is good about it? What is bad about it?
>
> (1) To follow the line of Mira vs. Jenkins:
>
>   * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.


>   * I did not find this information in Jenkins, when I was still
> spending more time on it last year.


Is what Dmitriy pointed out (the status page) sufficient?


>   * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.
>

We can think of multiple solutions to bring down the testboard build times
to 'quasi-interactive'.
This could also include incremental builds for the distribution if wanted.
Would you use the testboard if this was possible?


> (2) To follow the line of Jenkins vs. isatest:
>
> When Jenkins was about to supersede isatest last year, I put forward
> missing requirements e.g. here:
>
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html


Let me restate these:

* Realistic tests with typical settings. This means that x86 (and not
x86_64) is used by default. We've recently seen mysterious resource
problems occasionally, and the automatic testing infrastructure should be
able to point quickly to relevant changesets.

We now have a periodic build job for x86, too. Why would you still opt for
x86 as a default, considering it is very hard to get rid of spurious
failures in this setting (as Lars pointed out below)?

* Decent performance measurements and charts: both multi-core run-time and
heap space requirements.

Your point of criticism seems to be that the currently available charts are
not as reliable as what was available many years ago. However, this seems
to already have been a problem in the pre-Jenkins times. Can you suggest a
scheme to get more reliable measurements?


>
>
> Today we have already the isatest sucessor "isabelle_cronjob" in
> Isabelle/Scala, and a proper discussion wrt. Jenkins needs to continue
> there. See also
>
> http://isabelle.in.tum.de/repos/isabelle/file/f8681c62959d/src/Pure/Admin/isabelle_cronjob.scala
>
> The latter is all about Isabelle administration infrastructure, i.e. the
> parts that are only seen when they don't work properly.
>
>
What I take away from this thread so far is that most users generally seem
to be happy with the Jenkins infrastructure. Thus, we are happy to continue
the discussion, but I do not see why we would need a completely different
testing infrastructure.


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


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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Lars Hupel]

>   * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.
> 
>   * I did not find this information in Jenkins, when I was still
> spending more time on it last year.

This information is all there. Build status is accessible via the
Jenkins API, of which you are undoubtedly aware. We also had both public
and private conversations where I pointed out to you where this is
available.

The user-facing side of this is
, which broke sometime around
Isabelle/7ca8810b1d48 though no change of my own, but so far I haven't
had time to investigate what caused it. (All entries are marked as
"skipped".)

>   * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.

This has also already been discussed. The vast majority of people I
asked is interested in quick feedback about AFP, which the testboard
provides.

> When Jenkins was about to supersede isatest last year, I put forward
> missing requirements e.g. here:
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html

This has also already been discussed. Testing with x86 caused too many
spurious failures, even after countless hours of tweaking parameters. I
refuse to take flak for reducing build noise.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Uses of Jenkins at TUM

[Dmitriy Traytel]

Hi Makarius,

> On 24 Apr 2017, at 18:12, Makarius  wrote:
> 
> On 24/04/17 14:46, Makarius wrote:
>> 
>> Are there users of it outside the TUM group?

My usage is the same as in Jasmin’s and Andreas’ case.

>> 
>> What is good about it? What is bad about it?
> 
> (1) To follow the line of Mira vs. Jenkins:
> 
>  * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.
> 
>  * I did not find this information in Jenkins, when I was still
> spending more time on it last year.

It is there on the status page: 
https://ci.isabelle.systems/jenkins/job/afp-repo-afp/827/

> Revision: c05bec5d01ad6660f7825f6a8315f9aa350a7a67
> Revision: fd20a4c244d80bf87ea3f367c66c93b6164c85ce

And it was there from the beginning: 
https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1/ 


It would help if we would not need to guess which id is for isabelle and which 
one is for the AFP though (although this is easy to figure out).

> 
>  * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.

Since I usually change things early in HOL (around BNF_Def), incremental builds 
would not save a lot. I think the time spend on non-HOL logics is not zero but 
negligible.

Dmitriy


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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Mathias Fleury]

Hello all,


First, I would like to thank Lars for the time he is spending on Jenkins.


On 24.04.17 17:47, Blanchette, J.C. wrote:
>> On 24 Apr 2017, at 17:12, Andreas Lochbihler 
>>  wrote:
>>
>> Sure. Whenever I have to push something to the Isabelle repository, I use 
>> the Jenkins testboard installation to see whether something broke. It works 
>> more reliably than the previous testboard infrastructure, which often 
>> ignored some commits.
> The same applies to me (VU Amsterdam), and I believe Mathias Fleury (MPII 
> Saarbrücken) is also a heavy user of Testboard when he modifies Isabelle 
> (e.g. the multiset library).
>
> From a pure basic user's perspective, I don't see much of a difference 
> between Mira and Jenkins. To me it's just Testboard, and most of the time it 
> works, and then I'm happy. Sometimes Mathias just sends me a link to a patch 
> he's pushed to Testboard for me to review, before he pushes it to Isabelle. 
> That's also very useful.
Indeed. (Actually, patches can be seen here
 or here for AFP-testboard
, but both are unrelated to
Jenkins).
 
> What is good about it?
(I don't remember enough of the previous system to compare it to Jenkins.)

  * automatic testing (I have forgotten to add files a couple of times).

  * timings

(https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html).
It is useful to see how it evolves over time.


>  What is bad about it?
I am trying very hard to not break Isabelle and the AFP. Therefore, I
hate receiving an email of Jenkins telling me that I have broken something.

  * Spurious timeouts (like nightly-mac

currently). At some point, there were timeouts that appeared after
one of my changes, but I could not reproduce them (they were related
to timeouts of quickcheck). Interestingly, I am now in the opposite
situation: At home, I currently have a lot of timeouts related to
"export_code" in Refine_Imperative_HOL that do not appear in
Jenkins. I will send another email to the mailing list related to that.

  * Testing both Isabelle and AFP changes would be nice. This is
especially important for multisets that are not widely used in
Isabelle: Most bad simp rule break the AFP, not Isabelle.



However, both problems are hard to solve and I am happy with the current
situation. I even run a Jenkins instance at home.



Mathias
> Jasmin
>
> ___
> 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] Uses of Jenkins at TUM

[Makarius]

On 24/04/17 18:10, Lars Hupel wrote:
>> In parallel (before and after Mira) we've had the older isatest. I don't
>> know if Mira ever had the ambition to replace isatest, but Jenkins tried
>> to do all that and failed. This was the start of my great worries about
>> the Isabelle administration and release infrastructure ...
> 
> So, you're just going to unilaterally declare that it all failed and we
> should take your word for that?

I am speaking as a "customer", i.e. the one responsible for certain
administrative tasks.

The old isatest was part of that and slowly falling into decay. You
proposed a new project based on Jenkins, and we spent a lot of time
discussing that to get to a point where it could eventually replace
isatest. The new project did not meet these requirements. In that sense
it failed.

See again the somewhat arbitrary entry point
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html


Makarius

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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Lars Hupel]

> In parallel (before and after Mira) we've had the older isatest. I don't
> know if Mira ever had the ambition to replace isatest, but Jenkins tried
> to do all that and failed. This was the start of my great worries about
> the Isabelle administration and release infrastructure ...

So, you're just going to unilaterally declare that it all failed and we
should take your word for that?

The cliché that "Jenkins did X" is getting a bit old. At least be honest
and say my name, because it is me who built up that infrastructure. (Not
without external input, constraints, and requirements, but still.)

Finally, let me make one thing very clear: I strongly object to this
passive-aggressive attitude (not just about Jenkins, even). I have
little interest in arguing if there's not even a trace of mutual
understanding and charity.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Uses of Jenkins at TUM

[Blanchette, J.C.]

> On 24 Apr 2017, at 17:12, Andreas Lochbihler  
> wrote:
> 
> Sure. Whenever I have to push something to the Isabelle repository, I use the 
> Jenkins testboard installation to see whether something broke. It works more 
> reliably than the previous testboard infrastructure, which often ignored some 
> commits.

The same applies to me (VU Amsterdam), and I believe Mathias Fleury (MPII 
Saarbrücken) is also a heavy user of Testboard when he modifies Isabelle (e.g. 
the multiset library).

From a pure basic user's perspective, I don't see much of a difference between 
Mira and Jenkins. To me it's just Testboard, and most of the time it works, and 
then I'm happy. Sometimes Mathias just sends me a link to a patch he's pushed 
to Testboard for me to review, before he pushes it to Isabelle. That's also 
very useful.

Jasmin

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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Makarius]

On 24/04/17 17:12, Andreas Lochbihler wrote:
> Sure. Whenever I have to push something to the Isabelle repository, I
> use the Jenkins testboard installation to see whether something broke.
> It works more reliably than the previous testboard infrastructure, which
> often ignored some commits.

Thanks for contributing to the discussion.

The previous testboard was called "Mira" and done by Alex Krauss and
Florian Haftmann some years ago. It would be also interesting to go back
to that: What were its aims and its approach? Why did it not work out?
How does that compare to the new testboard based on Jenkins?

In parallel (before and after Mira) we've had the older isatest. I don't
know if Mira ever had the ambition to replace isatest, but Jenkins tried
to do all that and failed. This was the start of my great worries about
the Isabelle administration and release infrastructure ...


Makarius

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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Andreas Lochbihler]

Sure. Whenever I have to push something to the Isabelle repository, I use the Jenkins 
testboard installation to see whether something broke. It works more reliably than the 
previous testboard infrastructure, which often ignored some commits.


Andreas

On 24/04/17 14:46, Makarius wrote:

This is another attempt to open a discussion about Jenkins at TUM.

Are there users of it outside the TUM group?

What is good about it? What is bad about it?


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