I see that it uses the 'traditional' stepping forwards/backwards like ProofGener... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		chriswarbo on June 15, 2015 \| parent \| context \| favorite \| on: PeaCoq, a UI for Coq 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/ )

chriswarbo on June 15, 2015 [–]

Of course I meant 8.5, not 1.5!

Ptival on June 15, 2015 | [–]

Thanks, this is very interesting and I'd love to switch to 8.5.

I might wait a little for my benchmarks to be 8.5 ready though!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact