Ticket #185 (new defect)
Opened 4 years ago
Modular ACL2 reacts poorly to mixing of "code" and exports
|Reported by:||pnkfelix||Owned by:||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.