Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 12 Jul 1995 21:51:34 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA084050172; Wed, 12 Jul 1995 11:29:32 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from electra.cc.umanitoba.ca by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA084020169; Wed, 12 Jul 1995 11:29:29 -0600 Received: from eeserv.ee.umanitoba.ca (eeserv.ee.umanitoba.ca [130.179.8.1]) by electra.cc.umanitoba.ca (8.6.12/8.6.9) with ESMTP id MAA20838 for ; Wed, 12 Jul 1995 12:30:38 -0500 Received: from wine by eeserv.ee.umanitoba.ca (SMI-8.6/SMI-SVR4) id MAA00754; Wed, 12 Jul 1995 12:30:10 -0500 From: rahard@ee.umanitoba.ca (Budi Rahardjo) Received: by wine (5.x/25-eef) id AA22212; Wed, 12 Jul 1995 12:28:20 -0500 Message-Id: <9507121728.AA22212@wine> Subject: Future of HOL To: info-hol@leopard.cs.byu.edu Date: Wed, 12 Jul 1995 12:28:19 -0500 (CDT) X-Mailer: ELM [version 2.4 PL24] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Phil Windley: ... > HOL is just to hard for the non-expert to use and its time we did > something about it. If we don't, the world is going to be using PVS or > something else like it. Maybe we don't care...but I, for one, happen to > think that the HOL architecture has some very nice features that I wouldn't > want to give up. YES! Being a non-expert, the simpler HOL is the better. How do I learn practical HOL techniques and tricks? For example, I'd like to know how you guys interact with HOL. With emacs? screen? or windowing? others? How do I manage HOL sessions? How do I stop a session (e.g. too tired) and resume the next day/week? Is there a better HOL "shell" (e.g. use C-p to execute previous command)? e GRIND_TAC;; ? Would these issues be considered in HOL-2000? About PVS, I am tempted to use PVS. In fact, I just downloaded PVS documentations. I really want to stay with HOL, though. Thanks for listening to my rambling... -- budi -- Budi Rahardjo Electrical and Computer Engineering - University of Manitoba - Canada