[isabelle-dev] [Isabelle-ci] Build failed in Jenkins: afp-repo-checkin #80

[Lawrence Paulson]

I hope I didn’t sound too critical. It’s a very impressive system, but I was anxious to get those problems fixed quickly. I see that somebody else got there first. (I frequently find theorems that are near-duplicates, which I eliminate, and generally I’m pretty good at locating all uses of the eliminated theorem, but a couple got away here.)
Larry

> On 25 Feb 2016, at 11:04, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> Forgive me if I’m overlooking something obvious, but the attached
>> message about a failure in the AFP doesn’t seem to include any clue
>> as to which of the 200+ entries actually failed. I spent a little
>> time poking around https://ci.isabelle.systems/jenkins/  without
>> learning anything more. Is there a way of getting a little more
>> information out of this system?
> 
> You're not overlooking anything: the mails are mostly useless right now.
> Apologies for the confusion. Be assured that I'm trying to make the new
> CI useful to everyone, but it's a long process and I can only do so much
> at a time.
> 
> Makarius, our admins and me have introduced the prerequisites to get the
> well-known "afptest"-style mails back (without Perl!).
> 
> My short-term agenda looks like this, in decreasing order of priority:
> - afptest-style mails
> - more useful mails to the general public
> - ISABELLE_FULL_TEST and ~~/src/Benchmarks
> - testboard_submit script for simultaneous Isabelle & AFP testing
> 
> I estimate to be done with this by mid-March.
> 
> Irrespective of that, here's an appeal to anyone, in the spirit of
> Jasmin: If you have any problems with or suggestions for the
> infrastructure, please ping me. If I know what users want I can avoid
> needless work.
> 
> Cheers
> Lars
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev