Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: building HOL using Ibuki.
Date: Fri, 24 Jan 92 11:32:41 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.075:24.00.92.11.32.49"@cl.cam.ac.uk>


Further to my recent posting about building HOL using Ibuki
common lisp, attached is a relevant message from John Carroll.

Can anyone out there confirm that these changes work?

Tom
============================================================================
J CARROLL's MESSAGE OF 24 JAN:

Tom,

I saw your message in info-hol:

>> I have successfully built HOL using Ibuki.  It requires some minor
>> changes to the lisp sources, which I will post soon.
>
>Attached is a record of diffs I needed to build HOL with IBUKI. Basically,
>you must:
>
>  1: add "ibcl" to the conditional compilation statements wherever
>     "kcl" appears.  For example, #+kcl in f-cl.l becomes #+(or kcl ibcl).
>
>  2: change the line in f-freadth.l as indicated below.  I think this
>     was the source of the error posted by Ashish.
>
>Tom

I think I have better solutions to your 1. and 2.

1. There is already a piece of code in f-cl.l that is supposed to make
the ibcl compilation behave in the same way as kcl:

;;; IBCL uses the same settings as KCL, so add kcl to feature list
;;; (PJW 09.01.90)
#+ibcl (setq *features* (push :kcl *features*))

This is obviously no longer working. However I think the following will:

;;; IBCL uses the same settings as KCL, so add kcl to feature list
;;; (PJW 09.01.90)
#+ibcl (eval-when (compile load eval) (setq *features* (push :kcl *features*)))

This avoids the need to add ibcl to every #+/- that mentions kcl.


2. It's not a good idea to just take out that '#, in f-freadth.l,
since without it a string of length 256 will get allocated every single
time an atom is encounted when a theory file is read. The intention is
that the string should be static. Here is a better solution that does
not involve '#,:

(defvar *fast-read-atom-buffer* (make-string 256))

(defun fast-read-atom (stream char)
   (declare (optimize (speed 3) (safety 0)))
   (let
      ((buffer *fast-read-atom-buffer*)
       (index 0)
...

Are you able to try out these solutions in an ibcl implementation and
check that they indeed work?

John