The Coq mailing list

[Epiphanie <landeguy AT gmail.com>]

Hello all,

I'm writing a Coq IDE and I came along several problems I could not find any documentations about. I just would like to know if I missed something..

The first one is about -ideslave mode of coqtop. The only doc I could find out was the dtd and some stuff I decoded from the source on github. Thereby I still do not know how to use the multiprocess mechanics of it (everytime I call it on any id, it instantly gives the answer, I couldn't find find a way to "lock" the chanel)

Since the XML coq returns seems a bit messy (empty list, <list> tag inside <goal> tag and so on) I was also wondering how much it was subject to change. Is -ideslave a very internal project and therefor very mutable in nature or is it supposed to be used by other program in which case its interface is set in stone?

Since then, I found another mode of coqtop -quiet. This one seems to do exactly what I want since I will have my own tactics to display the goal and such. But since it is not -ideslave, I suppose multi-tasking in it is then impossible?

Is there any other mode I missed out?

Finally, I have questions about LTac. This language seems powerful enough to perform interesting automation, however as a post on Galinium showed, there seems to be some heavy restriction on it.

For instance, I cannot find a way to use the Search mechanic (vernacular command) inside a tactic, or even to know the number of subgoal there is.

I skimmed through the code of SSReflect and they do it through caml plugin, just like the said post suggested.

However, I found nothing in the documentation about how to write your own Coq extension just like SSReflect does, and its consacred section on the FAQ is left blank.

So here it is. Sorry if this is a lot of question, I'm just asking about links that explains this or simple explanations, I searched a lot but...

Well, thanks in advance for your help!

Cheers!

Epiphanie