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

On Mon, Feb 1, 2010 at 1:02 PM, Matthew Flatt <mflatt at cs.utah.edu> wrote:
> 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.

I am fairly certain that other editors can save files with a ".lisp"
extension, so I don't know what you mean here.

> Also, the space of
> file extensions seems much smaller than the space of `#lang' words.

Conceptually, no; pragmatically, you are probably right.  I'm not sure
this is a major concern for us, though.  This feature, even if we
adopt it, would be the exception rather than the rule for PLT Scheme,
right?

> 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.

Presumably the same way `#reader(planet "reader.ss" ("cce"
"dracula.plt" 8 0) "modular" "lang")' gets translated to the "Modular
ACL2" language level currently.  The language level tool must register
itself and its identifying metadata.

--Carl