diff options
Diffstat (limited to 'INSTALL.ide')
| -rw-r--r-- | INSTALL.ide | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/INSTALL.ide b/INSTALL.ide new file mode 100644 index 00000000..d8f1208b --- /dev/null +++ b/INSTALL.ide @@ -0,0 +1,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. |