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 -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
