diff options
| -rw-r--r-- | INSTALL | 46 | ||||
| -rw-r--r-- | INSTALL.ide | 96 | ||||
| -rw-r--r-- | INSTALL.macosx | 3 |
3 files changed, 104 insertions, 41 deletions
@@ -5,16 +5,44 @@ WHAT DO YOU NEED ? ================== - Coq is designed to work on computers equipped with the Unix operating - system. In order to compile Coq V8.1 you need: + Coq is designed to work on computers equipped with a POSIX (Unix or + a clone) operating system. It also works under Microsoft Windows + (see INSTALL.win); for a precompiled MacOS X package, see + INSTALL.macosx. + + Coq is known to be actively used under GNU/Linux (i386, amd64 and + ppc) and FreeBSD. Automated tests are run under many, many + different architectures under GNU/Linux. + + Naturally, Coq will run faster on an architecture where OCaml can + compile to native code, rather than only bytecode. At time of + writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, + HPPA and StrongArm. See + http://caml.inria.fr/ocaml/portability.en.html for details. + + + Your OS may already contain Coq under the form of a precompiled + package or ready-to-compile port. In this case, and if the supplied + version suits you, follow the usual procedure for your OS to + install it. E.g.: + + - Debian GNU/Linux (or Debian GNU/k*BSD or ...): + + aptitude install coq + + - Gentoo GNU/Linux: emerge sci-mathematics/coq + + + Should you need or prefer to compile Coq V8.1 yourself, you need: - Objective Caml version 3.07 or later (available at http://caml.inria.fr/) - Until now, it has mainly been tested on Sun workstations running Solaris, - DEC alpha and Pentium workstations running Linux. By FTP, Coq comes - as a single compressed tar-file. You have probably already - decompressed it if you are reading this document. + - a C compiler + + + By FTP, Coq comes as a single compressed tar-file. You have + probably already decompressed it if you are reading this document. QUICK INSTALLATION PROCEDURE. @@ -133,7 +161,7 @@ INSTALLATION PROCEDURE FOR ADVANCED USERS. ========================================== If you wish to write tactics (and that really means that you belong - to advanced users !) you *must* keep the Coq sources, without cleaning + to advanced users!) you *must* keep the Coq sources, without cleaning them. Therefore, to avoid a duplication of binaries and library, it is not necessary to do the installation step (6- above). You just have to tell it at configuration step (4- above) with the @@ -184,9 +212,11 @@ THE AVAILABLE COMMANDS. command "Require". A detailed description of these commands and of their options is given - in the Reference Manual (which you can get by FTP, in the doc/ directory) + in the Reference Manual (which you can get by FTP, in the doc/ + directory, or read online on http://coq.inria.fr/doc/) and in the corresponding manual pages. + There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html COMMON PROBLEMS. ================ diff --git a/INSTALL.ide b/INSTALL.ide index 0ca3d9e0a..d11ad646c 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -2,27 +2,73 @@ 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. +DISTRIBUTION PACKAGES + +Your POSIX operating system may already contain precompiled packages +for Coq, including CoqIde, or a ready-to-compile... If the version +provided there suits you, follow the usual procedure for your +operating system. + +E.g., on Debian GNU/Linux (or Debian GNU/k*BSD or ...), do: + aptitude install coqide +On Gentoo GNU/Linux, do: + USE=ide emerge sci-mathematics/coq + +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.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. + All recent distributions have precompiled packages. + Do not forget to install the developement headers packages. + + 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 for GTK+ 2.x, lablgtk2. + + Your distribution may contain precompiled packages. For + example, for Debian, run + aptitude install liblablgtk2-ocaml-dev + + If it does not, 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.07. 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. + INSTALLATION 0) For optimal performance, OCaml must support native threads (aka pthreads). @@ -33,39 +79,23 @@ INSTALLATION 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.07. - 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: + 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 3) You may now run bin/coqide diff --git a/INSTALL.macosx b/INSTALL.macosx index 70b0d4756..bf252ed81 100644 --- a/INSTALL.macosx +++ b/INSTALL.macosx @@ -1,6 +1,9 @@ INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X ------------------------------------------------------------------------ +You can also use fink, or the MacOS X package prepared by the Coq +team. To use the MacOS X package,: + 1) Download archive coq-8.1-macosx.dmg. 2) Double-click on its icon; it mounts a disk volume named "Coq V8.1". |