Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-5.6) id <09813-0@swan.cl.cam.ac.uk>; Mon, 2 Dec 1991 17:56:16 +0000 Received: by ted.cs.uidaho.edu (15.11/1.34) id AA08408; Mon, 2 Dec 91 09:41:30 pst Reply-To: info-hol@ted Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from [128.232.0.56] by ted.cs.uidaho.edu (15.11/1.34) id AA08398; Mon, 2 Dec 91 09:41:16 pst Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-5.6) to cl id <09579-0@swan.cl.cam.ac.uk>; Mon, 2 Dec 1991 17:41:18 +0000 To: info-hol@edu.uidaho.cs.ted Subject: HOL versions: a measure Date: Mon, 02 Dec 91 17:41:15 +0000 From: btg@uk.ac.cam.cl Message-Id: <"swan.cl.ca.583:02.11.91.17.41.25"@cl.cam.ac.uk> There has been a considerable number of changes to the basic HOL system in the past year. We have gone through versions: v1.11, v1.12, v1.13, and finally v2.0. The significant changes from a (naive) user's point of view include the changes to resolution, improvements to rewriting, and most recently a sound reimplementation of the "unwind" library. I first completed a (partial) proof of correctness of the SECD microprocessor using version 1.11, and have recently updated the proof to run under version 2.0. Since it is substantial in size, it gives an interesting measure of the impact of these changes. The following numbers summarize the system's measure of "Intermediate theorems generated", which is a count of the number of primitive inferences performed by system. HOL v1.11 HOL v2.0 =============================================== types sum is 99469 51161 defs sum is 257048 85863 expands sum is 446585 168003 phase sum is 4901115 1079274 mu-prog sum is 1145063 431135 liveness sum is 933 874 correctness sum is 1304044 667760 =============================================== total is 8154257 2484070 ======================================================== elapsed time: no figure avail. 27 hours 6 minutes. ======================================================== The proof was run on a 16 meg Sparc, using HOL built on Allegro Common Lisp. A brief explanation of the categories: types - type definitions, including some axiomatization of the types defs - component, specification, constraint, and abstraction function definitions and some basic theorems about the definitions. expands, phase, mu-prog, liveness, and correctness - 5 stages of the proof The measures should not be taken too literally, as there was some reorganization to the proof between versions, expecially in the types and defs categories. Overall however the totals are significantly changed. Improvements to rewriting greatly outweigh the increases due to the revision to resolution and the necessarily less efficient (but sound) unwind library. Very few deliberate improvements to the proof were included aside from adapting to changes in the system. As a final note, the SECD proof will be made available shortly via anonymous ftp. Brian Graham