aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.ide
diff options
context:
space:
mode:
authorGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-24 11:21:48 +0000
committerGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-24 11:21:48 +0000
commitcf706576978e52eff05df990adcbce63465549c0 (patch)
tree20237bd4fd9bd37bd5ee30299bf36c4bda8c55d5 /INSTALL.ide
parent5bb03931068aa9f453f74bdfe7f96219bda44d65 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3949 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL.ide')
-rw-r--r--INSTALL.ide12
1 files changed, 11 insertions, 1 deletions
diff --git a/INSTALL.ide b/INSTALL.ide
index f1144c694..7e08a2372 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -9,6 +9,7 @@ DISCLAIMER: CoqIde is ongoing work. Eventhough it should never let you
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.
@@ -24,9 +25,18 @@ REQUIREMENT:
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 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
- No current The latest CVS version is needed.
+ The latest CVS version is needed.
Use this one :
http://www.lri.fr/~monate/download/lablgtk2-coqide.tgz
If you are in a hurry just run :