On Mon, Feb 1, 2010 at 11:51 AM, Matthew Flatt <mfl...@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 _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev