Now I got it...
This "Which SML compiler is best? question is giving me a lot of headache lately!". I'm doing my master thesis on a sort of Isabelle plugin for automated theorem proving. In the beginning I didn't know SML so I though, "Well, I know scheme, I'll do it in scheme and I use some FFI and inverse FFI that usually comes with compilers"... at least I knew scheme was able to do it. After some discussion in #sml @ freenode and some personal research I found that it would take a 'temporary thesis' (as some named it) to create bindings between scheme and sml so I got ML for the Working Programmer and started reading it. Soon I found that SMLNJ was not able to do fact 35, without overflowing, like you did in the book and I asked yesterday at #sml @ freenode which compiler would be able to do that (maybe a compiler with infinite precision, which I initially thought it would be a ML standard requirement). Now, I get it... You used PolyML. :D This makes me a bit 'sad' since I've read some times (not only in the Isabelle Mailing List but also on the web) that PolyML would be better to run Isabelle (since it makes Isabelle a lot of faster) but I thought (and now I'm almost sure) that I shouldn't develop my 'isabelle plugin' (let's call it this way, however you can interpret it as a tactic, if you want, since it is inspired in blast_tac) in PolyML since it seems completely dead and the documentation seems pre-historic. So, it seems to me this is somehow a difficult choice, should I choose between developing on a dead compiler or on a slow compiler (regarding Isabelle)?
Cheers,
Paulo Matos
On Tue, 2004-03-16 at 09:37, Lawrence Paulson wrote:
On 16 Mar 2004, at 04:24, Ian Zimmerman wrote:
The one problem is that its Basis library is getting quite out of date, because the standard keeps changing in that respect.
Does anybody know what is really going on with the Basis Library?
When the 2nd edition of my ML book appeared (in 1996!) I had the problem of attempting to track the changes to the Library. I was promised that there would be a feature freeze very soon, but it never happened. Even after the book went to press, major changes were made that affected the text. Some of these, such as removing the equality operator on type real, struck me as being ill-advised.
I can't believe they are still tinkering with it eight years later.
Larry Paulson
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml