id	summary	reporter	owner	description	type	status	priority	milestone	component	resolution	keywords	cc	planetversion	pltversion
184	modular acl2 unresolved import problem, useless error message	pnkfelix	cce	"Running the following program in Modular ACL2
{{{
(interface Ispec-and1 (sig andp1 (x y)))

(interface Ispec-and2 (sig andp2 (x y)))

(module Mprob
  (import Ispec-and1)
  (defun andp2 (x y) (andp1 x y))
  (export Ispec-and2))

(module Mprob/impl-and1
  (defun andp1 (x y) (and x y))
  (export Ispec-and1))

(link Mprob/test (Mprob Mprob/impl-and1))
(invoke Mprob/test)
}}}

yields the following error message:
{{{
. invoke: unresolved imports:
((andp1))
from exports:
((andp1) (andp2))
 in: mprob/test
}}}

1. Is my program actually doing something wrong?  I do not see why any imports are unresolved.  (The error does not occur if I take out the invoke on the last line of the program.

2. Either way, the error message is not helpful.

"	defect	new	major		cce/dracula.plt					4.1.5