ilyakooo0/nixpkgs
1
0
Fork 0
mirror of https://github.com/ilyakooo0/nixpkgs.git synced 2024-12-24 20:02:58 +03:00
Code Issues Projects Releases Wiki Activity

prooftree: new expression 0.12

Browse Source
This commit is contained in:
John Wiegley 2014-06-08 05:35:26 +00:00
parent 476a3d818f
commit c6261157f8
2 changed files with 45 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
pkgs/applications/science/logic/prooftree/default.nix Normal file
View File

@ -0,0 +1,40 @@
{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 = "Prooftree is 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 ];
};
})

5
pkgs/top-level/all-packages.nix
View File

@ -10617,6 +10617,11 @@ let
picosat = callPackage ../applications/science/logic/picosat {};
prooftree = callPackage ../applications/science/logic/prooftree {
inherit (ocamlPackages) findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
prover9 = callPackage ../applications/science/logic/prover9 { };
satallax = callPackage ../applications/science/logic/satallax {};