*To*: Andreas Tille <andreas@an3as.eu>*Cc*: Hendrik Tews <tews@os.inf.tu-dresden.de>, 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*: Ralf Treinen <treinen@free.fr>*Date*: Mon, 14 May 2012 20:33:01 +0200*Message-id*: <20120514183301.GB3968@free.fr>*In-reply-to*: <20120514100332.GL31335@an3as.eu>*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> <20120514100332.GL31335@an3as.eu>

On Mon, May 14, 2012 at 12:03:32PM +0200, Andreas Tille wrote: > 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? ScienceLogic [1] would be more appropriate, IMHO, in particular when ScienceMathematics is getting crowded. [1] http://wiki.debian.org/DebianScience/Logic -Ralf.

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

**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>

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

- Prev by Date:
**Re: Please, uipload sumo** - Next by Date:
**Re: Bug#672480: ITP: prooftree -- proof tree visualization for Proof General** - 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):