00:46:43 alms_ [~alms_@209-6-130-32.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 02:33:50 -!- alms_ [~alms_@209-6-130-32.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_] 04:35:28 -!- PECCU [~peccu@ZU204236.ppp.dion.ne.jp] has quit [Ping timeout: 255 seconds] 04:50:42 PECCU [~peccu@ZL198047.ppp.dion.ne.jp] has joined #ccl 06:23:38 -!- clop [~jared@moat3.centtech.com] has quit [*.net *.split] 07:32:05 jdz [~jdz@193.206.22.97] has joined #ccl 07:57:35 clop [~jared@moat3.centtech.com] has joined #ccl 13:47:50 -!- sellout [~Adium@c-98-245-92-119.hsd1.co.comcast.net] has quit [Quit: Leaving.] 13:48:54 alms_ [~alms_@209-6-130-32.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has joined #ccl 14:50:12 milanj [~milanj_@212-200-192-196.dynamic.isp.telekom.rs] has joined #ccl 15:05:54 rme: Congrats! And thanks! 15:09:38 I hope 1.8 works well for you. 15:23:14 -!- jdz [~jdz@193.206.22.97] has quit [Ping timeout: 272 seconds] 15:33:32 -!- billstclair [~billstcla@unaffiliated/billstclair] has quit [Quit: Linkinus - http://linkinus.com] 15:34:14 billstclair [~billstcla@68.237.143.59] has joined #ccl 15:34:14 -!- billstclair [~billstcla@68.237.143.59] has quit [Changing host] 15:34:14 billstclair [~billstcla@unaffiliated/billstclair] has joined #ccl 16:07:50 rme: Likely the first thing I'll do is build a new ACL2. 16:09:31 ACL2 is built and run as part of CCL's automated testing, so I would expect it work with no problems. 16:11:17 Excellent. 17:43:18 rme: Out of curiosity, do you (or does anyone else here) know if anyone has tried to compile a recent PVS version out-of-the-box with CCL? 17:45:13 Not me, sorry. 17:46:47 No worries. It looks like, from the PVS site, they've still got a fairly heavily conditionalized pile of code. Will probably take some significant work to "port" to CCL. 17:47:01 Though it seems like current versions at least work under both ACL and SBCL now... 17:48:17 Either that, or it's vanilla Common Lisp and they've never bothered to try it on any other implementation. 18:43:46 rme_ [~rme@50.43.130.38] has joined #ccl 18:44:29 -!- rme [~rme@50.43.154.23] has quit [Ping timeout: 246 seconds] 18:44:30 -!- rme_ is now known as rme 18:44:50 -!- rme [rme@F9E6AB97.ED8853D8.699BA7A6.IP] has quit [Ping timeout] 19:09:52 rme_ [~rme@50.43.139.115] has joined #ccl 19:10:35 -!- rme [rme@833EE115.6C775BE1.699BA7A6.IP] has quit [Ping timeout] 19:10:36 -!- rme_ is now known as rme 19:12:37 -!- rme [~rme@50.43.130.38] has quit [Ping timeout: 276 seconds] 19:14:25 -!- rme_ is now known as rme 19:15:33 rme [~rme@50.43.130.54] has joined #ccl 19:15:59 -!- rme_ [~rme@50.43.139.115] has quit [Ping timeout: 246 seconds] 19:42:29 sellout [~Adium@c-98-245-92-119.hsd1.co.comcast.net] has joined #ccl 21:05:43 -!- alms_ [~alms_@209-6-130-32.c3-0.bkl-ubr1.sbo-bkl.ma.cable.rcn.com] has quit [Quit: alms_] 22:05:00 -!- rme [rme@2C929693.6C775BE1.699BA7A6.IP] has quit [Ping timeout] 22:05:20 rme_ [~rme@50.43.140.184] has joined #ccl 22:07:24 -!- rme [~rme@50.43.130.54] has quit [Ping timeout: 244 seconds] 22:07:24 -!- rme_ is now known as rme 22:28:41 rme_ [~rme@50.43.151.218] has joined #ccl 22:29:13 -!- rme [~rme@50.43.140.184] has quit [Ping timeout: 245 seconds] 22:29:13 -!- rme_ is now known as rme 22:29:42 -!- rme [rme@AFF44FA.2D6491A5.699BA7A6.IP] has quit [Ping timeout] 22:37:41 -!- milanj [~milanj_@212-200-192-196.dynamic.isp.telekom.rs] has quit [Quit: Leaving] 22:49:41 rme_ [~rme@50.43.143.55] has joined #ccl 22:49:49 -!- rme [rme@7E7ECE82.A884877E.699BA7A6.IP] has quit [Ping timeout] 22:49:50 -!- rme_ is now known as rme 22:50:53 -!- rme [~rme@50.43.151.218] has quit [Ping timeout: 246 seconds] 22:50:54 -!- rme_ is now known as rme 22:52:22 -!- rme [rme@119BF9DF.DEB6CE53.699BA7A6.IP] has quit [Quit: rme] 22:52:22 -!- rme [~rme@50.43.143.55] has quit [Client Quit] 23:47:15 rme [~rme@50.43.157.220] has joined #ccl