Can I dump a Coq file to a format besides a .vo? Preferably one that is easier to read and manipulate from another program.
I know that Coq supports extraction to OCaml, Haskell, Scheme and JSON, but I'm looking for something that doesn't require modifying the target source (if indeed such a thing exists).
Suppose I have a simple Coq file.
sh:2 $ cat add.v
Fixpoint add a b : nat :=
match a with
| O => b
| S a' => S (add a' b)
end
.
I can compile it into a .vo file with coqc. (You also get some other files, but the .vo is what you need to import a Coq file into another one. )
sh:2 $ coqc add.v ; xxd add.vo
00000000: 436f 7121 0001 404f 0000 0000 0000 0897 Coq!..@O........
00000010: 8495 a6be 0000 025c 0000 008c 0000 01c2 .......\........
00000020: 0000 0187 c0a0 2361 6464 4008 0000 3f00 ......#add@...?.
00000030: a0a0 294e 6f74 6174 696f 6e73 a024 496e ..)Notations.$In
00000040: 6974 a023 436f 7140 9030 f776 2c42 42ef it.#[email protected],BB.
00000050: 437a 0967 2cf5 6032 ff29 a0a0 244c 7461 Cz.g,.`2.)..$Lta
00000060: 63a0 2449 6e69 74a0 2343 6f71 4090 303f c.$Init.#[email protected]?
00000070: a669 1536 6f60 10a8 eac5 58d7 1f67 9fa0 .i.6o`....X..g..
00000080: a025 4c6f 6769 63a0 2449 6e69 74a0 2343 .%Logic.$Init.#C
00000090: 6f71 4090 30b8 fcd2 085c 6bdb 069a 2f70 [email protected]....\k.../p
000000a0: bca5 dba2 94a0 a029 4461 7461 7479 7065 .......)Datatype
000000b0: 73a0 2449 6e69 74a0 2343 6f71 4090 30d5 s.$Init.#[email protected].
000000c0: 4b98 149d 87f6 1901 9ba5 92e8 e3e5 93a0 K...............
000000d0: a026 5370 6563 6966 a024 496e 6974 a023 .&Specif.$Init.#
000000e0: 436f 7140 9030 daf5 8de3 14a4 da1e bc42 [email protected]
000000f0: 0002 3b03 9fbe a0a0 2744 6563 696d 616c ..;.....'Decimal
00000100: a024 496e 6974 a023 436f 7140 9030 5d56 .$Init.#[email protected]]V
00000110: 7d3e d01c a973 4c08 d3c3 ed63 2e74 a0a0 }>...sL....c.t..
00000120: 2b48 6578 6164 6563 696d 616c a024 496e +Hexadecimal.$In
00000130: 6974 a023 436f 7140 9030 176b a57e 6b15 it.#[email protected].~k.
00000140: d3cb f56a 457d a8fe 0172 a0a0 264e 756d ...jE}...r..&Num
00000150: 6265 72a0 2449 6e69 74a0 2343 6f71 4090 ber.$Init.#Coq@.
00000160: 30c7 679a 0eef 64f1 5da2 c5a2 ca6a 02c9 0.g...d.]....j..
00000170: 75a0 a023 4e61 74a0 2449 6e69 74a0 2343 u..#Nat.$Init.#C
00000180: 6f71 4090 3010 8781 d539 6bcf 49bb e360 [email protected]..`
00000190: 834a c36c d0a0 a024 4279 7465 a024 496e .J.l...$Byte.$In
000001a0: 6974 a023 436f 7140 9030 a0f6 a47a a6e5 it.#[email protected]..
000001b0: 11a9 5276 3f00 9e7c 6564 a0a0 2550 6561 ..Rv?..|ed..%Pea
000001c0: 6e6f a024 496e 6974 a023 436f 7140 9030 no.$Init.#[email protected]
000001d0: 2223 ea0d 85b5 2a88 3f69 517b ec50 c5eb "#....*.?iQ{.P..
000001e0: a0a0 2257 66a0 2449 6e69 74a0 2343 6f71 .."Wf.$Init.#Coq
000001f0: 4090 30ad 00ad 4336 ad65 1620 ee70 df92 @.0...C6.e. .p..
00000200: 13f2 28a0 a027 5461 6374 6963 73a0 2449 ..(..'Tactics.$I
00000210: 6e69 74a0 2343 6f71 4090 305e 26de a0fd nit.#[email protected]^&...
00000220: b7c1 952a 259a 1de0 19d6 80a0 a025 5461 ...*%........%Ta
00000230: 7574 6fa0 2449 6e69 74a0 2343 6f71 4090 uto.$Init.#Coq@.
00000240: 3037 9404 b26c d7b4 cad4 04fe 3970 17f3 07...l......9p..
00000250: 84a0 a027 5072 656c 7564 65a0 2449 6e69 ...'Prelude.$Ini
00000260: 74a0 2343 6f71 4090 30eb 08be 9fa9 fa24 t.#[email protected]......$
00000270: 0c6b 66ae 6068 a263 9125 352e 322e 3040 .kf.`h.c.%5.2.0@
00000280: d6f3 44df a907 381b 42ff c5e0 608e 077b ..D...8.B...`..{
00000290: 8495 a6be 0000 0574 0000 013c 0000 0429 .......t...<...)
000002a0: 0000 03bf b0c0 a023 6164 6440 e090 0404 .......#add@....
000002b0: 4190 a0a0 0406 9008 0000 2700 40a0 8080 A.........'.@...
000002c0: 919e a0a0 9040 40b0 90a0 9004 1240 90b6 .....@@......@..
000002d0: a090 2161 409b a0a0 90b0 90a0 2944 6174 ..!a@.......)Dat
000002e0: 6174 7970 6573 a024 496e 6974 a023 436f atypes.$Init.#Co
000002f0: 7140 236e 6174 020e f216 0640 041c b6a0 q@#nat.....@....
00000300: 9021 6240 0411 0411 90b7 0416 0413 b704 .!b@............
00000310: 0604 14fd d004 1440 a040 41a0 4041 b040 .......@.@A.@A.@
00000320: a040 a040 4044 042a 80a0 a090 0421 041e .@.@@D.*.....!..
00000330: 4040 9042 a0a0 8090 41a0 90a0 9022 6127 @@.B....A...."a'
00000340: 40a9 9ca0 a004 2942 043a 90a9 9044 a004 @.....)B.:...D..
00000350: 0e04 1104 3340 90a0 a00a 0000 0114 2c00 ....3@........,.
00000360: 0000 0100 0000 0000 0000 0000 0000 2c00 ..............,.
00000370: 0000 0300 0000 8800 0000 2800 0000 2a00 ..........(...*.
00000380: 0000 0000 0000 2800 0000 2900 0000 0100 ......(...).....
00000390: 0000 0000 0000 3b00 0000 0100 0002 1300 ......;.........
000003a0: 0000 0300 0000 0a00 0000 4e00 0000 1200 ..........N.....
000003b0: 0000 f9ff ffff 0000 0000 0200 0000 2700 ..............'.
000003c0: 0000 0200 0000 3d00 0000 0b00 0000 0a00 ......=.........
000003d0: 0000 3100 0000 2000 0000 3700 0000 0100 ..1... ...7.....
000003e0: 0000 2700 0000 0300 0000 0100 0000 2700 ..'...........'.
000003f0: 0000 0200 0000 2b00 0000 0000 0000 0400 ......+.........
00000400: 0000 1200 0000 0200 0000 8800 0000 3400 ..............4.
00000410: 0000 0100 0000 2700 0000 0100 0000 2b00 ......'.......+.
00000420: 0000 0000 0000 0600 0000 3500 0000 0100 ..........5.....
00000430: 0000 3800 0000 0000 0000 8800 0000 2b00 ..8...........+.
00000440: 0000 0000 0000 0700 0000 3500 0000 0100 ..........5.....
00000450: 0000 3800 0000 0000 0000 2700 0000 0100 ..8.......'.....
00000460: 0000 3400 0000 0100 0000 2700 0000 0100 ..4.......'.....
00000470: 0000 a0a0 90b0 a0a0 4040 a041 4141 4391 ........@@.AAAC.
00000480: 91a0 90b0 90a0 2944 6174 6174 7970 6573 ......)Datatypes
00000490: a024 496e 6974 a023 436f 7140 236e 6174 .$Init.#Coq@#nat
000004a0: 020e f216 0640 2558 5c1c 2018 8040 4008 .....@%X\. ..@@.
000004b0: 0000 2f00 4141 41c0 4040 a041 4004 0141 ../.AAA.@@[email protected]
000004c0: 4140 4040 4140 4040 a040 4090 40a0 4040 A@@@A@@@.@@.@.@@
000004d0: 0800 003f 00a0 a024 4279 7465 a024 496e ...?...$Byte.$In
000004e0: 6974 a023 436f 7140 9030 a0f6 a47a a6e5 it.#[email protected]..
000004f0: 11a9 5276 3f00 9e7c 6564 a0a0 2944 6174 ..Rv?..|ed..)Dat
00000500: 6174 7970 6573 a024 496e 6974 a023 436f atypes.$Init.#Co
00000510: 7140 9030 d54b 9814 9d87 f619 019b a592 [email protected]..........
00000520: e8e3 e593 a0a0 2744 6563 696d 616c a024 ......'Decimal.$
00000530: 496e 6974 a023 436f 7140 9030 5d56 7d3e Init.#[email protected]]V}>
00000540: d01c a973 4c08 d3c3 ed63 2e74 a0a0 2b48 ...sL....c.t..+H
00000550: 6578 6164 6563 696d 616c a024 496e 6974 exadecimal.$Init
00000560: a023 436f 7140 9030 176b a57e 6b15 d3cb .#[email protected].~k...
00000570: f56a 457d a8fe 0172 a0a0 254c 6f67 6963 .jE}...r..%Logic
00000580: a024 496e 6974 a023 436f 7140 9030 b8fc .$Init.#[email protected]..
00000590: d208 5c6b db06 9a2f 70bc a5db a294 a0a0 ..\k.../p.......
000005a0: 244c 7461 63a0 2449 6e69 74a0 2343 6f71 $Ltac.$Init.#Coq
000005b0: 4090 303f a669 1536 6f60 10a8 eac5 58d7 @.0?.i.6o`....X.
000005c0: 1f67 9fa0 a023 4e61 74a0 2449 6e69 74a0 .g...#Nat.$Init.
000005d0: 2343 6f71 4090 3010 8781 d539 6bcf 49bb #[email protected].
000005e0: e360 834a c36c d0a0 a029 4e6f 7461 7469 .`.J.l...)Notati
000005f0: 6f6e 73a0 2449 6e69 74a0 2343 6f71 4090 ons.$Init.#Coq@.
00000600: 30f7 762c 4242 ef43 7a09 672c f560 32ff 0.v,BB.Cz.g,.`2.
00000610: 29a0 a026 4e75 6d62 6572 a024 496e 6974 )..&Number.$Init
00000620: a023 436f 7140 9030 c767 9a0e ef64 f15d .#[email protected].]
00000630: a2c5 a2ca 6a02 c975 a0a0 2550 6561 6e6f ....j..u..%Peano
00000640: a024 496e 6974 a023 436f 7140 9030 2223 .$Init.#[email protected]"#
00000650: ea0d 85b5 2a88 3f69 517b ec50 c5eb a0a0 ....*.?iQ{.P....
00000660: 2750 7265 6c75 6465 a024 496e 6974 a023 'Prelude.$Init.#
00000670: 436f 7140 9030 eb08 be9f a9fa 240c 6b66 [email protected]......$.kf
00000680: ae60 68a2 6391 a0a0 2653 7065 6369 66a0 .`h.c...&Specif.
00000690: 2449 6e69 74a0 2343 6f71 4090 30da f58d $Init.#[email protected]...
000006a0: e314 a4da 1ebc 4200 023b 039f bea0 a027 ......B..;.....'
000006b0: 5461 6374 6963 73a0 2449 6e69 74a0 2343 Tactics.$Init.#C
000006c0: 6f71 4090 305e 26de a0fd b7c1 952a 259a [email protected]^&......*%.
000006d0: 1de0 19d6 80a0 a025 5461 7574 6fa0 2449 .......%Tauto.$I
000006e0: 6e69 74a0 2343 6f71 4090 3037 9404 b26c nit.#[email protected]
000006f0: d7b4 cad4 04fe 3970 17f3 84a0 a022 5766 ......9p....."Wf
00000700: a024 496e 6974 a023 436f 7140 9030 ad00 .$Init.#[email protected]..
00000710: ad43 36ad 6516 20ee 70df 9213 f228 a040 .C6.e. .p....(.@
00000720: 40a0 a095 a002 320a 518f a004 f3b0 9145 @.....2.Q......E
00000730: 4040 a095 a002 0fc0 a2b8 a090 e040 4140 @@...........@A@
00000740: 4040 40a0 a091 90b0 04fe 0501 0002 3417 @@@...........4.
00000750: 666b a0a0 4040 4040 a095 a002 2760 a06f fk..@@@@....'`.o
00000760: d040 9104 09a0 a029 6e61 745f 7363 6f70 .@.....)nat_scop
00000770: 6540 a0a0 0403 4040 a090 9204 f6a0 9092 e@....@@........
00000780: 04f9 40d0 d040 40a0 a0a0 2a74 7970 655f ..@..@@...*type_
00000790: 7363 6f70 6540 4040 4041 41a0 a0a0 2e66 scope@@@@AA....f
000007a0: 756e 6374 696f 6e5f 7363 6f70 6540 4040 unction_scope@@@
000007b0: d040 92a0 90b0 9004 b224 626f 6f6c 020e .@.......$bool..
000007c0: fc5a 2740 a0a0 a02a 626f 6f6c 5f73 636f .Z'@...*bool_sco
000007d0: 7065 4040 40d0 d040 92a0 90b0 040c 246c pe@@@..@......$l
000007e0: 6973 7402 0efd 5df3 40a0 a0a0 2a6c 6973 ist...].@...*lis
000007f0: 745f 7363 6f70 6540 4040 4041 92a0 90b0 t_scope@@@@A....
00000800: 0415 04d9 020e f216 0640 a0a0 a004 3040 [email protected]@
00000810: 4040 4042 4344 4040 ef19 ed3a 3bd9 48a6 @@@BCD@@...:;.H.
00000820: be02 0a4e 8db4 4c95 8495 a6be 0000 0001 ...N..L.........
00000830: 0000 0000 0000 0000 0000 0000 40c5 e354 [email protected]
00000840: 1197 5aef 719f 04a5 74b4 ff59 4084 95a6 ..Z.q...t..Y@...
00000850: be00 0000 0100 0000 0000 0000 0000 0000 ................
00000860: 0040 c5e3 5411 975a ef71 9f04 a574 b4ff [email protected]..
00000870: 5940 8495 a6be 0000 0001 0000 0000 0000 Y@..............
00000880: 0000 0000 0000 8061 44c8 6cd4 a168 cd70 .......aD.l..h.p
00000890: 495a 5cc4 22ad e900 0000 0500 0000 076c IZ\."..........l
000008a0: 6962 7261 7279 0000 0000 0000 0290 0000 ibrary..........
000008b0: 0000 0000 0588 ef19 ed3a 3bd9 48a6 be02 .........:;.H...
000008c0: 0a4e 8db4 4c95 0000 0007 6f70 6171 7565 .N..L.....opaque
000008d0: 7300 0000 0000 0008 7200 0000 0000 0000 s.......r.......
000008e0: 1561 44c8 6cd4 a168 cd70 495a 5cc4 22ad .aD.l..h.pIZ\.".
000008f0: e900 0000 0773 756d 6d61 7279 0000 0000 .....summary....
00000900: 0000 0010 0000 0000 0000 0270 d6f3 44df ...........p..D.
00000910: a907 381b 42ff c5e0 608e 077b 0000 0005 ..8.B...`..{....
00000920: 7461 736b 7300 0000 0000 0008 4d00 0000 tasks.......M...
00000930: 0000 0000 15c5 e354 1197 5aef 719f 04a5 .......T..Z.q...
00000940: 74b4 ff59 4000 0000 0975 6e69 7665 7273 [email protected]
00000950: 6573 0000 0000 0000 0828 0000 0000 0000 es.......(......
00000960: 0015 c5e3 5411 975a ef71 9f04 a574 b4ff ....T..Z.q...t..
00000970: 5940 Y@
This file pretty clearly contains some magic bytes Coq at the beginning, possibly followed by some version information.
It also contains references to the Coq standard library (that are presumably pulled in because I referenced a nat).
add itself appears to be defined on row 000002a0.
This fabulous answer from SO, which predates the existence of the PA Stack Exchange, explains that this file consists of a bunch of marshaled OCaml objects (with checksums) and includes a link to the dumper code.
I would like, however, to be able to read this serialized file from other programs and this format is not friendly for that.
OCaml also very aggressively erases types (but it has a uniform memory representation), so parsing this format from another program seems like a non-starter. It would be very, very sensitive to the Coq version.
coqc also doesn't seem to support an alternative output format. For example it doesn't appear to be able to dump JSON, or simplified Gallina with vernacular stuff removed, or XML, or whatever.
