diff options
Diffstat (limited to 'debian/README.Debian')
-rw-r--r-- | debian/README.Debian | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/debian/README.Debian b/debian/README.Debian new file mode 100644 index 00000000..d91bc559 --- /dev/null +++ b/debian/README.Debian @@ -0,0 +1,42 @@ +-------------------------- ++ 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. |