The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Is there a command I can run on a .vo file to extract its logical pathname?

I can do it interactively using votour, but I was wondering whether I can pass the instructions to votour at command line itself so that no future interaction is needed:

[abhishek@anand-lenovo ~]$ votour ~/.opam/4.07.1+flambda/lib/coq/theories/Arith/Arith.vo

Welcome to votour !
Enjoy your guided tour of a Coq .vo or .vi file
Object sizes are in words (64 bits)
At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits

File format: 81300
The file has 5 segments, choose the one to visit:
 0: library, starting at byte 6543 (size 3945w)
 1: opaques, starting at byte 13222 (size 0w)
 2: summary, starting at byte 16 (size 3866w)
 3: tasks, starting at byte 13185 (size 0w)
 4: universes, starting at byte 13148 (size 0w)
# 0

Depth 0 Pos  Context  
-------------
Here: library (size 3945w) [0x00000000], 2 children:
 0: compiled (size 3885w) [0x00000001]
 1: library_objects (size 57w) [0x0000055f]
-------------
# 0

Depth 1 Pos 0 Context library
-------------
Here: compiled (size 3885w) [0x00000001], 5 children:
 0: dirpath/list/string (size 13w) [0x00000002]
 1: module_body (size 16w) [0x00000007]
 2: universe_context_set (size 3w) [0x0000000c]
 3: array/dep (size 3847w) [0x0000000d]
 4: impr-set [imm=1] (size 0w)
-------------
# 0

Depth 2 Pos 0.0 Context library/compiled
-------------
Here: dirpath/list/string (size 13w) [0x00000002], 3 children:
 0: string [Arith] (size 2w) [0x00000003]
 1: string [Arith] (size 2w) [0x00000003]
 2: string [Coq] (size 2w) [0x00000006]

-- Abhishek

http://www.cs.cornell.edu/~aa755/