On Mon, Feb 1, 2010 at 1:02 PM, Matthew Flatt <[email protected]> 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
_________________________________________________
For list-related administrative tasks:
http://list.cs.brown.edu/mailman/listinfo/plt-dev
