[isabelle-dev] Uses of Jenkins at TUM

[Dmitriy Traytel]

Hi Makarius,

> On 24 Apr 2017, at 18:12, Makarius <makarius at sketis.net> wrote:
> 
> On 24/04/17 14:46, Makarius wrote:
>> 
>> Are there users of it outside the TUM group?

My usage is the same as in Jasmin’s and Andreas’ case.

>> 
>> What is good about it? What is bad about it?
> 
> (1) To follow the line of Mira vs. Jenkins:
> 
>  * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.
> 
>  * I did not find this information in Jenkins, when I was still
> spending more time on it last year.

It is there on the status page: https://ci.isabelle.systems/jenkins/job/afp-repo-afp/827/

> Revision: c05bec5d01ad6660f7825f6a8315f9aa350a7a67
> Revision: fd20a4c244d80bf87ea3f367c66c93b6164c85ce

And it was there from the beginning: https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1/ <https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1/>

It would help if we would not need to guess which id is for isabelle and which one is for the AFP though (although this is easy to figure out).

> 
>  * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.

Since I usually change things early in HOL (around BNF_Def), incremental builds would not save a lot. I think the time spend on non-HOL logics is not zero but negligible.

Dmitriy


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170425/7d21e296/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: logo.png
Type: image/png
Size: 3100 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170425/7d21e296/attachment-0002.png>