The Coq mailing list

[Michael Ganem <michael.ganem AT gmail.com>]

Hi Stephane,

Good news. I managed to fully install the system in byte code mode (I 
did not try native compilation again) without the -local flag.
I follow the regular flow but just set as you suggested the env variable 
CAML_LD_LIBRARY_PATH to be the full path of kernel/byterun after running 
./configure -byte-only. The compilation then passes and I manage to 
install the system. I did no fully test the system but looks good so far.

Thanks!

Michael



On 01/10/2014 04:14 PM, Stéphane Glondu wrote:
> Le 07/01/2014 21:00, Michael Ganem a écrit :
> > Looks much better when adding -local and compiling in byte code. I think
> > that the compilation completes correctly:
> > OCAMLC    ide/coqide_ui.ml <http://coqide_ui.ml>
> > OCAMLC    ide/coqide.mli
> > OCAMLC    ide/coqide.ml <http://coqide.ml>
> > OCAMLC -a -o ide/ide.cma
> > OCAMLC -o bin/coqide.byte
> > cd bin && ln -sf coqide.byte coqide
> > make[1]: Leaving directory `/coq'
> >
> >
> > But now, I got a failure when running make install:
> You are not supposed to do "make install" with -local. Nor should you
> run it as root. Just directly run e.g. bin/coqtop. You might need to set
> CAML_LD_LIBRARY_PATH to the full path of the directory containing
> dllcoqrun.so (in kernel/byterun IIRC).
>
> PS: please avoid sending private replies and send them to the
> mailing-list so that everyone can enjoy them.
>
> Cheers,