[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)
(u)
(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
- [Gcl-devel] hash,
Camm Maguire <=