Re: [isabelle-dev] Jenkins reconfiguration

[Makarius]

On 29/06/18 19:31, Lars Hupel wrote:
>> Does it mean that the great new hardware is now locked up and
>> exclusively available for Jenkins?
> 
> That assessment is accurate.

That is bad.

It means that the development process will continue to decline, as we
have seen in the past few years -- it can be indirectly see by the
decreasing number of changes, substantial reforms etc. that were pushed
through.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

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


That assessment is accurate.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins reconfiguration

[Makarius]

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

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

Re: [isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

> - The "testboard" job will also be replaced to run Isabelle+AFP
> together. Historic builds will be deleted, as they are not relevant for
> the official history.

I have implemented this now. I'm currently monitoring the situation, but
so far, it seems like this sped up the process overall.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

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.


- The jobs "afp-repo" and "isabelle-repo" and subjobs will disappear
from the front page and the status page soon. Old links will continue to
work (i.e. historic builds will not be deleted).

- The "testboard" job will also be replaced to run Isabelle+AFP
together. Historic builds will be deleted, as they are not relevant for
the official history.

Some display changes:

Jenkins will show a failure summary on the link that is in the email
(example in the attachment).

There are more changes related to the testboard in the pipeline.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev