Ticket #184 (new defect)
Opened 5 years ago
modular acl2 unresolved import problem, useless error message
|Reported by:||pnkfelix||Owned by:||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.