At Mon, 1 Feb 2010 11:57:31 -0600, Robby Findler wrote: > > One other possibility is to use a file extension. I don't like > > depending on extensions, but it's the one general way that systems > > offer to designate a file type. We could treat file extensions in a > > similar way to `#lang' declarations. If we did that, would using an > > ".acl2" extension (or whatever the right extension) be a good way > > indicate an ACL2 source? > > I'm not sure I really get the tradeoffs here-- what makes you worry > about this one? (It seems like a smooth path that has been getting > smoother in recent years, at least in my mac experience.)
If a file extension is the only way to declare ACL2, then you'd have to save a file in DrScheme to use the ACL2 language. Also, the space of file extensions seems much smaller than the space of `#lang' words. Finally, I'm not sure how a file extension would get mapped to "planet cce/acl2". But maybe all of that could be worked out. At Mon, 1 Feb 2010 12:58:25 -0500, Carl Eastlund wrote: > ACL2 uses the ".lisp" extension; it is mandatory for certification. > That would certainly be one way to detect use of Dracula. That's a good example of the limited namespace, since ".lisp" doesn't seem particularly tied to ACL2 otherwise. _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev
