The Coq mailing list

[Evgeny Makarov <emakarov AT gmail.com>]

Hello,

I am getting an error during installation of trunk 13238. The several
last commands in the output of "make VERBOSE=1" are the following:

cd kernel/byterun/ && \
        "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o 
coq_interp.o
"ranlib" kernel/byterun/libcoqrun.a
bin/coqmktop  -boot -opt -I config -I tools -I tools/coqdoc -I scripts
-I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I
pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I
plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote
-I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I
plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind
-I plugins/firstorder -I plugins/field -I plugins/subtac -I
plugins/rtauto -I plugins/nsatz -I plugins/syntax -I plugins/decl_mode
-I "+camlp5"    -o bin/coqtop.opt
No implementations provided for the following modules:
  Decl_mode referenced from plugins/xml/xml_plugin.cmxa(Dumptree)
  Ppdecl_proof referenced from plugins/xml/xml_plugin.cmxa(Dumptree)
make[1]: *** [bin/coqtop.opt] Error 2
make[1]: Leaving directory `/home/emakarov/coq/trunk'
make: *** [world] Error 2

I don't know much about installation, but it seems that the problem is
with dumptree.ml4 file, which references Decl_mode and Ppdecl_proof.
This file is first mentioned earlier in the output of make in the
following context:

echo "plugins/xml/dumptree.ml:  `sed -n -e 
's@^(\*.*camlp4deps:
"\(.*\)".*@\1@p'
 plugins/xml/dumptree.ml4`" >
"plugins/xml/dumptree.ml4.d" || (RV=$?; rm -f
"plugins/xml/dumptree.ml4.d"; exit ${RV})
\
        DEPS=`sed -n -e 
's@^(\*.*camlp4deps:
 
"\(.*\)".*@\1@p'
plugins/xml/dumptree.ml4`; \
        if ls ${DEPS} > /dev/null 2>&1; then \
        camlp5o pr_dump.cmo  -I "/usr/local/lib/ocaml" ${DEPS} pa_extend.cmo
q_MLast.cmo pa_macro.cmo -DOCAML310 -loc loc -impl
plugins/xml/dumptree.ml4 > "plugins/xml/dumptree.ml" || (RV=$?; rm -f
"plugins/xml/dumptree.ml"; exit ${RV}); \
        else echo plugins/xml/dumptree.ml4 : Dependency ${DEPS} not ready
yet; false; fi
plugins/xml/dumptree.ml4 : Dependency parsing/grammar.cma not ready yet

In the end, the file dumptree.ml4.d contains one line:
plugins/xml/dumptree.ml:  parsing/grammar.cma

Here is the output of configure:

> ./configure -local -opt

You have GNU Make 3.81. Good!
You have Objective-Caml 3.10.1. Good!
You have native-code compilation. Good!
LablGtk2 found, native threads: native CoqIde will be available.
pngtopnm was not found; documentation will not be available

  Coq top directory                 : /home/emakarov/coq/trunk
  Architecture                      : Linux
  Coq VM bytecode link flags        : -dllib -lcoqrun -dllpath
'/home/emakarov/coq/trunk'/kernel/byterun
  Coq tools bytecode link flags     :
  OS dependent libraries            : -cclib -lunix
  Objective-Caml/Camlp4 version     : 3.10.1
  Objective-Caml/Camlp4 binaries in : /usr/local/bin
  Objective-Caml library in         : /usr/local/lib/ocaml
  Camlp4 library in                 : +camlp5
  Native dynamic link support       : false
  Lablgtk2 library in               : +lablgtk2
  Documentation                     : None
  CoqIde                            : opt
  Web browser                       : firefox -remote
"OpenURL(%s,new-tab)" || firefox %s &
  Coq web site                      : http://coq.inria.fr/

I had installation problems before that were due to checking out Coq
SVN tree in Windows and then using it for installation under Linux
(apparently a problem with Windows/Unix line endings). However, this
time I believe I checked out the copy entirely under Linux. Also, my
versions of OCaml and Camlp5 may be old, but I am still using Ubuntu
8.04 (I'd like to clean it up and backup before installing the latest
10.04), and these are the latest versions provided in the repository.

Thanks for any help,
Evgeny