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.


> On 2 Nov 2016, at 22:22, Makarius <makar...@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.

isabelle-dev mailing list

Reply via email to