gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: HOL88 and GCL


From: Camm Maguire
Subject: [Gcl-devel] Re: HOL88 and GCL
Date: 18 Oct 2006 13:27:31 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

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 <address@hidden> 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                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah




reply via email to

[Prev in Thread] Current Thread [Next in Thread]