<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="">Version 5.7 doesn’t even build on my main workstation, though it works on my MacBook Pro running broadly similar software. No idea what is going on here, but I’m not happy about it.<br class=""><div class="">
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 11px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; "><div class="">Larry</div></span>
</div>
<br class=""><div><blockquote type="cite" class=""><div class="">On 15 May 2017, at 11:14, Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago<br class="">(see <a href="https://github.com/polyml/polyml/releases/tag/v5.7" class="">https://github.com/polyml/polyml/releases/tag/v5.7</a>), but announced<br class="">it only last week.<br class=""><br class="">I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that<br class="">is only for testing, not for production use. Some results can be seen here:<br class=""><br class=""><a href="http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html" class="">http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html</a><br class="">http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html<br class=""><br class="">The test hardware is similar or actually the same as "Linux A", but this<br class="">needs to be investigated further. It is also important to compare<br class="">timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task<br class="">is still busy digging into older history.<br class=""><br class=""><br class="">After the substantial changes of the code generator and representation<br class="">of ML values in memory, there are various open questions concerning<br class="">performance and robustness of Isabelle applications.<br class=""><br class="">This means, we need to skip the Poly/ML 5.7 release and stay on the last<br class="">Poly/ML 5.6 until the situation becomes more clear.<br class=""><br class=""><br class="">This is how to use the polyml-5.7 component locally:<br class=""><br class=""> $ edit $ISABELLE_HOME_USER/etc/settings<br class=""><br class=""> init_component "$HOME/.isabelle/contrib/polyml-5.7"<br class=""><br class=""> $ isabelle components -a<br class=""><br class=""><br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class="">isabelle-dev@in.tum.de<br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></div></div></blockquote></div><br class=""></body></html>