Stream: Elpi users & devs

Topic: Module enumeration (again)

view this post on Zulip Michael Soegtrop (Jan 16 2024 at 18:11):

I am working on a tool to compare (arithmetic) Coq libraries - based on enumerating modules and finding similar lemmas (with some heuristics). This is all nice and pleasant to do in elpi, just I don't see a way to enumerate the contents of top level modules like "ZArith". When I do something like:

    coq.locate-module "ZArith" MODPATH,
    coq.env.module MODPATH LISTMODITEM,
    coq.say "MODULE" MODPATH LISTMODITEM,

the result is

MODULE «Coq.ZArith.ZArith» []

view this post on Zulip Enrico Tassi (Jan 16 2024 at 20:26):

Looks like a bug. Technically Zarith is a library (a file I guess), not a module, but the API should not make any difference.

view this post on Zulip Michael Soegtrop (Jan 17 2024 at 08:30):

Indeed it would enable quite a few interesting search and library maintenance applications if one could enumerate say ZArith - I am looking forward to a fix.

Last updated: Oct 13 2024 at 01:02 UTC