Bug#736322: libcoq-ocaml-dev: It should depend on ocaml-best-compilers
Le 22/01/2014 10:49, Pierre Boutillier a écrit :
> please see https://coq.inria.fr/bugs/show_bug.cgi?id=3215
>
> Authors of plugins for coq are encouraged to use coq_makefile to generate their Makefile.
>
> Makefiles generated by coq_makefile ask coqtop for the ocaml compilers it has been compiled with in order to use it too. (It is done by "coqtop -config".)
foo@bar:~$ coqtop -v
The Coq Proof Assistant, version 8.4pl3 (January 2014)
compiled on Jan 19 2014 15:28:09 with OCaml 4.01.0
foo@bar:~$ coqtop -config
LOCAL=0
COQLIB=/usr/lib/coq/
DOCDIR=/usr/share/doc/coq/
OCAMLDEP=ocamldep
OCAMLC=ocamlc
OCAMLOPT=ocamlopt
OCAMLDOC=ocamldoc
CAMLBIN=/usr/bin/
CAMLLIB=/usr/lib/ocaml/
CAMLP4=camlp5
CAMLP4BIN=/usr/bin/
CAMLP4LIB=/usr/lib/ocaml/camlp5
HASNATDYNLINK=true
The *.opt variants do not appear here, and I don't remember having done
anything special for that. Maybe the reporter used a Makefile generated
elsewhere? In general, this is a bad idea since it could be run on an
architecture genuinely without the *.opt variants.
> Therefore, ocamlc.opt and ocamlopt.opt have to be available under platforms where coqtop has been compiled with them ...
It is the case on Debian. However, I wonder why the *.opt variants do
not appear above, then...
Cheers,
--
Stéphane
Reply to: