[isabelle-dev] Jenkins maintenance

Makarius makarius at sketis.net
Sat Oct 1 14:34:45 CEST 2016

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
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.


More information about the isabelle-dev mailing list