Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 1 Nov 1994 15:23:25 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA22258;
          Tue, 1 Nov 1994 08:17:46 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA22254;
          Tue, 1 Nov 1994 08:17:46 -0700
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA02101;
          Tue, 1 Nov 1994 08:14:11 -0700
Message-Id: <9411011514.AA02101@jaguar.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: bhogan@bedlam: HOL90 on a PC
Date: Tue, 01 Nov 1994 08:14:11 -0700
From: Phil Windley <windley@lal.cs.byu.edu>


I received the following report of using HOL90 on a PC (under linux).  I
pass it on to the list for those who might be interested in this option.

------- Forwarded Message

To: windley@leopard.cs.byu.edu
In-Reply-To: <9410271522.AA02643@jaguar.cs.byu.edu> (windley@lal.cs.byu.edu)
Subject: Re: FPL for proving theorems?
Reply-To: bhogan@rahul.net (Bill Hogan)

"PW" == Phil Windley <windley@lal.cs.byu.edu> writes:

  PW> On Thu, 27 Oct 94 08:15 PDT bhogan@bedlam writes
  PW> +--------------------
  PW> | Of course, now I can't wait to see if I can get HOL running on my PC.
  PW> | 

  PW> Your best bet is to get SML (Standard ML) running on your PC and then use
  PW> HOL90.  I know folks who have done it on Macs, don't know about PCs.

  PW> There is a mailing list, info-hol@lal.cs.byu.edu, that connects HOL users
  PW> from all over the world.  Someone on that list could help you.  Let me know
  PW> if you want on the list (I'm the maintainer) and then you could ask your
  PW> questions there.
  PW> --phil-

  Hello Phil,

    Just want to let you know that hol90.6 compiled "right out of the
box" on my -486dx Linux system using njsml-93 (from Stoney Brook).

   And, yes, I would like to be included in the HOL mailing-list.

   I am unlikely to have much of anything to contribute very soon but
I am a pretty good "lurker". :)
   
   Best regards,
    Bill

p.s. I don't have anything to compare it to, but just in case it might
be useful to you, here is a snippet from the benchmark output:

          HHH                 LL
          HHH                  LL
          HHH                   LL
          HHH                    LL
          HHH          OOOO       LL
          HHHHHHH     OO  OO       LL
          HHHHHHH     OO  OO       LLL
          HHH          OOOO        LLLL
          HHH                     LL  LL
          HHH                    LL    LL
          HHH                   LL      LL
          HHH                  LL        LL90.6

Created on Fri Oct 28 09:19:47 PDT 1994
using: Standard ML of New Jersey, Version 0.93, February 15, 1993

 [...]

 val MULT_CORRECTNESS =
  |- MULT_IMP (i1,i2,o1,o2,done) /\
     NEXT (x,x + d) done /\
     STABLE (x,x + d) (\x'. i1 x',i2 x') /\
     done x ==>
     (o2 (x + d) = i1 x * i2 x) : thm

Theory "MULT_VER" exported.
val it = () : unit
val it = () : unit
val it = "runtime: 150.710000s, gctime: 7.920000s." : string
- -

   
   
   



------- End of Forwarded Message