blob: d8f1208bf4725d9c5659c2fbe0cc90eaa0f78250 (
plain)
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
CoqIde Installation procedure.
CoqIde is a graphical interface to perform interactive proofs.
You should be able to do everything you do in coqtop inside CoqIde
excepted dropping to the ml toplevel.
DISCLAIMER: CoqIde is ongoing work. Eventhough it should never let you
loose a proof, you may encounter unexpected bugs.
Do not hesitate to send suggestions/bug reports.
REQUIREMENT:
- OCaml >= 3.06 with native thread support.
- make world must succeed.
- The graphical toolkit Gtk 2.x. See http://www.gtk.org.
The official supported version is at least 2.2.x.
You may still compile CoqIde with older 2.0.x versions and
use all features.
Run
"pkg-config --modversion gtk+-2.0"
to check your version.
All recent distributions have precompiled packages.
Do not forget to install the developement headers packages.
As for Debian/woody,
apt-get install libgtk2.0-dev
should be enough.
INSTALLATION
0) For optimal performance, OCaml must support native threads (aka pthreads).
If this not the case, this means that Coq computations will be slow and
"make ide" will fail. Use "make bin/coqide.byte" instead. To fix this
problem, just recompile OCaml from source and configure OCaml with :
"./configure --with-pthreads".
In case you install over an existing copy of OCaml, you should better
empty the OCaml installation directory.
1) You need to install the OCaml stub library lablgtk2. See
http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
The first official release of lablftk2 is here:
http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz
Note that even if its README requires ocaml > 3.07, it works ok with 3.06.
If you are in a hurry just run :
cd /tmp && \
wget \
http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz && \
tar zxvf lablgtk-2.2.0.tar.gz && \
cd lablgtk-2.2.0 && \
./configure && \
make world && \
make install
You must have write access to the OCaml standard library path.
If this fails read lablgtk-2.2.0/README.
2) Go into your Coq source directory and, as usual, configure with:
./configure
This should detect the ability of making CoqIde.
Then compile with
make world
and install with
make install
In case you are upgrading from an old version you may need to run
make clean-ide
3) You may now run bin/coqide
NOTES
There are three configuration files located in your $(HOME) dir.
You may need to set HOME to some sensible value under Windows.
- .coqiderc is generated by coqide itself. It may be edited by hand or
by using the Preference menu from coqide. It will be generated the first time
you save your the preferences in Coqide.
- .coqide-gtk2rc is a standard Gtk2 configuration file. A sample file can be
found in the coq lib "ide" subdir.
- .coqide.keys is a standard Gtk2 accelerator dump. You may edit this file
to change the default shortcuts for the menus.
Read ide/FAQ for more informations.
|
