<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div class="">
Larry
</div>
<div><br class=""><blockquote type="cite" class=""><div class="">On 3 May 2018, at 13:48, Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">On 03/05/18 14:04, Lawrence Paulson wrote:<br class=""><blockquote type="cite" class=""><blockquote type="cite" class=""><br class="">What is your changeset id?<br class=""></blockquote><br class="">~/isabelle/Repos/src/HOL: hg id<br class="">8dc792d440b9+ tip<br class=""></blockquote><br class="">That is after my change 0acf3206a723. Did you see the problem in<br class="">36209dfb981e, too?<br class=""></div></div></blockquote><div><br class=""></div><div>I have no idea how I could answer this question, as these change numbers appear to be absolutely random. I have recently been pulling changes every morning and I saw similar symptoms yesterday.</div><br class=""><blockquote type="cite" class=""><div class=""><div class="">What are the build options, e.g. the bottom of the output of "isabelle<br class=""><blockquote type="cite" class=""><blockquote type="cite" class="">build -?” ?<br class=""></blockquote></blockquote><br class="">The "isabelle build" tool with argument "-?" emits various settings for<br class="">convenience. <br class=""></div></div></blockquote><br class=""></div><div><div style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ISABELLE_BUILD_OPTIONS=""</span></div><p style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255); min-height: 15px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><br class="webkit-block-placeholder"></p><div style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ML_PLATFORM="x86-darwin"</span></div><div style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ML_HOME="/Users/lp15/.isabelle/contrib/polyml-5.7.1-5/x86-darwin"</span></div><div style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ML_SYSTEM="polyml-5.7.1"</span></div><div style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ML_OPTIONS="-H 1000"</span></div><div style="margin: 0px; font-stretch: normal; font-size: 13px; line-height: normal; font-family: Consolas; background-color: rgb(214, 254, 255); min-height: 15px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div></div><br class=""><div class="">Larry</div></body></html>