The Coq mailing list

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

Hi!

I'm having problems installing Coq in Ubuntu Linux:

"
$ ./configure
You have Objective-Caml 3.09.1. Good!
You have native-code compilation. Good!
LablGtk2 found, native threads: native CoqIde will be available
Where should I install the Coq binaries [/usr/local/bin] ?

Where should I install the Coq library [/usr/local/lib/coq] ?

Where should I install the Coq man pages [/usr/local/man] ?

Where should I install the Coq Emacs mode [/usr/share/emacs/site-lisp] ?

Where should I install Coqdoc TeX/LaTeX files
[/usr/share/texmf/tex/latex/misc] ?

Should I compile the complete theory of real analysis [Y/N, default is Y] ?


  Coq top directory                 : /home/joao/coq-8.0pl3
  Architecture                      : i686
  OS dependent libraries            : -cclib -lunix
  Objective-Caml/Camlp4 version     : 3.09.1
  Objective-Caml/Camlp4 binaries in : /usr/local/bin
  Objective-Caml library in         : /usr/local/lib/ocaml
  Camlp4 library in                 : +camlp4
  Reals theory                      : All
  CoqIde                            : opt

  Paths for true installation:
    binaries   will be copied in /usr/local/bin
    library    will be copied in /usr/local/lib/coq
    man pages  will be copied in /usr/local/man
    emacs mode will be copied in /usr/share/emacs/site-lisp

If anything in the above is wrong, please restart './configure'

*Warning* To compile the system for a new architecture
          don't forget to do a 'make archclean' before './configure'.


$ 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.

Please, can someone help me?

Thank you!


João