The Coq mailing list

[Jo�o Gomes <jg AT netvisao.pt>]

Sorry, I forgot to say that I had already found the solution.

You are right. It was the simple problem of bin directory did existed. :)

Thank you for your help!

João


Bruno Barras wrote:
João Gomes wrote:

>$ make world
>OCAMLC    config/coq_config.ml
>OCAMLC -o bin/coqmktop
>/usr/bin/ld: cannot open output file bin/coqmktop: Arquivo ou diretório
>não encontrado
>collect2: ld returned 1 exit status
>Error while building custom runtime system
>make: ** [bin/coqmktop] Erro 2
>"
>
>I can't understand what is going on.
>
>
>
Check that you have a (possibly empty) directory bin/ in coq-8.0pl3. If
not, create it and try again (some decompression tools might not create
empty dirs, which is nasty).
If it exists, check that it does not contain a write-protected coqmktop
file. Otherwise, you might have a serious installation problem with
either ocaml or gcc. Try running

LC_ALL=C make VERBOSE=1 CAMLDEBUG="-ccopt -###" bin/coqmktop

it may help spot at which stage compilation fails and why.
Hope this helps.

Bruno Barras.