The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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.