Unknown types error when importing thc file

[alwentiu]

Hi, I'm testing the import feature of Abella 2.05. but stumbled on a 'unknown types' error. Here's a simple example to trigger the error. Suppose test1.thm has a kind declaration:

Kind tm type.

Compile this to produce test1.thc. Then import this in test2.thm:

Import "test1".

This results in the following error:

Error: Imported file makes reference to unknown types: tm

Am I doing the import correctly? Or is this a bug?

Thanks, Alwen

[chaudhuri]

This is actually expected behavior, or at least intentionally programmed behavior. The semantics of "Import" is that it imports concrete things such as definitions and theorems, but not abstract stuff like type and constant declarations. Thus, at the point of an Import both the importer and the importee are expected to agree on the type signature.

Part of this is by necessity, since the specification and reasoning type signatures are directly identified, and we can have only at most one specification in a given development.

Personally, i have always felt this to be a rather peculiar quirk of Abella's implementation of Import. When we finally get reasoning-level modules working, we can probably do "the correct thing" with respect to parametric aspects of imported modules.

I think more discussion is needed and it is better suited for the Abella mailing list. I am closing this issue since I don't think this is a bug as such, and relation-level modules will eventually obviate any possible feature request.

[JimmyZJX]

Luckily I did not run into this issue because I Imported another thm before the Kind declaration, say Import "test0". in test1.thm. Then this error message no longer shows for test2.thm.

Is that the expected behavior of Abella?