--------------------------
+ Coq package for Debian +
--------------------------

Binary (in)compatibility
------------------------
The compiled libraries of Coq (the *.vo) are not expected to be backward or
upward compatible between releases (including plX releases). In case of a new
upstream release, your Coq files should be recompiled.


Coq frontends
-------------
For interactive use of coqtop, we suggest
- either the Debian cle package
- or the Proof-General (x)emacs mode, which unfortunately can not be
distributed by Debian for copyright reasons. However, a Debian package
might become available at proof general home page in the future
(http://zermelo.dcs.ed.ac.uk/~proofgen)

However we recommand you to use the CoqIde gtk interface provided in coqide.


Unstripped binaries
-------------------

Note that all bytecode files in this package need to be left
'unstripped' after compiling. The reason is the following:

  It is possible to strip the .out corresponding to ocaml code compiled in
  native code (and it is done in Coq (coqopt.out) When compiling in
  byte-code, the Coq system uses the -custom option in order to get an
  autonomous executable (running independently of an ocaml implementation on
  your computer). The way it works is that the .out file is composed of the
  executable of the byte-code interpreter plus the byte-code for your own
  program which is stored in the symbol table zone...  stripping such an
  executable, just remove your byte-code and consequentely cannot run
  properly.

Moreover the bytecode version is installed even on platforms having a
native version as the dynamic loading of tactics works only with the
bytecode version.