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

On Mon, Feb 1, 2010 at 11:51 AM, Matthew Flatt <mflatt at cs.utah.edu> wrote:
> At Mon, 1 Feb 2010 12:13:40 -0500, Carl Eastlund wrote:
>> (Pardon the overly dramatic title, this is probably a far-off concern
>> right now, but the pun was irresistible.)
>>
>> I know we are trying to make #lang into our primary "language level"
>> mechanism; this is a good thing.  My question to the other developers
>> is: are we trying to make it our only mechanism?  Are there plans to
>> abandon other methods of language specification?
>>
>> As the Dracula maintainer, this is crucial to me.  Dracula can only
>> cooperate with ACL2 if source files are readable by both.  If we go to
>> #lang-only modules, ACL2 will not be able to read files written in
>> Dracula, as it does not understand `#lang planet cce/dracula', and
>> Dracula will not be able to read ACL2's libraries, as `(in-package
>> "ACL2")' is not a #lang specification.
>>
>> What are our plans for non-#lang languages and compatibility with
>> other compilers, in the foreseeable future?
>
> I don't think that we will get rid of dialog-based language selection
> completely. We should get away from it as much as possible, but maybe
> that doesn't include ACL2.

Perhaps, eventually, the language-dialog-based selection of languages
will amount to an invisible "#lang acl2" (or whatever) stuck at the
front of the file and then otherwise using all of our other
#lang-specific tech?

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

Robby