Accès à la sortie AST riche en XML de Coq

Question

Dans les anciennes versions de Coq (< 8.5), le processus principal coqtop échangeait des données avec des IDE à l'aide de chaînes.

Cela a été supposé récemment changé - comment peut-on interroger la structure plus riche de type XML représentant les AST? Cas d'utilisation: Je voudrais interpréter n'importe quel Coq d'une manière différente - c'est-à-dire que j'ai besoin de ses résultats après avoir effectué des opérations (comme invoquer des tactiques) sous une forme que je n'ai pas besoin d'analyser.

Answer 1

En utilisant le protocole XML, vous pouvez utiliser le Annotate stm call, où stm est la phrase que vous voulez imprimer. Cependant, notez que l'imprimante XML est loin d'être entièrement fonctionnelle dans les versions 8.5/8.6 et peut être supprimée. Vous pouvez voir tous les cas manquants here. Notez également qu'il ne génère aucune représentation structurée des termes à aucun niveau.

Alternativement, vous pouvez utiliser SerAPI, un addon spécialisé dans ce but particulier. En utilisant SerAPI vous pouvez obtenir une représentation complète de toute structure Coq:

$ rlwrap ./sertop.native --printer=human --prelude=/home/egallego/external/coq-v8.6/ 
(Control (StmAdd() "Lemma u n : n + 0 = n.")) 
> (Answer 0 (StmAdded 2 (...) NewTip)) 
(Query() (Ast 2)) 
> (Answer 1(ObjList 
> ((CoqAst 
> (VernacStartTheoremProof Lemma 
>  ((((((Id u))())) 
>  (((LocalRawAssum 
>   (((Name (Id n)))) 
>   (Default Explicit) 
>   (CHole() IntroAnonymous()))) 
>  (CNotation 
>   "_ = _" 
>   (((CNotation 
>   "_ + _" 
>   (((CRef 
>    (Ident 
>     (Id n))) 
>    ()) 
>    (CPrim 
>    (Numeral (Ser_Bigint 0)))) 
>   ()())) 
>   (CRef 
>   (Ident 
>    (Id n))) 
>   ())) 
>   ()())) 
>  ()))) 
>  false))))) 

Notez que SerAPI est un logiciel expérimental.