The Coq mailing list

[Wouter Geraedts <radboud AT woutergeraedts.nl>]

Hello,

I am attempting to extract the XML:ACIC representation of the Coq 
standard library. Ideally I would like to have a separate XML file per 
.v file.

I have tried several approaches, of which the two most successful are:
(1) adding -xml to the COQ_XML variable in Makefile.build as suggested 
at the documentation + Mowgli documentation.
(2) running 'bin/coqtop.opt -boot -xml -nois -compile Datatypes' and 
similar as suggested here:
        
http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/4016

Approach (1) dumps all XML to stdout. This is not ideal as this is mixed 
with various output from the Coq build process. Declaring 
COQ_XML_LIBRARY_ROOT should write separate XML files to this root folder.
This approach (1b) however fails, with coqdoc attempting to read from 
empty .v files which are deployed to the COQ_XML_LIBRARY_ROOT-folder. 
Oddly the following succeeds:
- first building without the COQ_XML_LIBRARY_ROOT declaration
- aborting midway
- building with COQ_XML_LIBRARY_ROOT
This succeeds up to the point of the abort. Looking at the file diff I 
only see some .glob files deleted after running the first pass. Letting 
the first pass complete before running the second pass results in the 
same problems as if the first pass was never run.

Approach (2) does not yield any output to stdout or file. It just runs 
and returns to the commandline.

I am running coq-8.4pl5 from source on Ubuntu 14.04 x64.

Any help will be appreciated.

Greetings,
Wouter Geraedts