<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi Makarius,<div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 24 Apr 2017, at 18:12, Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">On 24/04/17 14:46, Makarius wrote:<br class=""><blockquote type="cite" class=""><br class="">Are there users of it outside the TUM group?<br class=""></blockquote></div></div></blockquote><div><br class=""></div><div>My usage is the same as in Jasmin’s and Andreas’ case.</div><br class=""><blockquote type="cite" class=""><div class=""><div class=""><blockquote type="cite" class=""><br class="">What is good about it? What is bad about it?<br class=""></blockquote><br class="">(1) To follow the line of Mira vs. Jenkins:<br class=""><br class=""> * My main use of Mira was to figure out which Isabelle version<br class="">corresponds to which AFP version, when something was broken in AFP.<br class=""><br class=""> * I did not find this information in Jenkins, when I was still<br class="">spending more time on it last year.<br class=""></div></div></blockquote><div><br class=""></div><div>It is there on the status page: <a href="https://ci.isabelle.systems/jenkins/job/afp-repo-afp/827/" class="">https://ci.isabelle.systems/jenkins/job/afp-repo-afp/827/</a></div><div><br class=""></div><div><pre class="console-output" style="box-sizing: border-box; white-space: pre-wrap; word-wrap: break-word; margin-top: 0px; margin-bottom: 0px; color: rgb(51, 51, 51); font-size: 13px;"></pre><blockquote type="cite" class=""><pre class="console-output" style="box-sizing: border-box; white-space: pre-wrap; word-wrap: break-word; margin-top: 0px; margin-bottom: 0px; color: rgb(51, 51, 51); font-size: 13px;"><img alt="" style="box-sizing: border-box; vertical-align: middle; border: 0px; margin-right: 1em;" apple-inline="yes" id="FCF4481D-23FA-443A-AF41-D51812A58D64" src="cid:9748E4E4-EC14-42D3-AB50-096883F51C99@inf.ethz.ch" class=""><b style="box-sizing: border-box;" class="">Revision</b>: c05bec5d01ad6660f7825f6a8315f9aa350a7a67</pre><pre class="console-output" style="box-sizing: border-box; white-space: pre-wrap; word-wrap: break-word; margin-top: 0px; margin-bottom: 0px; color: rgb(51, 51, 51); font-size: 13px;"><img alt="" style="box-sizing: border-box; vertical-align: middle; border: 0px; margin-right: 1em;" apple-inline="yes" id="CDB9C2FC-DE1B-420E-A23B-0CEB99D77861" src="cid:9748E4E4-EC14-42D3-AB50-096883F51C99@inf.ethz.ch" class=""><b style="box-sizing: border-box;" class="">Revision</b>: fd20a4c244d80bf87ea3f367c66c93b6164c85ce</pre></blockquote><div><br class=""></div><div>And it was there from the beginning: <a href="https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1/" class="">https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1/</a></div><div><br class=""></div><div>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).</div></div><div><br class=""></div><blockquote type="cite" class=""><div class=""><div class=""><br class=""> * For actual quasi-interactive testing I always use "isabelle build"<br class="">directly on a local or remote machine, with incrementally updated global<br class="">build state (heaps and logs). Here it is important to get results within<br class="">approx. 20-30 min -- presently we are at > 30 min.</div></div></blockquote><br class=""></div></div><div>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.</div><div><br class=""></div><div>Dmitriy</div><div><br class=""></div><div><br class=""></div></body></html>