diff options
Diffstat (limited to 'INSTALL.ide')
| -rw-r--r-- | INSTALL.ide | 70 |
1 files changed, 47 insertions, 23 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index 365f59ee..fbb484fd 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -2,9 +2,9 @@ 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. +excepted dropping to the ML toplevel. -DISCLAIMER: CoqIde is ongoing work. Eventhough it should never let you +DISCLAIMER: CoqIde is ongoing work. Although it should never let you loose a proof, you may encounter unexpected bugs. Do not hesitate to send suggestions/bug reports. @@ -23,51 +23,58 @@ On Gentoo GNU/Linux, do: Else, read the rest of this document to compile your own CoqIde. REQUIREMENT: - - OCaml >= 3.07 with native thread support. + - OCaml >= 3.07 with native threads support. - make world must succeed. - - The graphical toolkit Gtk 2.x. See http://www.gtk.org. + - The graphical toolkit GTK+ 2.x. See http://www.gtk.org. The official supported version is at least 2.8.x. You may still compile CoqIde with older 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 development headers packages. - As for Debian or Ubuntu, - apt-get install libgtk2.0-dev - should be enough. + All recent distributions have precompiled packages. + Do not forget to install the developement headers packages. - - The OCaml bindings for for GTK+ 2.x, lablgtk2. + On Debian, installing lablgtk2 (see below) will automatically + install GTK+. (But "aptitude install libgtk2.0-dev" will + install GTK+ 2.x should you need to force it for one reason + or another.) + + - The OCaml bindings for GTK+ 2.x, lablgtk2. + + You need at least version 2.10.0. Your distribution may contain precompiled packages. For example, for Debian, run aptitude install liblablgtk2-ocaml-dev + for Mandriva, run + urpmi ocaml-lablgtk2-devel If it does not, see http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html . - The latest official release of lablftk2 is here: - http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.0.tar.gz + One official releases of lablgtk2 is here: + http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/dist/lablgtk-2.10.1.tar.gz Note that even if its README requires ocaml > 3.07, it works ok with 3.07. If you are in a hurry just run : cd /tmp && \ wget \ - http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.0.tar.gz && \ - tar zxvf lablgtk-2.10.0.tar.gz && \ - cd lablgtk-2.10.0 && \ + http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.1.tar.gz && \ + tar zxvf lablgtk-2.10.1.tar.gz && \ + cd lablgtk-2.10.1 && \ ./configure && \ make world && \ make install You must have write access to the OCaml standard library path. - If this fails, read lablgtk-2.10.0/README. + If this fails, read lablgtk-2.10.1/README. + INSTALLATION -0) For optimal performance, OCaml must support native threads (aka pthreads). + 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 : @@ -75,23 +82,26 @@ INSTALLATION In case you install over an existing copy of OCaml, you should better empty the OCaml installation directory. -1) Go into your Coq source directory and, as usual, configure with: + 1) Go into your Coq source directory and, as usual, configure with: ./configure - This should detect the ability of making CoqIde. - Then compile with + This should detect the ability of making CoqIde; check that is + says it has detected this ability and activated the building of + CoqIde. + + Then compile with make world - and install with + and install with make install - In case you are upgrading from an old version you may need to run + In case you are upgrading from an old version you may need to run make clean-ide -2) You may now run bin/coqide +3) You may now run bin/coqide NOTES @@ -109,3 +119,17 @@ There are three configuration files located in your $(HOME) dir. to change the default shortcuts for the menus. Read ide/FAQ for more informations. + + +TROUBLESHOOTING + + - Problem with automatic templates + + Some users may experiment problems with unwanted automatic + templates while using Coqide. This is due to a change in the + modifiers keys available through GTK. The straightest way to get + rid of the problem is to edit by hand your .coqiderc (either + /home/<user>/.coqiderc under Linux, or + C:\Documents and Settings\<user>\.coqiderc under Windows) + and replace any occurence of MOD4 by MOD1. + |