The Coq mailing list

[Carst Tankink <carst.tankink AT inria.fr>]

Enrico merged François Poulain's work into trunk 1.5 weeks ago, which 
adds the support for XML ASTs. See 
https://github.com/coq/coq/commit/09d13ea251ba9f271fd698edd0d6560b88996a65

I don't know exactly what is planned, but this is the cliff-notes 
version of that commit:

- The command print_ast function is part of the STM API, and if you are 
developing a UI for 8.5, I would strongly suggest building on that API, 
or even consider PIDE (shameless self-advertisement) if you are in the 
JVM world.
- The function prints out the AST for command spans, so after parsing is 
done successfully (when you get parse errors, you cannot recover the AST)
- Most of the generated XML has offset information, relative to the 
command span's begin (which you can/have to record for yourself in your 
UI). In some cases the location is omitted, either because it wasn't 
necessary for the original use cases of the printer, or because the 
information is lost in processing.
- Ltac phrases (VernacSolve entries in the AST) are not marked up, just 
delivered as raw source text. In my understanding, this is because the 
AST for an Ltac is difficult/impossible to recover, but I haven't tried 
yet going against common wisdom to see how far we /can/ push it.

Now, your question about the goals: this is a different set of commits:
https://github.com/coq/coq/commit/9a3abe5b18a84733c0c01c2647108196798a761c
 and
https://github.com/coq/coq/commit/6b9b86ccd9f122e684cf4830f3e00bc3f70a0d8a

Right now, I mimic the data structure for CoqIDE, with some XML 
decoration: you get the record of background/focused/shelved goals, and 
the goals are structured as (hypothesis list, conclusion) but the 
hypothesis and conclusion are just represented as raw text. One could 
spend the time to add more structure to this (separating label and 
statement in the individual hypotheses, for example) and I expect it 
would be possible to use the functions introduced for printing the AST 
to also print the statements in the goals as XML, but that will take a 
while to be done, so I have no idea if it'll make it into 8.5


Carst


On 10/09/2014 04:06 AM, Kenneth Roe wrote:
> I'm told that Coq 8.5 is going to support conversion of Coq syntax to
> XML.  Can someone give me more information on what is planned?  I am in
> the process of developing a UI for Coq.  A couple of items that would be
> nice is if this conversion 1) Saved line/character information in the
> original Coq source and 2) would be able to parse the goal/hypothesis
> status information that is printed after a proof tactic is applied.
>
>                      - Ken