[isabelle-dev] Jenkins reconfiguration

Makarius makarius at sketis.net
Fri Jun 29 19:24:55 CEST 2018


On 28/06/18 11:41, Lars Hupel wrote:
> Dear Isabelle developers,
> 
> you may have already noticed that some Jenkins jobs got reconfigured.
> 
> The following changes are relevant for developers:
> 
> - The new job "isabelle-all" runs Isabelle+AFP together, incrementally.
> This should improve overall performance and avoid double builds. There
> is, once again, an automatic "grace period" of 2 minutes to allow
> simultaneous Isabelle+AFP changes to be pushed before a build starts.
> <https://ci.isabelle.systems/jenkins/job/isabelle-all/>

Does it mean that the great new hardware is now locked up and
exclusively available for Jenkins?

Note that real Isabelle development requires running "isabelle build"
with varying options, e.g. I need a "build -o export_theory -d '$AFP'"
right now, but it will take some hours longer than necessary, on slower
hardware.

In the past, many people very also quite virtuous in doing
quasi-interactive builds: keeping the remote hardware busy on partial
builds while doing incremental updates locally. In those days we were
much more efficient in maintenance of Isabelle + AFP: the frequency of
changes has declined in recent years.


Anyway, I don't want to re-open the thread "What are the remaining uses
of Isabelle/Jenkins?".

Instead the question is: Why does Isabelle/Jenkins need exclusive access
to high-end hardware that it cannot even saturate?


	Makarius



More information about the isabelle-dev mailing list