[Top][All Lists]

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

Re: [Gcl-devel] hash

From: Matt Kaufmann
Subject: Re: [Gcl-devel] hash
Date: Mon, 11 Nov 2013 15:02:21 -0600

Hi, Camm --

Yes, I've reproduced this using a fresh ACL2(h) built on your new
/p/bin/gcl-2.6.10pre -- thanks!!  This is really great.  Case closed!

-- Matt
   From: Camm Maguire <address@hidden>
   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]