Ticket #184 (new defect)
Opened 15 years ago
modular acl2 unresolved import problem, useless error message
Reported by: | pnkfelix | Owned by: | cce |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | cce/dracula.plt | Keywords: | |
Cc: | Version: | ||
Racket Version: | 4.1.5 |
Description
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.
Note: See
TracTickets for help on using
tickets.