Bug#672480: ITP: prooftree -- proof tree visualization for Proof General

[Hendrik Tews <hendrik@askra.de>]

Package: wnpp
Owner: Hendrik Tews <hendrik@askra.de>
Severity: wishlist

* Package name    : prooftree
  Version         : 0.9
  Upstream Author : Hendrik Tews
* URL or Web page : http://askra.de/software/prooftree/
* License         : GPL-3
  Description     : proof tree visualization for Proof General

 Prooftree draws proof trees during interactive proof development
 with Proof General. One can inspect goals and proof commands
 and check where existential variables were introduced and
 instantiated. Currently, Prooftree does only work for Coq.


Actually Prooftree requires Coq 8.4, which has not been released
yet. There is also work on supporting HOL Light, but this has not
been released either. However, there is a good chance that 
Coq 8.4 and/or the HOL Light support in Proof General will get
included in the next Debian release. Given the time it takes to
get a new package into Debian, it is probably not too early to
start now with packaging Prooftree.

Even if Coq 8.4 and the HOL Light support in Proof General will
not be included in the next Debian release, it would be good to
have Prooftee in the archive. Users would then only need to
install Coq or Proof General manually and could rely on the
Prooftree package.


Bye,

Hendrik