*To*: Hendrik Tews <tews@os.inf.tu-dresden.de>*Cc*: 672480@bugs.debian.org, Debian Science List <debian-science@lists.debian.org>*Subject*: Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General*From*: Andreas Tille <andreas@an3as.eu>*Date*: Mon, 14 May 2012 12:03:32 +0200*Message-id*: <20120514100332.GL31335@an3as.eu>*In-reply-to*: <20400.51148.459834.631620@blau.inf.tu-dresden.de>*References*: <6x3976vqt0.fsf@blau.inf.tu-dresden.de> <20120512185620.GD32645@an3as.eu> <20400.45995.639943.711869@blau.inf.tu-dresden.de> <20120514080333.GD31335@an3as.eu> <20400.51148.459834.631620@blau.inf.tu-dresden.de>

On Mon, May 14, 2012 at 10:52:28AM +0200, Hendrik Tews wrote: > > and tell us, in what task your package might fit best. > > If prooftree ever makes it into Debian, it should be together > with coq and proof-general, ie. science-mathematics. OK, thanks. I'll care for this. > BTW: > - matita, agda, prover9 are proof assistants similar to coq, but > not listed in science-mathematics > - hol-light, currently waiting in the new-queue, too I will add all these - new is regarded in the tasks generation script as well. > - minisat would also belong to this group > - you might want to have a separate meta-package > "theorem-proving" or "formal-methods" for all these tools This kind of input is exactly what is wanted here on this list. Regarding the split into separate meta-packages: While I agree that science-mathematics becomes a bit crowded I'm not fully sure that we should keep on maintaining mathematical packages under the Debian Science umbrella. I'd rather vote for some math-* tasks which enables mor fine grained tasks (same probably for physics). Any opinions? Kind regards Andreas. -- http://fam-tille.de

**Follow-Ups**:**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General***From:*Ralf Treinen <treinen@free.fr>

**References**:**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General***From:*Andreas Tille <andreas@an3as.eu>

**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General***From:*Hendrik Tews <tews@os.inf.tu-dresden.de>

**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General***From:*Andreas Tille <andreas@an3as.eu>

**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General***From:*Hendrik Tews <tews@os.inf.tu-dresden.de>

- Prev by Date:
**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General** - Next by Date:
**Re: Please, uipload sumo** - Previous by thread:
**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General** - Next by thread:
**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General** - Index(es):