Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from cs.uidaho.edu (actually ted.cs.uidaho.edu !OR! info-hol-request@cs.uidaho.edu) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Wed, 14 Jul 1993 16:50:06 +0100
Received: by cs.uidaho.edu (16.6/2.0) id AA04060; Wed, 14 Jul 93 08:42:57 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from dbms1.cs.byu.edu by cs.uidaho.edu (16.6/2.0) id AA04055;
          Wed, 14 Jul 93 08:42:52 -0700
Received: by dbms1.cs.byu.edu (5.57/Ultrix3.0-C) id AA24202;
          Wed, 14 Jul 93 09:44:30 -0600
Message-Id: <9307141544.AA24202@dbms1.cs.byu.edu>
To: markaa@ultrastar.ee.cornell.edu (Mark D. Aagaard)
Cc: info-hol@cs.uidaho.edu
Subject: Re: kgs of proofs??
In-Reply-To: Your message of Wed, 14 Jul 93 10:42:04 -0400. <9307141442.AA10979@ultrastar.EE.CORNELL.EDU>
Date: Wed, 14 Jul 93 09:44:29 -0600
From: Phil Windley <windley@dbms1.cs.byu.edu>
X-Mts: smtp



On Wed, 14 Jul 93 10:42:04 EDT, markaa@ultrastar.ee.cornell.edu wrote:
+------------
| Does anyone have any statistics, estimates,
| or guesses on the lines of code, number of 
| proofs, kg of specification, etc produced
| in/for/by HOL? I realize that this is a 
| difficult thing to quantify, but any useful
| information along these lines would be helpful.

I was thinking it would be fun if HOL kept a running tally of the number of
primitive inference made (in a file somewhere) that could be consulted to
see how many inferences had been made by a particular executable.

I was going to get a scoreboard for the lab and have contests.

--phil--