Tom 7 Radar: all comments

[ next 25 ]

2247. Tom 7 (gs82.sp.cs.cmu.edu) – 16 Mar 2005 17:07:41 NEW: Escape Beta 2! ]
OK. =) Well, I can't claim to be consistent with the way linux folks do stuff!

It would probably make sense to have the source code include a version number, since the source code doesn't update itself (there'd be little point in that!). I was thinking about the binaries.
 
2246. Anonymous (sotn-cache-2.server.ntli.net) – 16 Mar 2005 15:54:27 NEW: Escape Beta 2! ]
"rolling my eyes" was a poor choice of words - damn your non-editable comments section! - but usually linux progs are distributed as tarballs, so "foobar-x.y.z.tar.gz" is considered "normal", i think. Often, fairly shaky or amateurish progs unpack into "foobar-src" or "foobar" or, in some extreme cases, unpack into the current directory instead of creating a subdirectory(!). It can sometimes be handy to have two different-version source trees side-by-side. I know nothing of this self-updating of which you speak, so yeah, there's presumably reasons for doing it the way you do. I'm not really sure how this makes it difficult for distro makers, it might just be a consistency thing.
 
2245. Hock (sleepy.cs.wisc.edu) – 16 Mar 2005 13:30:03 Pi day... awesome! ]
You made metafilter again:
http://www.metafilter.com/mefi/40453
 
2244. jcreed (wittgenstein.wv.cc.cmu.edu) – 16 Mar 2005 12:26:21 Very Big ]
The nanobots are lulling you into a false sense of security. Watch out for the red-green-blue-gray-goo!
 
2243. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 16 Mar 2005 11:00:47 NEW: Escape Beta 2! ]
Hmm. Well, Escape updates itself, so I'm not sure what sense that would make (you'd install in escape-200503150, but later you'd have 200601010 in there). How does this make including a game in a distro easier, or why does it make you roll your eyes to not do it? (Just curious.)
 
2242. Anonymous (sotn-cache-2.server.ntli.net) – 16 Mar 2005 07:35:45 NEW: Escape Beta 2! ]
versioned, i presume, as in "escape-1.0.0.tar.gz" for example, with the top directory being "escape-1.0.0" rather than "escape-src". It seems to be normal practice for linux software. Not wanting to be a snob, but when i see a tarball unpack to "foogame" rather than "foogame-x.y.z" i give a little sigh and roll my eyes. ;)
 
2241. Alice (mail.app.aconex.com) – 15 Mar 2005 23:04:30 Pi day... awesome! ]
Here in Australia, where we write dates as dd/MM, pi approximation day is the 22nd of July.
 
2240. Alice (mail.app.aconex.com) – 15 Mar 2005 22:55:59 Pi day... awesome! ]
Here in Australia, where we write dates as dd/MM, pi approximation day is the 22nd of July.
 
2239. Tom 7 (gs82.sp.cs.cmu.edu) – 15 Mar 2005 13:55:32 HSE: Real Books ]
NOT EVEN LIGHTNING BOLT.
 
2238. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 14 Mar 2005 19:24:26 Pi day... awesome! ]
No indeed. ;)
But maybe it can last until I graduate...
 
2237. Mike Nolan (207.160.210.253) – 14 Mar 2005 16:33:46 Pi day... awesome! ]
I don't guess the doubling pattern can continue indefinitely though, unless the people there are <i>really</i> amazing, though.
 
2236. Tadbot (pcp0010451887pcs.walngs01.pa.comcast.net) – 14 Mar 2005 14:12:17 Pi day... awesome! ]
Dave put a couple pix at http://vaxcave.com/index.php?p=314
 
2235. Tadbot (pcp0010451887pcs.walngs01.pa.comcast.net) – 14 Mar 2005 14:01:55 Pi day... awesome! ]
r0x. A nice Π party. Celebrate it yearly. Smath can visit annually.
Aronofsky, Darren's cinematic Max vs Ant arthouse film - supply it!
Anyway, how's Dan now? Nerdcore job or working 9-5?
 
2234. ndm (c-67-165-67-55.client.comcast.net) – 14 Mar 2005 14:00:00 Pi day... awesome! ]
yeah, where's the pics?
 
2233. FARINA00 (host226-98.pool8536.interbusiness.it) – 14 Mar 2005 13:08:58 Pi day... awesome! ]
PIctures!
 
2232. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 14 Mar 2005 00:30:27 Very Big ]
I think it's "Digital light processing" or something like that. It's a MEMS technology which uses an array of (millions of) miniature mirrors on a chip that can be tilted to different angles in order to reflect different amounts of light. A color wheel sends red, blue, green, and white light alternatingly to bounce off the chip and onto the surface. It's generally better than LCD because it doesn't require three different imaging devices per pixel (so there is greater pixel density for cheaper), and the colors all end up exactly on top of one another, and the pixels can be larger. Anyway, it looks sweet.
 
2231. jcreed (pool-70-17-165-61.pitt.east.verizon.net) – 13 Mar 2005 23:35:19 Very Big ]
What does DLP stand for?
 
2230. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 13 Mar 2005 00:26:18 NEW: Escape Beta 2! ]
I haven't heard of versioned tarballs, and can't find something easily on google that explains it. Any tips, anyone?
 
2229. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 13 Mar 2005 00:23:02 Spring Break! ]
In fact, Twelf does already have constraint domains for integers (and soon, I believe, integers-modulo-2^n), although the coverage checker currently doesn't work on these.
 
2228. ruskie@mages.ath.cx (84.20.228.4) – 12 Mar 2005 16:27:21 NEW: Escape Beta 2! ]
Ever heard of versioned tarballs... try to use them... it's a great help to us who try to provide the game in a distro...
 
2227. Andrew (yale128036074005.student.yale.edu) – 12 Mar 2005 14:19:52 Spring Break! ]
As I said, it depends on what you are doing. For something like assembly, with lots of arithmetic and little substitution, I think Coq is a lot better.

Also, there is no reason Twelf cannot have an arithmetic decision procedure, whereas there is a reason Coq cannot have HOAS, but your query seems more pragmatic than that.
 
2226. Anonymous (dsl-80-45-182-153.access.as9105.com) – 12 Mar 2005 10:40:07 FLAMING TEXT ]
This is shit
 
2225. adamc (12.45.39.194) – 11 Mar 2005 23:04:51 Spring Break! ]
So my statement about "the functional subset of OCaml" was inaccurate. In my defense, I did preface it with the get-out-of-jail-free-card "basically." :-)

What I really meant is that you can use the basic ML syntax that you're used to instead of having to express all recursion as calls to fold functions, or otherwise indicating primitive recursion explicitly.

In response to Andrew: I'm still not convinced that substitution lemmas alone make Twelf worth using. An arithmetic decision procedure is such a time saver for proving facts about assembly programs. Coq also has a bag of other very useful tactics, including one that uses a complete propositional logic decision procedure (combined with definition unfolding and other low-cost tactics) to solve as much of a goal as it can and then decompose the rest into simplified subgoals.
 
2224. jcreed (pool-151-201-33-228.pitt.east.verizon.net) – 11 Mar 2005 21:14:38 UPD: Welcome to the Machine ]
I've got a machine-head. It is better than the rest.
Green to red. Machine-head.
And I walk from my machine.
Indeed, I walk from my machine.
 
2223. Tom 7 (gs82.sp.cs.cmu.edu) – 11 Mar 2005 17:26:40 shhhhh. ]
I think it's more like formally proving that it's incorrect.
 

[ next 25 ]