[isabelle-dev] Jenkins maintenance

[Makarius]

On 27/09/16 11:43, Lars Hupel wrote:
> 
> In an ideal world everyone would run "isabelle build -D $AFP -a -o
> document=pdf" before pushing, but clearly that is impractical.

According to the official README_REPOSITORY
(http://isabelle.in.tum.de/repos/isabelle/file/ec0fb01c6d50/README_REPOSITORY#l282)
there is

  * a strict obligation to make a full build -a, before pushing anything
to the Isabelle repository (also after the merge)

  * no need to test pdf documents

  * no need to have AFP in a fully working state (although it would be
nice to sort problems out eventually)


> That is not entirely true. Currently we cover 2, 6, and 8 threads on
> Linux and both 32 and 64 bit.

The 1 thread test is the base of all other tests. Without that it
becomes very difficult to see anything concerning performance changes.


> Missing Mac tests are not the fault of the infrastructure itself, but a
> result of a difficult hardware situation, imposed by Apple. Still, I'm
> working on it, as I've already told you earlier this month. However,
> it's not a deal-breaker: Many Mac users routinely use the development
> version; system bootstrapping or integration problems will get detected
> very early even without automated testing. (That doesn't change the fact
> that automated testing on Mac is imminent, hopefully early October.)

I am still hoping for October (which is actually now). I have explained
many times privately, what the purpose of "platform tests" is: a
portfolio of officially supported platforms -- some of them unusual for
most isabelle-dev users -- need to be continuously tested (meaning once
per day, or even once per week).

That platform coverage is especially important when we approach a
release -- that is a phase when components tend to be updated.


	Makarius