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] NEWS: GCD and Binomial in Main

[Florian Haftmann]

Am 25.04.2017 um 11:06 schrieb Manuel Eberl:
> I think you actually solved that problem by now. If I recall correctly,
> it was one of the two dictionary-related problems I told you about a
> year ago or so, and then Lars and you solved that problem somehow.
> 
> I can try putting in that code equation again and seeing what happens.

Excellent, thanks.

Florian

> 
> 
>>> (*TODO: This code equation breaks Scala code generation in 
>>> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. 
>>> *)
> 
> Manuel
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Manuel Eberl]

I think you actually solved that problem by now. If I recall correctly,
it was one of the two dictionary-related problems I told you about a
year ago or so, and then Lars and you solved that problem somehow.

I can try putting in that code equation again and seeing what happens.


>> (*TODO: This code equation breaks Scala code generation in 
>> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)

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

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Florian Haftmann]

> * Theories "GCD" and "Binomial" are already included in "Main" (instead
> of "Complex_Main").
> 
> 
> This refers to Isabelle/f533820e7248: the change came up while exploring
> theory imports systematically. Normally, only "Main" or "Complex_Main"
> should be imported from the HOL session, not anything in between. (This
> is a concession to the complex bootstrap process of HOL.)
> 
> In Isabelle/85ed070017b7 Florian has already improved the imports of GCD
> further.
> 
> Are there good ideas how to do it with Binomial? Thus we could get rid
> of the Pre_Main theory from f533820e7248.

The import could be changed e.g. to Groups_List.

Desirable would also be to split the theory into Factorial and Binomial,
to raise awareness of existing combinatorial material in HOL.

As an aside, maybe someone is eager to take the comment

> (*TODO: This code equation breaks Scala code generation in 
> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)

seriously.

Cheers,
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

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