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