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