On Mon, Feb 1, 2010 at 2:26 PM, Matthias Felleisen <[email protected]> wrote: > > Can't the language come with code that makes the > > #lang acl2 > > line appear and disappear on write/read from the program's file? > > As for sending it from drscheme to the ACL2 theorem prover, I > imagine that this is all under your control. -- Matthias
DrScheme needs to be able to read ACL2 files written by other programs, such as the ACL2 books. ACL2 should be able to read files written by DrScheme directly, without always having to go through Dracula. If we want ACL2 to "open up" for compatibility with other tools such as Dracula, there's a quid pro quo that we not make our own tool needlessly incompatible with ACL2. --Carl _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev
