diff options
| -rw-r--r-- | INSTALL | 32 | ||||
| -rw-r--r-- | INSTALL.ide | 123 |
2 files changed, 16 insertions, 139 deletions
@@ -1,6 +1,6 @@ - INSTALLATION PROCEDURES FOR THE COQ V8.8 SYSTEM - ----------------------------------------------- + INSTALLATION PROCEDURE + ---------------------- WHAT DO YOU NEED ? @@ -27,11 +27,14 @@ WHAT DO YOU NEED ? port install coq - To compile Coq V8.8 yourself, you need: + To compile Coq yourself, you need: - OCaml version 4.02.3 or later (available at https://ocaml.org/) + - The Num package, which used to be part of the OCaml standard library, + if you are using an OCaml version >= 4.06.0 + - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) @@ -42,20 +45,24 @@ WHAT DO YOU NEED ? - a C compiler - - for Coqide, the Lablgtk development files, and the GTK libraries - including gtksourceview, see INSTALL.ide for more details + - for CoqIDE, the lablgtk development files (version >= 2.18.3), + and the GTK 2.x libraries including gtksourceview2. - Note that camlp5 and lablgtk should be properly registered with + Note that num, camlp5 and lablgtk should be properly registered with findlib/ocamlfind as Coq's makefile will use it to locate the libraries during the build. - Opam (https://opam.ocaml.org/) is recommended to install ocaml and + Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam install ocamlfind camlp5 lablgtk-extras + $ opam install num ocamlfind camlp5 lablgtk conf-gtksourceview should get you a reasonable OCaml environment to compile Coq. + Nix users can also get all the required dependencies by running: + + $ nix-shell + Advanced users may want to experiment with the OCaml Flambda compiler as way to improve the performance of Coq. In order to profit from Flambda, a special build of the OCaml compiler that has @@ -76,7 +83,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler installed on your +1- Check that you have the OCaml compiler installed on your computer and that "ocamlc" (or, better, its native code version "ocamlc.opt") lies in a directory which is present in your $PATH environment variable. At the time of writing this sentence, all @@ -183,11 +190,6 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). make install Of course, you may need superuser rights to do that. - To use the Coq emacs mode you also need to put the following lines - in you .emacs file: - - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) 7- Optionally, you could build the bytecode version of Coq via: @@ -258,8 +260,6 @@ THE AVAILABLE COMMANDS. 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/getting-started - COMPILING FOR DIFFERENT ARCHITECTURES. ====================================== diff --git a/INSTALL.ide b/INSTALL.ide deleted file mode 100644 index c4da84048..000000000 --- a/INSTALL.ide +++ /dev/null @@ -1,123 +0,0 @@ - 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. - - -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. - - -COMPILATION REQUIREMENTS - -- OCaml >= 4.02.3 with native threads support. -- make world must succeed. -- The graphical toolkit GTK+ 2.x. See http://www.gtk.org. - The official supported version is at least 2.24.x. - You may still compile CoqIde with older versions and use all features. - Run - - pkg-config --modversion gtk+-2.0 - - to check your version. - Do not forget to install the development 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 GTK+ 2.x, lablgtk2 with support for gtksourceview2. - You need at least version 2.18.3. - - Your distribution may contain precompiled packages. For example, for - Debian, run - - aptitude install liblablgtksourceview2-ocaml-dev - - for Mandriva, run - - urpmi ocaml-lablgtk-devel - - If it does not, see http://lablgtk.forge.ocamlcore.org/ - - The basic command installing lablgtk2 from the source package is: - - ./configure && make world && make install - - You must have write access to the OCaml standard library path. - If this fails, read the README. - - -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) Go into your Coq source directory and, as usual, configure with: - - ./configure - - This should detect the ability of making CoqIde; check in the - report printed by configure that ability to build CoqIde is detected. - - 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 - -2) You may now run bin/coqide - - -NOTES - -There are three configuration files located in your $(XDG_CONFIG_HOME)/coq -dir (defaulting to $HOME/.config/coq). - -- 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.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. - - -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>/.config/coq/coqiderc under Linux, or - C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows) - and replace any occurrence of MOD4 by MOD1. - |