From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 INSTALL.ide | 88 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)
 create mode 100644 INSTALL.ide

(limited to 'INSTALL.ide')

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.
-- 
cgit v1.2.3