[Top][All Lists]

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

[Gcl-devel] hash

From: Camm Maguire
Subject: [Gcl-devel] hash
Date: Mon, 11 Nov 2013 12:09:44 -0500

[ may be repeat due to new mail system misconfiguration ]

Greetings!  Believe its fixed now.  New package installed at ut.  

(ubt! 1)
(include-book "portcullis")
(rebuild "solutions.lisp" t)
(time$ (def-gl-thm 1f :hyp (and (unsigned-byte-p 3000 x)(unsigned-byte-p
3000 y)) :concl (equal (+ x y) (+ y x)) :g-bindings (gl::auto-bindings
(:mix (:nat x 3000)  (:nat y 3000)))))


; 76.93 seconds realtime,
; 75.44 seconds runtime, 0.00 seconds child runtime,
; 1.35 seconds systime, 0.00 seconds child systime.

The hash keys were insufficiently random.

I'll do a quick profiling run in the test directory.

Did the chmod you requested.

Please let me know if you see any problems.  I'd like a few days of
problem free happiness before release :-)

Take care,
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]