id,summary,reporter,owner,description,type,status,priority,milestone,component,resolution,keywords,cc,planetversion,pltversion
185,"Modular ACL2 reacts poorly to mixing of ""code"" and exports",pnkfelix,cce,"Open up the following in Modular ACL2, select the module m, and click ""Admit All"" button

{{{
(interface Ig (sig g (y)))
(interface Ih (sig h (z)))

(module m 
  (defun g (y) (+ y y))
  (defun h (z) (g z))
  (export Ig)
  (in-theory (disable (:executable-counterpart h)))
  (export Ih))
}}}

I get the following internal error from the guts of Dracula/DrScheme:
{{{
highlight/save: start position 177 > end position 125

 === context ===
/Users/pnkfelix/Library/PLT Scheme/planet/300/4.1.5/cache/cce/dracula.plt/8/2/drscheme/dracula-drscheme-tab.ss:
}}}

The obvious workaround is to put the {{{in-theory}}} invocation above the export.  Note however that I think some people might have reason to write down {{{in-theory}}} invocations that effect the proof attempts for some signatures but not all of them.

In any case the internal error is bad.


",defect,new,minor,,cce/dracula.plt,,,,,4.1.5