Hi Makarius,

> On 24 Apr 2017, at 18:12, Makarius <makar...@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: 

> Revision: c05bec5d01ad6660f7825f6a8315f9aa350a7a67
> Revision: fd20a4c244d80bf87ea3f367c66c93b6164c85ce

And it was there from the beginning: 

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 


isabelle-dev mailing list

Reply via email to