forked from mirrors/nixpkgs
c9baba9212
(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.
41 lines
1.7 KiB
Nix
41 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 ];
|
|
};
|
|
})
|