[plt-dev] Associating metadata with modules

From: Jay McCarthy (jay.mccarthy at gmail.com)
Date: Sun Mar 7 21:34:09 EST 2010

Since I've studied the zo format quite a bit recently, I can say that
this structure:


accurately shows what is available in a module at the bytecode level.

Internally, it is just a list. I'm not sure the best way to get
information into there (ie what API do we want), but it would be easy
to put into the structure.

Another way to do it is to have a provide at a strange phase (rather
than taking a name from the global eval (phase 0) namespace.)


On Sun, Mar 7, 2010 at 6:43 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> Yes, if there were a way to add arbitrary properties to modules that
> would be wonderful and greatly simplify my code.
> Carl Eastlund
> On Sun, Mar 7, 2010 at 8:33 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> There are properties in the compiled file that tell us about a
>> module's exports. Would something like that work, if that mechanism
>> could be extended?
>> Robby
>> On Sun, Mar 7, 2010 at 2:15 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
>>> For Hygienic ACL2, I need to associate a few pieces of metadata with
>>> compiled modules.  These include the proof obligations of the module,
>>> the exports of the module, and so forth.  I'm not sure where to
>>> "stick" this information so that it will be available to clients (in
>>> their transformer phase, should that be relevant).
>>> It has been suggested to me that I add an export to the module with
>>> the data I need, but this is inconvenient.  It means I eat up a point
>>> in the module's namespace, and that I have to play "except-in" or
>>> "rename-in" or "prefix-in" games with all of my module requires so
>>> that this one common import doesn't clash between multiple
>>> dependencies.
>>> I have tried creating a hash table associating module names with
>>> metadata, but it turns out that module names are a moving target.
>>> They can be symbols or paths; for the modules I have tried, I get a
>>> symbol back during the module's own transformer phase, but I get a
>>> path back during its runtime phase and from either phase of another
>>> module that depends on it.  (In all cases, I used the name of a
>>> resolved module path.  In the module itself, I got this from a
>>> variable reference; from a different module, I used the module name
>>> resolver.)
>>> Does anyone have a better suggestion for how to associate data with a
>>> module, or for a reliable module identity to serve as a key in a hash
>>> table?
>>> Carl Eastlund
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-dev

Jay McCarthy <jay at cs.byu.edu>
Assistant Professor / Brigham Young University

"The glory of God is Intelligence" - D&C 93

Posted on the dev mailing list.