diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-15 16:17:58 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-15 16:17:58 +0000 |
commit | 002fb17410892b80527927a559501b84560d804e (patch) | |
tree | 1b7f401f27f3b6d0a70f154036d138500f2b7d65 /debian/README.Debian | |
parent | 6b649aba925b6f7462da07599fe67ebb12a3460e (diff) |
Getting prepared for the licensing-problems-free 8.0 release of COQ.
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. |