The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Definitely look at the jsCoq side too; they are doing plenty of neat things 
wrt printing goals.

On 03/27/2016 08:53 AM, Gregory Malecha wrote:
> Hello, Hani --
> 
> What format are you looking for the information to be in? Without doing 
> anything on the Coq implementation side, you can run the ideslvae protocol 
> and parse the results (you might want to issue 'Set Printing All' first so 
> you don't need to worry about notations). I know of several projects that 
> have done something similar to this.
> 
> I did a very hacky implementation a while ago:
> https://github.com/gmalecha/coq-interact
> Val Roberts at UCSD has done something nicer for PeaCoq:
> http://goto.ucsd.edu/peacoq/ (probably check out the source code)
> 
> 
> On Sat, Mar 26, 2016 at 5:40 PM, Hani Awni 
> <hani.awni AT gmail.com
>  
> <mailto:hani.awni AT gmail.com>>
>  wrote:
> 
>     Hello,
>     What would be the best way to get the current proof state at the point 
> in interactive proving where Coq is expecting the human to suggest the next 
> tactic? For example, I need the information for Proof General's display of 
> the list of goals when it is waiting for the user to input "intros", 
> "trivial", etc.
> 
>     For background, I am a cognitive scientist and budding computer 
> scientist working in Dr. Hummel's Abstract Relational Reasoning cognitive 
> science lab at UIUC, where we have a python model (called LISA) of how 
> humans solve relational analogies. The idea is, during an attempt at using 
> Coq to prove a human-specified theorem, our model should be able to 
> recognize the abstract, structural similarity of the current goals and 
> proof state to previous examples it has seen, and consequently suggest the 
> appropriate tactic string, including specific mappings like what variable 
> to apply over.
>     In order for this to happen, I must automatically translate the proof 
> state given by Coq into a series of propositions for LISA to understand. I 
> can design this translation, but the first step in this is getting my hands 
> on Coq's current goals list, whether in OCaml or Lisp or Python.
> 
>     On the #coq IRC, it was suggested that I implement a new tactic using a 
> Coq plugin in OCaml, because there I could acquire the proof state; 
> however, a tactic specifies the new proof state, whereas our model can only 
> provide the tactic to use. Can I recursively attempt a new tactic in place 
> of my current one?
> 
>     This seems like a basic need, so I feel like I have overlooked 
> something very basic in my searching; feel free to point out the obvious 
> approaches first.
> 
>     Thank you,
>     Hani Awni
> 
> 
> 
> 
> -- 
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/

Attachment: signature.asc
Description: OpenPGP digital signature