[isabelle-dev] Jenkins maintenance
nipkow at in.tum.de
Fri Oct 7 08:01:23 CEST 2016
On 06/10/2016 17:11, Makarius wrote:
> On 06/10/16 17:03, Tobias Nipkow wrote:
>> Sorry, I don't consider them useless.
>> On 06/10/2016 17:00, Makarius wrote:
>>> This is actually my main point of criticism for the present situation:
>>> the Jenkins setup uses a lot of hardware resources, by doing too many
>>> useless tests.
> I need to be more specific:
> * Why is a plain "nightly build" done many times per day? (As
> immediate reaction on repository pushes.)
> * Why are testboard policies intermixed with "nightly build" policies?
I can only guess what "nightly build" is: probably without the AFP. In which
case I can only repeat what was said more than once: we want to test as much as
possible in reasonable time, rather than with a delay of a day.
> Add-on question:
> * Why is there a testboard at all, instead of plain ssh access?
For one thing it makes sure that enough is tested (eg incl AFP and latex). We
find it very convenient.
A final point before I bow out. I am very grateful to Lars for setting up the
test infrastructure. This does not contribute but distracts from his PhD work
and his teaching duties. For that very reason he will tune Jenkins further as
required but he will not spend much time on it.
PS I have recently talked to a number of mathematicians who had taken a serious
look at Isabelle. Their main complaint was uniformly that the theories were
unreadable because there was not enough plain latex text in them.
> None of this has been seriously discussed so far.
> As far as I remember, the original Mira testboard was introduced in a
> situation, where builds became so slow and unwieldy that the mental
> model was changed to "batch-queue management" on a hypothetical
> computing cluster. Luckily, David Matthews saved us from that, and made
> everything small and fast again.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev