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 <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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to