Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <21196-0@swan.cl.cam.ac.uk>; Wed, 8 Jul 1992 15:09:16 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05187; Wed, 8 Jul 92 06:54:44 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA05182; Wed, 8 Jul 92 06:54:37 -0700 Received: by infix.cs.ruu.nl id AA20967 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Wed, 8 Jul 1992 15:55:37 +0200 From: Wishnu Prasetya Message-Id: <199207081355.AA20967@infix.cs.ruu.nl> Subject: problem with long string? To: info-hol@edu.uidaho.cs.ted (hol mailing list) Date: Wed, 8 Jul 92 15:55:36 METDST X-Mailer: ELM [version 2.3 PL11] Hi there, I tried to mail this before, but I'm not sure if it is broadcasted through the list. I thought not, so let me try again. There seems to be a problem in HOL 1.1, which I hope is fixed in 2.0. I was trying to write derivation rules. As others often do I also use the trap operator `? ` to print some diagnostic messages upon evaluation failure. That is, using ? failwith `xxx whatever xxx` The strange thing is, when I `load` my written file using the `load` function, thing goes smoothly. But when I simply cut the definition and copy it the `hol window` (I'm using emacs as environment), and then try to evaluate it, the program hangs. Later I found out that if I shorten the `xxx whatever xxx` string, the program won't hang and evaluates as intended. So I wonder if this problem is in the HOL itself, or is there perhaps some trouble in the combination HOL-emacs. If you have any comment in this, I would love to hear it. Thank you, -Wishnu Prasetya- CS Dept. University of Utrecht. --