Greetings! OK here is my patch against the hol88 sources:
diff -ruN hol.ori/Makefile hol/Makefile
--- hol.ori/Makefile 1994-02-24 07:33:42.000000000 -0500
+++ hol/Makefile 2006-10-18 09:00:26.000000000 -0400
@@ -150,7 +150,7 @@
LispType=cl
Obj=o
-Lisp=akcl
+Lisp=gcl
Liszt=
LisztComm=
Allegro=(set-case-mode :case-insensitive-upper)
@@ -159,7 +159,7 @@
AllegroV4.1= $(AllegroV4.0) (setq *enable-package-locked-errors* nil)
AllegroStuff= (progn () $(AllegroV4.1))
-HOLdir=/usr/local/hol
+HOLdir=/fix/t1/camm/debian/gcl/hol88/hol
Theory=$(HOLdir)/theories
Library=$(HOLdir)/Library
Help=$(HOLdir)/help/ENTRIES/
@@ -244,7 +244,6 @@
'set_search_path[``; `~/`; `${Theory}/`];;'\
'set_help_search_path (words `$(Help)`);;'\
'set_library_search_path [`${Library}/`];;'\
- 'lisp `(load "lisp/akcl.l")`;;'\
'lisp `(setup)`;;'\
'save `${ExeName}`;;'\
'set_thm_count 0;;'\
--- hol.ori/lisp/f-cl.l 1992-10-27 12:38:59.000000000 -0500
+++ hol/lisp/f-cl.l 2006-10-18 10:58:59.000000000 -0400
@@ -569,10 +569,19 @@
(setq *standard-input* (pop inputstack))
(close current-input)))
+(defconstant +fast-digits+ 4)
+(defconstant +slow-digits+ (- (truncate (log most-positive-fixnum 10) 1.0)
+fast-digits+))
+(defconstant +fast-mod+ (expt 10 +fast-digits+))
+(defconstant +slow-mod+ (expt 10 +slow-digits+))
+
(defun clock ()
;; Get absolute time - just for time-stamps
- (get-universal-time))
+ (let ((s (get-universal-time))
+ (m (si::gettimeofday)))
+ (+ (* +fast-mod+ (mod s +slow-mod+))
+ (mod (truncate (* +fast-mod+ m) 1.0) +fast-mod+))))
+; (get-universal-time))
;;; Add extension .o to a file name for output name in process of
diff -ruN hol.ori/lisp/f-format.l hol/lisp/f-format.l
--- hol.ori/lisp/f-format.l 1991-09-28 12:00:55.000000000 -0400
+++ hol/lisp/f-format.l 2006-09-26 15:44:09.000000000 -0400
@@ -131,8 +131,8 @@
(defun flush-output-buffer nil
;; Some data types (e.g. streams) cannot be catenated in franz, so
;; print out items in buffer separately.
- #+franz (mapc #'llprinc (nreverse %output-buffer))
- #-franz (llprinc (apply #'catenate (nreverse %output-buffer)))
+ #+(or franz gcl) (mapc #'llprinc (nreverse %output-buffer))
+ #-(or franz gcl) (llprinc (apply #'catenate (nreverse %output-buffer)))
(setq %output-buffer nil))
diff -ruN hol.ori/lisp/f-iox-stand.l hol/lisp/f-iox-stand.l
--- hol.ori/lisp/f-iox-stand.l 1993-03-22 06:38:50.000000000 -0500
+++ hol/lisp/f-iox-stand.l 2006-10-18 11:28:36.000000000 -0400
@@ -283,7 +283,7 @@
(defun find-file1 (dir name exts)
(do
- ((exts exts (cdr exts))
+ ((exts (cons "" exts) (cdr exts))
(file nil))
((null exts) nil)
(setq file (catenate dir name (car exts)))
This now reliably builds on the CLtL1 images of both 2.6.8 and CVS
head, aka 2.7.0.
Working on the package. Will post when done.
Take care,
John R Harrison <[EMAIL PROTECTED]> writes:
> Hi Camm,
>
> | Greetings! OK, think I've got it.
> |
> | The code assumes that (clock) is strictly increasing, which, as it is
> | a simple call to (get-universal-time), is not reliably true on today's
> | fast hardware. I'm putting in a si::gettimofday function for
> | microsecond resolution, and this seems to be working. More later.
>
> Excellent! That does sound a plausible candidate. If this is indeed
> the problem, it will be really great to have it fixed.
>
> | BTW, how does one escape to lisp from the hol ml prompt?
>
> You can call the ML function
>
> lisp "something";;
>
> which passes "something" direct to the Lisp interpreter. Is that all
> you need? I'm not sure offhand how to globally break into the Lisp
> read-eval-print loop, but there no doubt is a way...
>
> John.
>
>
--
Camm Maguire [EMAIL PROTECTED]
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
_______________________________________________
Gcl-devel mailing list
Gcl-devel@gnu.org
http://lists.gnu.org/mailman/listinfo/gcl-devel
