← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to INSTALL.ide

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
INSTALL.ide
 
1
                        CoqIde Installation procedure.
 
2
 
 
3
CoqIde is a graphical interface to perform interactive proofs.
 
4
You should be able to do everything you do in coqtop inside CoqIde 
 
5
excepted dropping to the ML toplevel.
 
6
 
 
7
DISCLAIMER: CoqIde is ongoing work. Although it should never let you
 
8
            loose a proof, you may encounter unexpected bugs.
 
9
            Do not hesitate to send suggestions/bug reports.
 
10
 
 
11
DISTRIBUTION PACKAGES
 
12
 
 
13
Your POSIX operating system may already contain precompiled packages
 
14
for Coq, including CoqIde, or a ready-to-compile... If the version
 
15
provided there suits you, follow the usual procedure for your
 
16
operating system.
 
17
 
 
18
E.g., on Debian GNU/Linux (or Debian GNU/k*BSD or ...), do:
 
19
   aptitude install coqide
 
20
On Gentoo GNU/Linux, do:
 
21
   USE=ide emerge sci-mathematics/coq
 
22
 
 
23
Else, read the rest of this document to compile your own CoqIde.
 
24
 
 
25
REQUIREMENT:
 
26
        - OCaml >= 3.07 with native threads support.
 
27
        - make world must succeed.
 
28
        - The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
 
29
          The official supported version is at least 2.8.x.
 
30
          You may still compile CoqIde with older versions and 
 
31
          use all features.
 
32
          Run 
 
33
                "pkg-config --modversion gtk+-2.0"
 
34
          to check your version.
 
35
          All recent distributions have precompiled packages.
 
36
          Do not forget to install the developement headers packages.
 
37
 
 
38
          On Debian, installing lablgtk2 (see below) will automatically
 
39
          install GTK+. (But "aptitude install libgtk2.0-dev" will
 
40
          install GTK+ 2.x should you need to force it for one reason
 
41
          or another.)
 
42
 
 
43
        - The OCaml bindings for GTK+ 2.x, lablgtk2.
 
44
 
 
45
          You need at least version 2.10.0.
 
46
 
 
47
          Your distribution may contain precompiled packages. For
 
48
          example, for Debian, run
 
49
                aptitude install liblablgtk2-ocaml-dev
 
50
                   for Mandriva, run
 
51
                urpmi ocaml-lablgtk2-devel
 
52
 
 
53
          If it does not, see
 
54
          http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html .
 
55
 
 
56
          One official releases of lablgtk2 is here:
 
57
          http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/dist/lablgtk-2.10.1.tar.gz
 
58
 
 
59
          Note that even if its README requires ocaml > 3.07, it works
 
60
          ok with 3.07. If you are in a hurry just run :
 
61
 
 
62
              cd /tmp && \
 
63
              wget \
 
64
               http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.1.tar.gz && \
 
65
              tar zxvf lablgtk-2.10.1.tar.gz && \
 
66
              cd lablgtk-2.10.1 && \
 
67
              ./configure && \
 
68
              make world && \
 
69
              make install
 
70
 
 
71
          You must have write access to the OCaml standard library path.
 
72
 
 
73
          If this fails, read lablgtk-2.10.1/README.
 
74
 
 
75
 
 
76
INSTALLATION
 
77
 0) For optimal performance, OCaml must support native threads (aka pthreads). 
 
78
    If this not the case, this means that Coq computations will be slow and 
 
79
    "make ide" will fail. Use "make bin/coqide.byte" instead. To fix this 
 
80
    problem, just recompile OCaml from source and configure OCaml with : 
 
81
        "./configure --with-pthreads". 
 
82
    In case you install over an existing copy of OCaml, you should better 
 
83
    empty the OCaml installation directory.
 
84
 
 
85
 1) Go into your Coq source directory and, as usual, configure with:
 
86
 
 
87
        ./configure
 
88
 
 
89
    This should detect the ability of making CoqIde; check that is
 
90
    says it has detected this ability and activated the building of
 
91
    CoqIde.
 
92
 
 
93
    Then compile with
 
94
 
 
95
        make world
 
96
 
 
97
    and install with
 
98
 
 
99
        make install
 
100
 
 
101
    In case you are upgrading from an old version you may need to run
 
102
        make clean-ide
 
103
 
 
104
3) You may now run bin/coqide
 
105
 
 
106
 
 
107
NOTES
 
108
There are three configuration files located in your $(HOME) dir. 
 
109
 You may need to set HOME to some sensible value under Windows.
 
110
 
 
111
- .coqiderc is generated by coqide itself. It may be edited by hand or 
 
112
  by using the Preference menu from coqide. It will be generated the first time
 
113
  you save your the preferences in Coqide.
 
114
 
 
115
- .coqide-gtk2rc is a standard Gtk2 configuration file. A sample file can be
 
116
  found in the coq lib "ide" subdir.
 
117
 
 
118
- .coqide.keys is a standard Gtk2 accelerator dump. You may edit this file 
 
119
  to change the default shortcuts for the menus.
 
120
 
 
121
Read ide/FAQ for more informations.
 
122
 
 
123
 
 
124
TROUBLESHOOTING
 
125
 
 
126
  - Problem with automatic templates
 
127
 
 
128
    Some users may experiment problems with unwanted automatic
 
129
    templates while using Coqide. This is due to a change in the
 
130
    modifiers keys available through GTK. The straightest way to get
 
131
    rid of the problem is to edit by hand your .coqiderc (either
 
132
    /home/<user>/.coqiderc under Linux, or 
 
133
    C:\Documents and Settings\<user>\.coqiderc under Windows) 
 
134
    and replace any occurence of MOD4 by MOD1.
 
135