<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="">I have to say, I’m absolutely mystified by the response to my suggestion.<div class=""><br class=""></div><div class="">MetiTarski, which during execution relies heavily on large integers, nevertheless benefits to the tune of 30% to having all other integers fixed-precision. During its execution, Isabelle makes very heavy use of small integers, in the representation of bound variables and flexible variables, which are renamed by having an offset before each and every resolution step.</div><div class=""><br class=""></div><div class="">We have spent a lot of time discussing problems caused by the cost of regression testing, and now we have the possibility of reducing that by 30%.</div><div class=""><br class=""></div><div class="">As to changes in behaviour that could be caused by overflows, I checked: exception Overflow is explicitly caught in only two places throughout the sources, both in HOL decision procedures (and therefore well outside the kernel) while the wildcard exception is caught in three places in Pure. No exception handlers had to be added when I converted MetiTarski to use fixed integers. An uncaught exception doesn’t prove anything, of course.</div><div class=""><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 2 Nov 2016, at 14:43, Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">On 02/11/16 15:30, Lawrence Paulson wrote:<br class=""><blockquote type="cite" class=""><br class="">I actually can’t think of many places where Isabelle would need large<br class="">integers, so it would probably benefit even more than MetiTarski does.<br class=""></blockquote><br class="">"Can't think of" merely indicates a lack of empirical tests, against the<br class="">Isabelle repository and AFP. Afterwards the situation usually looks<br class="">quite different, and the initial hypothesis needs to be changed.<br class=""><br class="">When we moved to proper int by default some years ago, there were<br class="">several tool implementors approaching me, asking to be delivered from<br class="">the curse of many different "int" types.<br class=""><br class="">We also have conceptual reasons to stay true to the concept of an<br class="">integer that is an integer, a string that is a string etc. -- and thus<br class="">not using a machine word instead of an integer, or a "char" type that<br class="">cannot hold a textual character (not even in Unicode). Isabelle/ML is<br class="">meant to be a programming environment free from bad jokes like that.<br class=""><br class=""><br class="">Nonetheless, I do think that proper use of machine words in isolated<br class="">situations can help, but they should not be called "int" and used by<br class="">default.<br class=""><br class=""><br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br class=""><br class=""></div></div></blockquote></div><br class=""></div></body></html>