[isabelle-dev] Jenkins maintenance

[Makarius]

On 24/09/16 17:47, Lars Hupel wrote:
>> This reminds me of a still open question: Why is there this "continuous
>> integration" on every push anyway?
> 
> This question is not open; it has been answered quite often in the past.
> 
> For the repositories, it serves as a reminder to not push "broken"
> changes. (Or at least repair problems when they appear, with a clear
> picture of what exactly happened.) This may happen to all of us, and in
> fact, happens to all of us.

It happens to very few people, only every 1-2 years. Such incidents are
not a problem and need not be taken into account of technical engineering.


In contrast, the present real-time testing of the repositories (not
testboards) introduces real problems that are unnecessary.

It wastes CPU resources that are missing for important tests: coverage
of thread parameters and other platform options is presently at 10-20%
of what the last isatest setup was doing (which was already in a state
of decline). We are flying mostly blind for a long time.


We have also lost the correlation of Isabelle vs. AFP.

In the past, there was usually an accidental pairing of both repository
snapshots, because tests were started at a fixed time after midnight
when nobody was pushing.

By recording the two repository ids together with the nightly build
status, it is usually easy to find a working state of particular AFP
entries, based on a suitable Isabelle version.


> For the testboards, the answer is even simpler: developers would like to
> get immediate feedback for testing bigger changes without a manual hg
> push/ssh/isabelle build cycle. This is hardly a new concept – it's not
> just industry standard, but even best practice (the term "Continuous
> integration" itself traces back to 1991). There is no point in going
> back to an outdated development model.

That is a different game. The testboards emulate a batch-job queue
manager. If Jenkins can do that -- fine. There is otherwise no
connection to repository testing. No need to pretend that Isabelle
repository testing is instantaneous like the testboard.


You could easily improve both the repository testing and testboard
reactivity as follows:

  * 8 hours during the night (in Europe) are used for testing repository
versions, e.g. one changeset id with many thread / platform parameters.
(A smarter setup would incrementally dig into the repository history, as
far as elapsed time permits.)

  * The remaining 16 hours of the day are available for testboard jobs,
with instantaneous reaction of pushes.


	Makarius