tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 pkg-config,
6 ncurses,
7 ocamlPackages,
8}:
9
10stdenv.mkDerivation rec {
11 pname = "prooftree";
12 version = "0.14";
13
14 src = fetchurl {
15 url = "https://askra.de/software/prooftree/releases/prooftree-${version}.tar.gz";
16 sha256 = "sha256-nekV2UnjibOk4h0jZ1jV7W5pE/hXWb3fUoLTJb3Jzc0=";
17 };
18
19 strictDeps = true;
20
21 nativeBuildInputs = [
22 pkg-config
23 ]
24 ++ (with ocamlPackages; [
25 ocaml
26 findlib
27 camlp5
28 ]);
29 buildInputs = [ ncurses ] ++ (with ocamlPackages; [ lablgtk ]);
30
31 prefixKey = "--prefix ";
32
33 meta = with lib; {
34 description = "Program for proof-tree visualization";
35 mainProgram = "prooftree";
36 longDescription = ''
37 Prooftree is a program for proof-tree visualization during interactive
38 proof development in a theorem prover. It is currently being developed
39 for Coq and Proof General. Prooftree helps against getting lost between
40 different subgoals in interactive proof development. It clearly shows
41 where the current subgoal comes from and thus helps in developing the
42 right plan for solving it.
43
44 Prooftree uses different colors for the already proven subgoals, the
45 current branch in the proof and the still open subgoals. Sequent texts
46 are not displayed in the proof tree itself, but they are shown as a
47 tool-tip when the mouse rests over a sequent symbol. Long proof commands
48 are abbreviated in the tree display, but show up in full length as
49 tool-tip. Both, sequents and proof commands, can be shown in the display
50 below the tree (on single click) or in a separate window (on double or
51 shift-click).
52 '';
53 homepage = "http://askra.de/software/prooftree";
54 platforms = platforms.unix;
55 maintainers = [ maintainers.jwiegley ];
56 license = licenses.gpl3;
57 };
58}