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