[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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


this seems like a perfect target for Debian Science.  Would you consider
team maintenance.

Kind regards


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


Reply to: