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


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

Reply via email to