Getting prepared for the licensing-problems-free 8.0 release of COQ.

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.