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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
