-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathINSTALL
69 lines (47 loc) · 2.28 KB
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
============================================================================
PREREQUISITES
============================================================================
Make sure you have Proof General later than March 2021 and Coq 8.11 or
better.
If you want to install Prooftree from sources you need OCaml with the Gtk
bindings from the LablGtk2 library installed. The configure script checks
if
ocamlopt.opt -I +lablgtk2 lablgtk.cmxa gtkInit.cmx
runs without errors. For Debian, installing the packages ocaml-nox and
liblablgtk2-ocaml-dev suffice (but the package ocaml-native-compilers is
strongly recommended for binary compilation). For opam, package lablgtk
must be installed.
============================================================================
INSTALLATION
============================================================================
1. Configure with
./configure
optionally supply -prefix <dir> or -bindir <dir> to set the installation
directories. The configure script does trial-and-error to find LablGtk2.
You might therefore see spurious compilation errors. If the script is
successful, it prints "Configuration successful." together with a
summary.
2. Compile with
make all
3. This step only installs the man page and the executable. You can omit
this step and run the prooftree executable out of this directory. If you
want to install, acquire the necessary rights and install with
make install
============================================================================
EMACS CONFIGURATION
============================================================================
Before you can enjoy prooftree you have to configure Emacs to find
prooftree and use the right versions of Proof General and Coq. Of course
you have to disable any other setting that select a particular Proof
General or Coq version.
1. Prooftree is controlled by Proof General as a subprocess of Emacs. You
therefore have to make sure Emacs loads the right version of Proof
General. Put
(load-file "<pg-dir>/generic/proof-site.el")
in your .emacs, where <pg-dir> is the installation directory of your
version of Proof General.
============================================================================
Local Variables:
mode: indented-text
fill-column: 75
End: