from Hacker News

PeaCoq, a UI for Coq

by geal on 6/14/15, 7:54 PM with 8 comments

• by rubiquity on 6/15/15, 12:41 AM

  I can't think of a more perfect name for a UI library for the Coq programming language. I'll show myself out now.

• by chriswarbo on 6/15/15, 9:13 AM

  I see that it uses the 'traditional' stepping forwards/backwards like ProofGeneral and CoqIDE.

  Improvements have been made in Coq 1.5 which make this unnecessary: using the PIDE system (originally from Isabelle) you can now throw the whole file at Coq, then send it diffs as the user makes edits. No need to rewind, go-to, etc.

  I've used this in jEdit ( http://coqpide.bitbucket.org/ ) but there's also an Eclipse system built on it too ( https://coqoon.github.io/cav2015/ )

• by mpu on 6/15/15, 4:52 AM

  For hardcore users I don't think this tactic suggestion thing is a good idea, for example, how does it deal with custom ltac tactics (cf Chlipala's bedrock)? To prove me wrong one could test the idea on, say, compcert's development and compute how often the next tactic is among the suggested ones.

  On the other hand, One common problem in large proofs is having too many hypothesis in stock, one super nice extension would be to quantify the relevance of each and color/display them accordingly, leaving the option to move the 'tolerance' threshold for display. This relevance metric would have to be aware if lemmas available (of A -> B is proved by a lemma, and B is the goal, A is relevant).

  My 2 cts.

• by microcolonel on 6/15/15, 2:37 AM

  I use proof general(which also supports Isabelle), but I'm aware that there are in fact some people in the world who have not seen the light of St. Ignucius, and for those I'm sure this is plenty cool.

  Good job. :)