Ticket #184 (new defect)

Opened 5 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.