01:53:53 Vivitron [~Vivitron@c-50-172-44-193.hsd1.il.comcast.net] has joined #ccl 03:18:47 -!- ubii [~ubii@unaffiliated/ubii] has quit [Read error: Connection reset by peer] 03:19:15 ubii [~ubii@unaffiliated/ubii] has joined #ccl 03:44:38 -!- alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_] 04:10:15 -!- Vivitron [~Vivitron@c-50-172-44-193.hsd1.il.comcast.net] has quit [Ping timeout: 240 seconds] 04:38:43 -!- rme [rme@3363A27E.B0A14555.699BA7A6.IP] has quit [Quit: rme] 04:38:43 -!- rme [~rme@50.43.163.42] has quit [Quit: rme] 05:22:08 ubii_ [~ubii@198.45.198.1] has joined #ccl 05:23:35 ubii__ [~ubii@198.45.198.1] has joined #ccl 05:24:59 -!- ubii [~ubii@unaffiliated/ubii] has quit [Ping timeout: 240 seconds] 05:26:58 -!- ubii_ [~ubii@198.45.198.1] has quit [Ping timeout: 240 seconds] 05:47:42 Vivitron [~Vivitron@c-50-172-44-193.hsd1.il.comcast.net] has joined #ccl 06:03:51 -!- Vivitron [~Vivitron@c-50-172-44-193.hsd1.il.comcast.net] has quit [Remote host closed the connection] 07:49:37 -!- ubii__ [~ubii@198.45.198.1] has quit [Quit: Leaving] 11:26:42 -!- aftershave [~textual@h-238-41.a336.priv.bahnhof.se] has quit [Quit: Textual IRC Client: www.textualapp.com] 11:27:39 aftershave [~textual@h-238-41.a336.priv.bahnhof.se] has joined #ccl 12:05:37 pnpuff [~harmonic@unaffiliated/pnpuff] has joined #ccl 13:11:41 aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has joined #ccl 13:15:18 -!- aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has quit [Client Quit] 13:21:13 -!- asedeno [~asedeno@66.102.14.24] has quit [Ping timeout: 272 seconds] 13:25:08 dnm [~user@184-77-202-69.war.clearwire-wmx.net] has joined #ccl 13:46:20 -!- pnpuff [~harmonic@unaffiliated/pnpuff] has quit [] 14:28:09 STilda [~kvirc@188.162.166.23] has joined #ccl 14:45:51 segv- [~mb@cpeB-151.mvcable.net] has joined #ccl 14:55:32 alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 14:58:38 -!- alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Client Quit] 14:59:52 aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has joined #ccl 15:04:11 pnpuff [~harmonic@unaffiliated/pnpuff] has joined #ccl 15:28:09 alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 15:32:42 -!- aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has quit [Quit: Computer has gone to sleep.] 15:45:51 rme [~rme@50.43.163.42] has joined #ccl 17:05:38 aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has joined #ccl 17:34:19 -!- aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has quit [Quit: Computer has gone to sleep.] 17:52:10 -!- pnpuff [~harmonic@unaffiliated/pnpuff] has quit [] 18:20:04 aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has joined #ccl 18:35:03 -!- aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has quit [Quit: Computer has gone to sleep.] 19:02:49 milanj [~milanj@109-92-127-249.dynamic.isp.telekom.rs] has joined #ccl 19:03:55 -!- milanj [~milanj@109-92-127-249.dynamic.isp.telekom.rs] has quit [Client Quit] 19:24:15 -!- alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_] 19:34:05 alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 19:40:53 -!- alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_] 19:53:41 -!- STilda [~kvirc@188.162.166.23] has quit [Ping timeout: 252 seconds] 20:10:47 -!- dnm [~user@184-77-202-69.war.clearwire-wmx.net] has quit [] 20:34:03 is there a way to explicitly resize a package in ccl? 20:34:28 alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 20:39:10 I'm not sure why you're wondering, but there's the internal-use-only ccl::%resize-package. 20:39:35 I'm not sure it's even safe to call, actually. 20:39:56 it seems like packages grow very slowly and it seems to get expensive once there are more than a few million symbols there 20:40:07 (which admittedly we probably shoudn't be doing, but, you know...) 20:42:34 aha, it looks like make-package maybe also can be given :internal-size and :external-size options... i can probably use that 20:42:45 make-package takes :internal-size ... what you said 20:48:47 For sizes larger than about 32000, it looks like we screw around a lot trying to find a value for size that is relatively prime to a number of factors. For millions of values, I could imagine that this takes a while. (see %initialize-htab) 20:52:46 interesting -- i had just assumed it was due to not adding very many elements at a time; it looks like %resize-htab is growing the table by about 1.25x, which might be on the small side, or maybe is okay 20:53:16 i guess i should make a test and try timing these 20:53:18 Vivitron [~Vivitron@c-50-172-44-193.hsd1.il.comcast.net] has joined #ccl 21:41:19 it looks like the relatively-prime stuff takes very little time, here's an analysis... 21:42:17 http://pastebin.com/BxpH0y8w 21:44:17 Would it be OK if copy that paste into a Trac ticket? 21:44:27 yes definitely 21:44:28 If I copy it, that is. 21:44:29 OK. 21:50:47 Thanks for the report. The ticket is http://trac.clozure.com/ccl/ticket/1136 21:50:54 dnm [~user@67-131-0-251.dia.static.qwest.net] has joined #ccl 22:01:26 What a coincidence. I'd just made a resolution to care about what happens when someone interns a million symbols, and here's my chance! 22:04:22 i fear you may be mocking me :( 22:07:15 the final tally was 53 minutes, fwiw 22:09:45 It's a bad sign when people can't tell if they're being mocked ... when I was younger, people were SURE. Oh well. 22:11:07 -!- alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_] 22:11:54 alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 22:15:12 well, i'm pretty sure i deserve to be mocked 22:15:36 alas, sometimes using ACL2 drives you to do things that would be stupid for real Lisp programmers 22:15:51 -!- mdc_mobile [mdc@clozure-19689DF6.hsd1.ca.comcast.net] has quit [Ping timeout] 22:17:33 -!- mdc_mobile [~mdc_mobil@c-98-248-35-30.hsd1.ca.comcast.net] has quit [Ping timeout: 272 seconds] 22:29:43 aftersha_ [~textual@h-238-41.a336.priv.bahnhof.se] has joined #ccl 22:35:17 clop2: Heh. 22:35:52 Perhaps when the working set is limited to 4 billion bytes, one million symbol packages sound ridiculous. 22:36:19 But not anymore when you've got 64-bit address spaces. 22:36:59 it's just one package 22:37:18 clop2: What are you using ACL2 on? 22:37:39 my company uses it for hardware verification 22:37:48 mdc_mobile [~mdc_mobil@c-98-248-35-30.hsd1.ca.comcast.net] has joined #ccl 22:37:53 In any case, I wouldn't expect packages to be worse than hashtable. So if you want to suggest using hashtables as an alternative, wrong. 22:43:29 clop2: Neat. Can you say what kind of hardware you're verifying? 22:43:48 yeah, i work at centaur technology, we develop an x86 processor 22:44:29 we have some papers about it, e.g., just google "centaur technology formal verification" or similar 22:45:19 Oh hey, the WinChip people. 22:45:26 clop2: Will do. Thanks! 22:46:07 sure thing -- thanks for your help guys, /me heads home 22:46:09 Damn you Springer! http://link.springer.com/chapter/10.1007%2F978-1-4419-1539-9_3 22:46:23 clop2: I was curious and tried (time (dotimes (i 1000000) (intern (format nil ... in another implementation. Thats been running for about 45 minutes so far 22:47:09 gbyers, it came to about 53 minutes on my computer, but it's not a very fast box 22:47:17 on ccl, i mean 22:47:30 but sbcl finished it in about 5 seconds 22:47:58 i have to run, can chat tomorrow more 22:48:02 I'm using SBCL, so there's something funny here. 22:48:26 ah, hrmn, i'm using 1.0.46 on linux-x86-64 22:48:30 which is probably pretty old now 22:48:58 i used the code from the bottom of that paste 22:49:26 "This is SBCL 1.1.1.0.debian" on a fairly fast Core i7 laptop. 22:49:36 -!- alms_ [~alms_@209-6-153-34.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_]