blob: bb65ad1979571959d324f3e30e5c47d16a70866b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
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, provided in the proofgeneral-coq
Debian package.
|
