[isabelle-dev] Integers in Poly/ML

[Lawrence Paulson]

Just as remark: MetiTarski took a slight performance hit in the transition to the new compiler, happily greatly reversed by my decision to use fixed-precision integers.

Of course I would like to use the IDE for Standard ML, but getting started is always more complicated than it looks.

Larry

> On 2 Nov 2016, at 22:22, Makarius <makarius at sketis.net> wrote:
> 
> 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.

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