[isabelle-dev] Integers in Poly/ML

[Lawrence Paulson]

Okay then. Obviously proceed with caution, as always.

MetiTarski also has high standards, and doesn’t have the added security of a kernel architecture. Every significant change is checked by regression testing using tools that highlight significant changes in the runtime of the full test suite. This test suite includes many statements known to be false in order to catch soundness errors. Not that I was expecting any in this case: the required changes were small and logically trivial (mainly, converting between large and small integers).

I think it would be quite straightforward to try the experiment of building Isabelle with the new compiler, but I would need some help with our present setup (whereas I recall we keep our own copy of the compiler packaged in a special way somewhere). Also now is perhaps about time to accumulate changes, though I don’t expect to see many.

Can we wait until the next release is out? And yes, I could do it myself.

Is the question of 32 versus 64 bits relevant here? I suspect it isn’t. Any integers of ours requiring more than 32 bits need to be large integers.

Larry

> On 2 Nov 2016, at 15:29, Makarius <makarius at sketis.net> wrote:
> 
> On 02/11/16 15:58, Lawrence Paulson wrote:
>> I have to say, I’m absolutely mystified by the response to my suggestion.
> 
> Why? I did not reject the idea, but only put it into the context of
> Isabelle. MetiTarski is a small research experiment, but Isabelle a huge
> and complex software product, with very high standards.
> 
> 
>> 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%.
> 
> Where is the empirical measurement for Isabelle? Without that it is just
> speculation.
> 
> A quick test with x86_64 and int = FixedInt might actually give some
> ideas about the order of potential performance improvement. Do you want
> to make one?
> 
> 
> In the Jenkins project, there were also proposals to move to 64bit by
> default, and thus lose a lot of performance. (The general waste of
> resources of Jenkins is caused by high-level policies, though, and
> theses were not openly discussed so far.)
> 
> 
>> 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.
> 
> I routinely check these things before each release. Catch-all patterns
> are more frequent than that, but they are OK.
> 
> I don't think that such a change would cause wrong results, but just
> unexpected failure, and that is already bad enough in everyday use.
> 
> 
>> No exception handlers had to be added when I converted MetiTarski
>> to use fixed integers. An uncaught exception doesn’t prove anything, of
>> course.
> 
> BTW, you have a lot of catch-all exception handlers in MetiTarski. The
> Isabelle/ML IDE shows that -- my changeset from last summer is attached
> again.
> 
> 
> 	Makarius
> 
> <ch-PIDE.txt>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/7c564f2c/attachment-0002.html>