Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 25 Jun 1993 14:43:39 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10748; Fri, 25 Jun 93 06:33:41 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from concorde.inria.fr by ted.cs.uidaho.edu (16.6/1.34) id AA10743; Fri, 25 Jun 93 06:33:34 -0700 Received: from margaux.inria.fr by concorde.inria.fr; Fri, 25 Jun 1993 15:33:45 +0200 Original-Received: from localhost.inria.fr by margaux.inria.fr, Fri, 25 Jun 93 15:38:27 +0200 PP-warning: Illegal Received field on preceding line To: Lawrence C Paulson Cc: info-hol@ted.cs.uidaho.edu, murthy@margaux.inria.fr Subject: Re: Poly/ML vs SML/NJ In-Reply-To: Your message of Fri, 25 Jun 93 11:39:35 +0100. <"swan.cl.cam.:173120:930625103943"@cl.cam.ac.uk> Return-Receipt-To: Chet.Murthy@inria.fr Date: Fri, 25 Jun 93 15:38:25 N Message-Id: <14257.741015505@margaux.inria.fr> From: Chet.Murthy@inria.fr >>>>> On Fri, 25 Jun 93 11:39:35 +0100, Lawrence C Paulson said: LCP> However, an Isabelle rebuild (which takes several hours on a LCP> Sun-4 and consists almost entirely of theorem-proving) is LCP> slightly faster with Poly/ML. Has it actually been verified with profiling that this is the case? I know that for my own example, the time spent in Nuprl tactic invocation was vastly dwarfed by the time required to parse and type-check the tactic invocation phrases. Meaning, does Isabelle have its own parser for user input? If not, then how can one tell that the major part of the time is spent in theorem-proving? Or, could one take the entire Isabelle build-file, and put it in a functor - compile the functor, and then invoke it, to cause the build. Then, you would see exactly how much was compilation/parsing/type-checking, and how much was theorem-proving. --chet--