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