Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: info-hol@ted.cs.uidaho.edu
Subject: Poly/ML vs SML/NJ
Date: Fri, 25 Jun 93 11:39:35 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:173120:930625103943"@cl.cam.ac.uk>


I can confirm Mike Fourman's remarks, and have no vested interest in Poly/ML
except that I shared an office with its developer (Dave Matthews) about 8
years ago.

The sorting examples in "ML for the Working Programmer" do indeed run about 3
times faster on SML of NJ than they do under Poly/ML, perhaps because they
involve real numbers.  

However, an Isabelle rebuild (which takes several hours on a Sun-4 and
consists almost entirely of theorem-proving) is slightly faster with Poly/ML. 
This holds consistently on my two machines, a SPARC ELC with 40Mb and a SPARC
SS-10 with 112Mb.  The former machine (not a small memory one in my opinion)
struggles to run even a single Isabelle-HOL compiled under SML of NJ, while it
happily supports a couple of Isabelle users compiled under Poly/ML.  Not only
does the NJ compiler require a large address space, but memory locality is
poor -- it seems to want it all at once before even printing a prompt.  To
base a large project on this compiler risks spending more on equipment than
would be saved in the licence fee.

I am posting this message to help people avoid getting into difficulties.  I
am certainly not trying to put down the New Jersey compiler, which is freely
available to all and is a great service to the ML community.  

							Larry Paulson