The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

Hi,

I am trying to install the "Equations" plugin for Coq8.3pl2.

I've tried it on two machines, one with Ubuntu 10.10 + ocaml 3.11.2
and the other with Ubuntu 11.10 + ocaml 3.12.0.
I just followed the installation instruction by tapping

coq_makefile -f Make -o Makefile; make

But both trial ends with an error in a very short time. The following
is a copy of the whole process which is not long.

Any help will be appreciated.

Gyesik



=====

gslee@ubuntu:~/Coq-Equations$
 coq_makefile -f Make -o Makefile; make
Warning: install target will copy files at the first level of the coq
contributions installation directory; option -R is recommended
ocamlopt.opt -c -rectypes  -I src -I /home/gslee/coq-8.3pl2/kernel -I
/home/gslee/coq-8.3pl2/lib -I /home/gslee/coq-8.3pl2/library -I
/home/gslee/coq-8.3pl2/parsing -I /home/gslee/coq-8.3pl2/pretyping -I
/home/gslee/coq-8.3pl2/interp -I /home/gslee/coq-8.3pl2/proofs -I
/home/gslee/coq-8.3pl2/tactics -I /home/gslee/coq-8.3pl2/toplevel -I
/home/gslee/coq-8.3pl2/plugins/cc -I /home/gslee/coq-8.3pl2/plugins/dp
-I /home/gslee/coq-8.3pl2/plugins/extraction -I
/home/gslee/coq-8.3pl2/plugins/field -I
/home/gslee/coq-8.3pl2/plugins/firstorder -I
/home/gslee/coq-8.3pl2/plugins/fourier -I
/home/gslee/coq-8.3pl2/plugins/funind -I
/home/gslee/coq-8.3pl2/plugins/groebner -I
/home/gslee/coq-8.3pl2/plugins/interface -I
/home/gslee/coq-8.3pl2/plugins/micromega -I
/home/gslee/coq-8.3pl2/plugins/nsatz -I
/home/gslee/coq-8.3pl2/plugins/omega -I
/home/gslee/coq-8.3pl2/plugins/quote -I
/home/gslee/coq-8.3pl2/plugins/ring -I
/home/gslee/coq-8.3pl2/plugins/romega -I
/home/gslee/coq-8.3pl2/plugins/rtauto -I
/home/gslee/coq-8.3pl2/plugins/setoid_ring -I
/home/gslee/coq-8.3pl2/plugins/subtac -I
/home/gslee/coq-8.3pl2/plugins/subtac/test -I
/home/gslee/coq-8.3pl2/plugins/syntax -I
/home/gslee/coq-8.3pl2/plugins/xml -I /usr/lib/ocaml/camlp5 -pp
""camlp5"o -I /usr/lib/ocaml -I . -I /home/gslee/coq-8.3pl2/kernel -I
/home/gslee/coq-8.3pl2/lib -I /home/gslee/coq-8.3pl2/library -I
/home/gslee/coq-8.3pl2/parsing -I /home/gslee/coq-8.3pl2/pretyping -I
/home/gslee/coq-8.3pl2/interp -I /home/gslee/coq-8.3pl2/proofs -I
/home/gslee/coq-8.3pl2/tactics -I /home/gslee/coq-8.3pl2/toplevel -I
/home/gslee/coq-8.3pl2/plugins/cc -I /home/gslee/coq-8.3pl2/plugins/dp
-I /home/gslee/coq-8.3pl2/plugins/extraction -I
/home/gslee/coq-8.3pl2/plugins/field -I
/home/gslee/coq-8.3pl2/plugins/firstorder -I
/home/gslee/coq-8.3pl2/plugins/fourier -I
/home/gslee/coq-8.3pl2/plugins/funind -I
/home/gslee/coq-8.3pl2/plugins/groebner -I
/home/gslee/coq-8.3pl2/plugins/interface -I
/home/gslee/coq-8.3pl2/plugins/micromega -I
/home/gslee/coq-8.3pl2/plugins/nsatz -I
/home/gslee/coq-8.3pl2/plugins/omega -I
/home/gslee/coq-8.3pl2/plugins/quote -I
/home/gslee/coq-8.3pl2/plugins/ring -I
/home/gslee/coq-8.3pl2/plugins/romega -I
/home/gslee/coq-8.3pl2/plugins/rtauto -I
/home/gslee/coq-8.3pl2/plugins/setoid_ring -I
/home/gslee/coq-8.3pl2/plugins/subtac -I
/home/gslee/coq-8.3pl2/plugins/subtac/test -I
/home/gslee/coq-8.3pl2/plugins/syntax -I
/home/gslee/coq-8.3pl2/plugins/xml pa_extend.cmo pa_macro.cmo
q_MLast.cmo grammar.cma -loc loc -impl" src/equations_common.ml
ocamlopt.opt -c -rectypes  -I src -I /home/gslee/coq-8.3pl2/kernel -I
/home/gslee/coq-8.3pl2/lib -I /home/gslee/coq-8.3pl2/library -I
/home/gslee/coq-8.3pl2/parsing -I /home/gslee/coq-8.3pl2/pretyping -I
/home/gslee/coq-8.3pl2/interp -I /home/gslee/coq-8.3pl2/proofs -I
/home/gslee/coq-8.3pl2/tactics -I /home/gslee/coq-8.3pl2/toplevel -I
/home/gslee/coq-8.3pl2/plugins/cc -I /home/gslee/coq-8.3pl2/plugins/dp
-I /home/gslee/coq-8.3pl2/plugins/extraction -I
/home/gslee/coq-8.3pl2/plugins/field -I
/home/gslee/coq-8.3pl2/plugins/firstorder -I
/home/gslee/coq-8.3pl2/plugins/fourier -I
/home/gslee/coq-8.3pl2/plugins/funind -I
/home/gslee/coq-8.3pl2/plugins/groebner -I
/home/gslee/coq-8.3pl2/plugins/interface -I
/home/gslee/coq-8.3pl2/plugins/micromega -I
/home/gslee/coq-8.3pl2/plugins/nsatz -I
/home/gslee/coq-8.3pl2/plugins/omega -I
/home/gslee/coq-8.3pl2/plugins/quote -I
/home/gslee/coq-8.3pl2/plugins/ring -I
/home/gslee/coq-8.3pl2/plugins/romega -I
/home/gslee/coq-8.3pl2/plugins/rtauto -I
/home/gslee/coq-8.3pl2/plugins/setoid_ring -I
/home/gslee/coq-8.3pl2/plugins/subtac -I
/home/gslee/coq-8.3pl2/plugins/subtac/test -I
/home/gslee/coq-8.3pl2/plugins/syntax -I
/home/gslee/coq-8.3pl2/plugins/xml -I /usr/lib/ocaml/camlp5 -pp
""camlp5"o -I /usr/lib/ocaml -I . -I /home/gslee/coq-8.3pl2/kernel -I
/home/gslee/coq-8.3pl2/lib -I /home/gslee/coq-8.3pl2/library -I
/home/gslee/coq-8.3pl2/parsing -I /home/gslee/coq-8.3pl2/pretyping -I
/home/gslee/coq-8.3pl2/interp -I /home/gslee/coq-8.3pl2/proofs -I
/home/gslee/coq-8.3pl2/tactics -I /home/gslee/coq-8.3pl2/toplevel -I
/home/gslee/coq-8.3pl2/plugins/cc -I /home/gslee/coq-8.3pl2/plugins/dp
-I /home/gslee/coq-8.3pl2/plugins/extraction -I
/home/gslee/coq-8.3pl2/plugins/field -I
/home/gslee/coq-8.3pl2/plugins/firstorder -I
/home/gslee/coq-8.3pl2/plugins/fourier -I
/home/gslee/coq-8.3pl2/plugins/funind -I
/home/gslee/coq-8.3pl2/plugins/groebner -I
/home/gslee/coq-8.3pl2/plugins/interface -I
/home/gslee/coq-8.3pl2/plugins/micromega -I
/home/gslee/coq-8.3pl2/plugins/nsatz -I
/home/gslee/coq-8.3pl2/plugins/omega -I
/home/gslee/coq-8.3pl2/plugins/quote -I
/home/gslee/coq-8.3pl2/plugins/ring -I
/home/gslee/coq-8.3pl2/plugins/romega -I
/home/gslee/coq-8.3pl2/plugins/rtauto -I
/home/gslee/coq-8.3pl2/plugins/setoid_ring -I
/home/gslee/coq-8.3pl2/plugins/subtac -I
/home/gslee/coq-8.3pl2/plugins/subtac/test -I
/home/gslee/coq-8.3pl2/plugins/syntax -I
/home/gslee/coq-8.3pl2/plugins/xml pa_extend.cmo pa_macro.cmo
q_MLast.cmo grammar.cma -loc loc -impl" src/sigma.ml
File "src/sigma.ml", line 89, characters 2-165:
Error: Unbound record field label ci_cstr_ndecls
make: *** [src/sigma.cmx] Error 2
gslee@ubuntu:~/Coq-Equations$
 1

========