[isabelle-dev] Integers in Poly/ML

[Makarius]

On 02/11/16 17:30, Lawrence Paulson wrote:
> 
> 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

I've been working with David Matthews for some weeks to see the new
compiler and related run-time system changes work with Isabelle, and
perform well. Right now the situation is that all of the Isabelle
repository compiles, and AFP almost works (I have tested it for the
first time only a few days ago).

At the same time, we have taken some looks at performance: in the very
first round, the new approach was much slower, now it is a bit faster --
thanks to some improvements in string comparison. More systematic
performance tests will come later.

Nothing of this is fundamentally new: Poly/ML has changed many times
before, and Isabelle was changed to follow-up and improve the overall
situation: towards more clarity, more correctness, more performance.


> 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.

The short int has only 31 bits and there is also a sign bit. It means
there are only approx. 10E9 different values, lets say for some uniquely
generated identifier or index into some data structure.

As an array index that is only 1GB, afterwards overflow happens. In
Java, this has led to some surprises some years ago (IIRC in array
sorting algorithms). Although nobody should be surprised, when small
finite values do eventually overflow.

For us there would be spurious exceptions, instead of silent overflow. I
need to correct an earlier statement of mine: overflow *can* be a
problem, e.g. in the frequently used "try" and "can" combinators. Only
interrupt exceptions are carefully separated from the mathematical
meaning of Isabelle/ML, not overflows or other soft errors.


> whereas I recall we keep our own copy of the compiler packaged in
> a special way somewhere

I was talking a tiny little bit about this at the Isabelle workshop in
Nancy. There are several stages of Isabelle/ML compiler bootstrap, also
the separation of a physical and a virtual version of the ML
environment. That is definitely interesting to look at, but not so easy
to understand.

To get a feel for it, I recommend to start as a user of the IDE for
Isabelle/ML or Standard ML.


	Makarius