Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General
Hi,
this seems like a perfect target for Debian Science. Would you consider
team maintenance.
Kind regards
Andreas.
On Fri, May 11, 2012 at 02:35:23PM +0200, Hendrik Tews wrote:
> 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
>
>
>
> --
> To UNSUBSCRIBE, email to debian-devel-REQUEST@lists.debian.org
> with a subject of "unsubscribe". Trouble? Contact listmaster@lists.debian.org
> Archive: http://lists.debian.org/6x3976vqt0.fsf@blau.inf.tu-dresden.de
>
>
--
http://fam-tille.de
Reply to: