The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

Hi Yves,

Thank you for your response.

The output of the commands you requested:

Prayag:/usr/local/coq-8.2beta4 root# ls $(ocamlc -where)/camlp5/stdpp.*

/usr/local/ocaml-3.10.2/lib/camlp5/stdpp.cmi    /usr/local/ocaml-3.10.2/lib/camlp5/stdpp.mli

Prayag:/usr/local/coq-8.2beta4 root# 

For my installation here is what I do:

I type this:

Prayag:/usr/local/coq-8.2beta4 root# ./configure -camldir /usr/local/ocaml-3.10.2/bin -camlp5dir /usr/local/camlp5-5.10/main

and I get  the following:

You have GNU Make 3.81. Good!

You have Objective-Caml 3.10.2. Good!

LablGtk2 not found: CoqIde will not be available.

hevea was not found: documentation will not be available

Where should I install the Coq binaries [/usr/local/bin] ?

/usr/local/coq-8.2beta4/bin

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

/usr/local/coq-8.2beta4/lib

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

Where should I install the Coq documentation [/usr/local/share/doc] ?

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

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

  Coq top directory                 : /usr/local/coq-8.2beta4

  Architecture                      : i386

  OS dependent libraries            : -cclib -lunix

  Objective-Caml/Camlp4 version     : 3.10.2

  Objective-Caml/Camlp4 binaries in : /usr/local/ocaml-3.10.2/bin

  Objective-Caml library in         : /usr/local/ocaml-3.10.2/lib

  Camlp4 library in                 : /usr/local/camlp5-5.10/main

  FSets theory                      : All

  Reals theory                      : All

  Documentation                     : None

  CoqIde                            : no

  Web browser                       : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &

  Paths for true installation:

    binaries      will be copied in /usr/local/coq-8.2beta4/bin

    library       will be copied in /usr/local/coq-8.2beta4/lib

    man pages     will be copied in /usr/local/man

    documentation will be copied in /usr/local/man

    emacs mode    will be copied in /usr/local/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'.

Prayag:/usr/local/coq-8.2beta4 root# 

Prayag:/usr/local/coq-8.2beta4 root# ./configure  -camlp5dir /usr/local/camlp5-5.10/main

After this when I do make world I get

....

CAMLP4DEPS contrib/cc/g_congruence.ml4

rm contrib/xml/xml.ml tactics/tauto.ml tactics/class_tactics.ml parsing/g_prim.ml contrib/xml/proofTree2Xml.ml tools/coq_makefile.ml toplevel/whelp.ml contrib/romega/g_romega.ml parsing/g_ltac.ml contrib/cc/g_congruence.ml parsing/q_coqast.ml contrib/xml/xmlentries.ml lib/compat.ml parsing/q_constr.ml contrib/setoid_ring/newring.ml contrib/subtac/g_eterm.ml tactics/extraargs.ml contrib/subtac/g_subtac.ml parsing/g_decl_mode.ml contrib/interface/centaur.ml tools/coq-tex.ml contrib/omega/g_omega.ml contrib/rtauto/g_rtauto.ml parsing/vernacextend.ml contrib/micromega/g_micromega.ml contrib/field/field.ml contrib/ring/g_quote.ml tactics/hipattern.ml parsing/g_tactic.ml parsing/g_constr.ml contrib/interface/debug_tac.ml contrib/firstorder/g_ground.ml parsing/pcoq.ml parsing/tacextend.ml contrib/funind/g_indfun.ml contrib/extraction/g_extraction.ml parsing/g_xml.ml lib/pp.ml tactics/eauto.ml tactics/extratactics.ml parsing/g_vernac.ml contrib/interface/line_parser.ml parsing/argextend.ml parsing/lexer.ml parsing/q_util.ml toplevel/mltop.ml contrib/xml/acic2Xml.ml contrib/ring/g_ring.ml contrib/fourier/g_fourier.ml contrib/jprover/jprover.ml contrib/xml/dumptree.ml tactics/eqdecide.ml parsing/g_proofs.ml contrib/dp/g_dp.ml

make[1]: Leaving directory `/usr/local/coq-8.2beta4'

make[1]: Entering directory `/usr/local/coq-8.2beta4'

OCAMLC    config/coq_config.mli

OCAMLC    config/coq_config.ml

OCAMLC    lib/pp_control.mli

OCAMLC    lib/pp_control.ml

OCAMLC    lib/pp.mli

OCAMLC4   lib/pp.ml4

OCAMLC4   lib/compat.ml4

File "lib/compat.ml4", line 17, characters 11-25:

Unbound type constructor Stdpp.location

make[1]: *** [lib/compat.cmo] Error 2

make[1]: Leaving directory `/usr/local/coq-8.2beta4'

make: *** [stage1] Error 2