> 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