nixpkgs-suyu/pkgs/applications/science/logic/prooftree/default.nix
Bjørn Forsman c9baba9212 Fix many package descriptions
(My OCD kicked in today...)

Remove repeated package names, capitalize first word, remove trailing
periods and move overlong descriptions to longDescription.

I also simplified some descriptions as well, when they were particularly
long or technical, often based on Arch Linux' package descriptions.

I've tried to stay away from generated expressions (and I think I
succeeded).

Some specifics worth mentioning:
 * cron, has "Vixie Cron" in its description. The "Vixie" part is not
   mentioned anywhere else. I kept it in a parenthesis at the end of the
   description.

 * ctags description started with "Exuberant Ctags ...", and the
   "exuberant" part is not mentioned elsewhere. Kept it in a parenthesis
   at the end of description.

 * nix has the description "The Nix Deployment System". Since that
   doesn't really say much what it is/does (especially after removing
   the package name!), I changed that to "Powerful package manager that
   makes package management reliable and reproducible" (borrowed from
   nixos.org).

 * Tons of "GNU Foo, Foo is a [the important bits]" descriptions
   is changed to just [the important bits]. If the package name doesn't
   contain GNU I don't think it's needed to say it in the description
   either.
2014-08-24 22:31:37 +02:00

40 lines
1.7 KiB
Nix

{stdenv, fetchurl, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
stdenv.mkDerivation (rec {
name = "prooftree-${version}";
version = "0.12";
src = fetchurl {
url = "http://askra.de/software/prooftree/releases/prooftree-${version}.tar.gz";
sha256 = "08yp66j05pdkdpv9xkfqymqy82mir5xbwfh9mkzhh219xkps4b4m";
};
buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
dontAddPrefix = true;
configureFlags = [ "--prefix" "$(out)" ];
meta = {
description = "A program for proof-tree visualization";
longDescription = ''
Prooftree is a program for proof-tree visualization during interactive
proof development in a theorem prover. It is currently being developed
for Coq and Proof General. Prooftree helps against getting lost between
different subgoals in interactive proof development. It clearly shows
where the current subgoal comes from and thus helps in developing the
right plan for solving it.
Prooftree uses different colors for the already proven subgoals, the
current branch in the proof and the still open subgoals. Sequent texts
are not displayed in the proof tree itself, but they are shown as a
tool-tip when the mouse rests over a sequent symbol. Long proof commands
are abbreviated in the tree display, but show up in full length as
tool-tip. Both, sequents and proof commands, can be shown in the display
below the tree (on single click) or in a separate window (on double or
shift-click).
'';
homepage = http://askra.de/software/prooftree;
platforms = stdenv.lib.platforms.unix;
maintainers = [ stdenv.lib.maintainers.jwiegley ];
};
})