[plt-dev] #lang: the stake in Dracula's heart?

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.