The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Evgeny,

Did you "make clean" before compiling? The files implementing the
declarative mode (files decl_mode, ppdecl_proof, etc) are no longer in
the same directory and you need to be sure that no corresponding *.cm?
remain in the old directory to have the compilation going correctly.

Hugo

On Mon, Jul 05, 2010 at 08:39:47PM +0400, Evgeny Makarov wrote:
> 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