Full build log

build.log (text/plain), 29.64 KB, created by Jiri Svoboda on 2011-05-26 18:56:14 UTC

[32;01m * [39;49;00mPackage:    sci-mathematics/coq-8.3_p1
[32;01m * [39;49;00mRepository: gentoo
[32;01m * [39;49;00mMaintainer: [e-mail] [e-mail]
[32;01m * [39;49;00mUSE:        elibc_glibc kernel_linux ocamlopt userland_GNU x86
[32;01m * [39;49;00mFEATURES:   sandbox
>>> Unpacking source...
>>> Unpacking coq-8.3pl1.tar.gz to /var/tmp/portage/sci-mathematics/coq-8.3_p1/work
>>> Source unpacked in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work
>>> Preparing source in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1 ...
>>> Source prepared.
>>> Configuring source in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1 ...
You have GNU Make >= 3.81. Good!
You have Objective-Caml 3.11.2. Good!
You have native-code compilation. Good!
CoqIde disabled as requested.

  Coq top directory                 : /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1
  Architecture                      : i686
  Coq VM bytecode link flags        : -dllib -lcoqrun -dllpath '/usr/lib/coq'
  Coq tools bytecode link flags     : 
  OS dependent libraries            : -cclib -lunix
  Objective-Caml/Camlp4 version     : 3.11.2
  Objective-Caml/Camlp4 binaries in : /usr/bin
  Objective-Caml library in         : /usr/lib/ocaml
  Camlp4 library in                 : /usr/lib/ocaml/camlp5
  Native dynamic link support       : true
  Documentation                     : None
  CoqIde                            : no
  Web browser                       : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
  Coq web site                      : http://coq.inria.fr/

  Paths for true installation:
    binaries      will be copied in /usr/bin
    library       will be copied in /usr/lib/coq
    man pages     will be copied in /usr/share/man
    documentation will be copied in /usr/share/doc/coq-8.3_p1
    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'.
>>> Source configured.
>>> Compiling source in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1 ...
make -j5 STRIP=true -j1 
*****************************************************
*****************************************************
****************** Entering stage1 ******************
*****************************************************
*****************************************************
make --warn-undefined-variable --no-builtin-rules -f Makefile.stage1 "stage1"
make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'
sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
               -e '/^}/q' kernel/byterun/coq_instruct.h > \
                          kernel/byterun/coq_jumptbl.h \
	  || ( RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV} )
CCDEP     kernel/byterun/coq_fix_code.c
CCDEP     kernel/byterun/coq_interp.c
CCDEP     kernel/byterun/coq_memory.c
CCDEP     kernel/byterun/coq_values.c
OCAMLLEX  ide/highlight.mll
455 states, 31494 transitions, table size 128706 bytes
OCAMLLEX  ide/config_lexer.mll
13 states, 332 transitions, table size 1406 bytes
OCAMLLEX  ide/coq_lex.mll
457 states, 31161 transitions, table size 127386 bytes
OCAMLLEX  ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX  dev/ocamlweb-doc/lex.mll
99 states, 6415 transitions, table size 26254 bytes
OCAMLLEX  tools/gallina_lexer.mll
190 states, 498 transitions, table size 3132 bytes
OCAMLLEX  tools/coqdoc/cpretty.mll
2130 states, 6466 transitions, table size 38644 bytes
OCAMLLEX  tools/coqdep_lexer.mll
200 states, 5470 transitions, table size 23080 bytes
2243 additional bytes used for bindings
OCAMLLEX  tools/coqwc.mll
230 states, 833 transitions, table size 4712 bytes
OCAMLLEX  plugins/dp/dp_zenon.mll
85 states, 637 transitions, table size 3058 bytes
1881 additional bytes used for bindings
OCAMLYACC ide/config_parser.mly
OCAMLYACC dev/ocamlweb-doc/syntax.mly
3 shift/reduce conflicts.
ECHO... > scripts/tolink.ml
sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' \
	kernel/byterun/coq_instruct.h | \
	awk -f kernel/make-opcodes > kernel/copcodes.ml \
	|| ( RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV} )
"ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > theories/Numbers/Natural/BigN/NMake_gen.v
TOUCH     tactics/extratactics.ml
TOUCH     tactics/hipattern.ml
TOUCH     tactics/extraargs.ml
TOUCH     tactics/rewrite.ml
TOUCH     tactics/tauto.ml
TOUCH     tactics/class_tactics.ml
TOUCH     tactics/eqdecide.ml
TOUCH     tactics/eauto.ml
TOUCH     toplevel/mltop.ml
TOUCH     toplevel/whelp.ml
TOUCH     parsing/g_vernac.ml
TOUCH     parsing/g_proofs.ml
TOUCH     parsing/g_tactic.ml
TOUCH     parsing/g_prim.ml
TOUCH     parsing/q_constr.ml
TOUCH     parsing/lexer.ml
TOUCH     parsing/g_decl_mode.ml
TOUCH     parsing/tacextend.ml
TOUCH     parsing/q_util.ml
TOUCH     parsing/argextend.ml
TOUCH     parsing/q_coqast.ml
TOUCH     parsing/pcoq.ml
TOUCH     parsing/g_xml.ml
TOUCH     parsing/vernacextend.ml
TOUCH     parsing/g_constr.ml
TOUCH     parsing/g_ltac.ml
TOUCH     tools/coq_makefile.ml
TOUCH     tools/coq_tex.ml
TOUCH     lib/refutpat.ml
TOUCH     lib/compat.ml
TOUCH     lib/pp.ml
TOUCH     plugins/ring/g_ring.ml
TOUCH     plugins/firstorder/g_ground.ml
TOUCH     plugins/omega/g_omega.ml
TOUCH     plugins/dp/g_dp.ml
TOUCH     plugins/extraction/g_extraction.ml
TOUCH     plugins/quote/g_quote.ml
TOUCH     plugins/field/field.ml
TOUCH     plugins/micromega/g_micromega.ml
TOUCH     plugins/setoid_ring/newring.ml
TOUCH     plugins/rtauto/g_rtauto.ml
TOUCH     plugins/xml/dumptree.ml
TOUCH     plugins/xml/xmlentries.ml
TOUCH     plugins/xml/xml.ml
TOUCH     plugins/xml/acic2Xml.ml
TOUCH     plugins/xml/proofTree2Xml.ml
TOUCH     plugins/subtac/g_subtac.ml
TOUCH     plugins/romega/g_romega.ml
TOUCH     plugins/fourier/g_fourier.ml
TOUCH     plugins/nsatz/nsatz.ml
TOUCH     plugins/cc/g_congruence.ml
TOUCH     plugins/funind/g_indfun.ml
CAMLP4DEPS parsing/q_constr.ml4
OCAMLDEP4 parsing/q_constr.ml4
CAMLP4DEPS parsing/q_coqast.ml4
OCAMLDEP4 parsing/q_coqast.ml4
CAMLP4DEPS parsing/lexer.ml4
OCAMLDEP4 parsing/lexer.ml4
CAMLP4DEPS parsing/g_constr.ml4
OCAMLDEP4 parsing/g_constr.ml4
CAMLP4DEPS parsing/g_ltac.ml4
OCAMLDEP4 parsing/g_ltac.ml4
CAMLP4DEPS parsing/g_tactic.ml4
OCAMLDEP4 parsing/g_tactic.ml4
CAMLP4DEPS parsing/g_prim.ml4
OCAMLDEP4 parsing/g_prim.ml4
CAMLP4DEPS parsing/vernacextend.ml4
OCAMLDEP4 parsing/vernacextend.ml4
CAMLP4DEPS parsing/tacextend.ml4
OCAMLDEP4 parsing/tacextend.ml4
CAMLP4DEPS parsing/argextend.ml4
OCAMLDEP4 parsing/argextend.ml4
CAMLP4DEPS parsing/pcoq.ml4
OCAMLDEP4 parsing/pcoq.ml4
CAMLP4DEPS parsing/q_util.ml4
OCAMLDEP4 parsing/q_util.ml4
CAMLP4DEPS lib/pp.ml4
OCAMLDEP4 lib/pp.ml4
CAMLP4DEPS lib/compat.ml4
OCAMLDEP4 lib/compat.ml4
OCAMLDEP  dev/ocamlweb-doc/syntax.mli
OCAMLDEP  ide/config_parser.mli
OCAMLDEP  kernel/indtypes.mli
OCAMLDEP  kernel/pre_env.mli
OCAMLDEP  kernel/univ.mli
OCAMLDEP  kernel/environ.mli
OCAMLDEP  kernel/names.mli
OCAMLDEP  kernel/cbytecodes.mli
OCAMLDEP  kernel/mod_typing.mli
OCAMLDEP  kernel/modops.mli
OCAMLDEP  kernel/vconv.mli
OCAMLDEP  kernel/vm.mli
OCAMLDEP  kernel/safe_typing.mli
OCAMLDEP  kernel/subtyping.mli
OCAMLDEP  kernel/esubst.mli
OCAMLDEP  kernel/cooking.mli
OCAMLDEP  kernel/cemitcodes.mli
OCAMLDEP  kernel/cbytegen.mli
OCAMLDEP  kernel/reduction.mli
OCAMLDEP  kernel/declarations.mli
OCAMLDEP  kernel/retroknowledge.mli
OCAMLDEP  kernel/term.mli
OCAMLDEP  kernel/typeops.mli
OCAMLDEP  kernel/entries.mli
OCAMLDEP  kernel/conv_oracle.mli
OCAMLDEP  kernel/closure.mli
OCAMLDEP  kernel/sign.mli
OCAMLDEP  kernel/term_typing.mli
OCAMLDEP  kernel/type_errors.mli
OCAMLDEP  kernel/inductive.mli
OCAMLDEP  kernel/csymtable.mli
OCAMLDEP  kernel/mod_subst.mli
OCAMLDEP  plugins/funind/rawtermops.mli
OCAMLDEP  plugins/funind/indfun_common.mli
OCAMLDEP  plugins/funind/functional_principles_proofs.mli
OCAMLDEP  plugins/funind/functional_principles_types.mli
OCAMLDEP  plugins/funind/rawterm_to_relation.mli
OCAMLDEP  plugins/cc/ccalgo.mli
OCAMLDEP  plugins/cc/ccproof.mli
OCAMLDEP  plugins/cc/cctac.mli
OCAMLDEP  plugins/nsatz/polynom.mli
OCAMLDEP  plugins/nsatz/utile.mli
OCAMLDEP  plugins/romega/const_omega.mli
OCAMLDEP  plugins/subtac/subtac_classes.mli
OCAMLDEP  plugins/subtac/subtac_coercion.mli
OCAMLDEP  plugins/subtac/subtac.mli
OCAMLDEP  plugins/subtac/subtac_command.mli
OCAMLDEP  plugins/subtac/subtac_cases.mli
OCAMLDEP  plugins/subtac/eterm.mli
OCAMLDEP  plugins/subtac/subtac_utils.mli
OCAMLDEP  plugins/subtac/subtac_obligations.mli
OCAMLDEP  plugins/subtac/subtac_errors.mli
OCAMLDEP  plugins/subtac/subtac_pretyping.mli
OCAMLDEP  plugins/xml/xml.mli
OCAMLDEP  plugins/xml/unshare.mli
OCAMLDEP  plugins/xml/doubleTypeInference.mli
OCAMLDEP  plugins/xml/xmlcommand.mli
OCAMLDEP  plugins/rtauto/proof_search.mli
OCAMLDEP  plugins/rtauto/refl_tauto.mli
OCAMLDEP  plugins/micromega/sos.mli
OCAMLDEP  plugins/micromega/micromega.mli
OCAMLDEP  plugins/extraction/extraction.mli
OCAMLDEP  plugins/extraction/modutil.mli
OCAMLDEP  plugins/extraction/extract_env.mli
OCAMLDEP  plugins/extraction/miniml.mli
OCAMLDEP  plugins/extraction/common.mli
OCAMLDEP  plugins/extraction/table.mli
OCAMLDEP  plugins/extraction/mlutil.mli
OCAMLDEP  plugins/extraction/ocaml.mli
OCAMLDEP  plugins/extraction/haskell.mli
OCAMLDEP  plugins/extraction/scheme.mli
OCAMLDEP  plugins/dp/fol.mli
OCAMLDEP  plugins/dp/dp_zenon.mli
OCAMLDEP  plugins/dp/dp_why.mli
OCAMLDEP  plugins/dp/dp.mli
OCAMLDEP  plugins/firstorder/rules.mli
OCAMLDEP  plugins/firstorder/formula.mli
OCAMLDEP  plugins/firstorder/instances.mli
OCAMLDEP  plugins/firstorder/ground.mli
OCAMLDEP  plugins/firstorder/sequent.mli
OCAMLDEP  plugins/firstorder/unify.mli
OCAMLDEP  library/nametab.mli
OCAMLDEP  library/impargs.mli
OCAMLDEP  library/goptions.mli
OCAMLDEP  library/decl_kinds.mli
OCAMLDEP  library/library.mli
OCAMLDEP  library/libobject.mli
OCAMLDEP  library/declaremods.mli
OCAMLDEP  library/summary.mli
OCAMLDEP  library/decls.mli
OCAMLDEP  library/global.mli
OCAMLDEP  library/dischargedhypsmap.mli
OCAMLDEP  library/libnames.mli
OCAMLDEP  library/lib.mli
OCAMLDEP  library/declare.mli
OCAMLDEP  library/nameops.mli
OCAMLDEP  library/states.mli
OCAMLDEP  library/heads.mli
OCAMLDEP  checker/indtypes.mli
OCAMLDEP  checker/environ.mli
OCAMLDEP  checker/modops.mli
OCAMLDEP  checker/safe_typing.mli
OCAMLDEP  checker/subtyping.mli
OCAMLDEP  checker/reduction.mli
OCAMLDEP  checker/check_stat.mli
OCAMLDEP  checker/declarations.mli
OCAMLDEP  checker/term.mli
OCAMLDEP  checker/typeops.mli
OCAMLDEP  checker/closure.mli
OCAMLDEP  checker/type_errors.mli
OCAMLDEP  checker/inductive.mli
OCAMLDEP  pretyping/unification.mli
OCAMLDEP  pretyping/retyping.mli
OCAMLDEP  pretyping/recordops.mli
OCAMLDEP  pretyping/cases.mli
OCAMLDEP  pretyping/indrec.mli
OCAMLDEP  pretyping/termops.mli
OCAMLDEP  pretyping/typing.mli
OCAMLDEP  pretyping/pretype_errors.mli
OCAMLDEP  pretyping/coercion.mli
OCAMLDEP  pretyping/inductiveops.mli
OCAMLDEP  pretyping/vnorm.mli
OCAMLDEP  pretyping/typeclasses.mli
OCAMLDEP  pretyping/pattern.mli
OCAMLDEP  pretyping/classops.mli
OCAMLDEP  pretyping/rawterm.mli
OCAMLDEP  pretyping/tacred.mli
OCAMLDEP  pretyping/clenv.mli
OCAMLDEP  pretyping/reductionops.mli
OCAMLDEP  pretyping/typeclasses_errors.mli
OCAMLDEP  pretyping/evd.mli
OCAMLDEP  pretyping/cbv.mli
OCAMLDEP  pretyping/detyping.mli
OCAMLDEP  pretyping/namegen.mli
OCAMLDEP  pretyping/pretyping.mli
OCAMLDEP  pretyping/evarconv.mli
OCAMLDEP  pretyping/evarutil.mli
OCAMLDEP  pretyping/term_dnet.mli
OCAMLDEP  pretyping/matching.mli
OCAMLDEP  lib/flags.mli
OCAMLDEP  lib/heap.mli
OCAMLDEP  lib/bstack.mli
OCAMLDEP  lib/system.mli
OCAMLDEP  lib/pp.mli
OCAMLDEP  lib/dnet.mli
OCAMLDEP  lib/bigint.mli
OCAMLDEP  lib/util.mli
OCAMLDEP  lib/hashcons.mli
OCAMLDEP  lib/rtree.mli
OCAMLDEP  lib/gmapl.mli
OCAMLDEP  lib/tlm.mli
OCAMLDEP  lib/segmenttree.mli
OCAMLDEP  lib/pp_control.mli
OCAMLDEP  lib/predicate.mli
OCAMLDEP  lib/gmap.mli
OCAMLDEP  lib/dyn.mli
OCAMLDEP  lib/explore.mli
OCAMLDEP  lib/fmap.mli
OCAMLDEP  lib/gset.mli
OCAMLDEP  lib/profile.mli
OCAMLDEP  lib/fset.mli
OCAMLDEP  lib/tries.mli
OCAMLDEP  lib/envars.mli
OCAMLDEP  lib/option.mli
OCAMLDEP  lib/edit.mli
OCAMLDEP  tools/coqdoc/cpretty.mli
OCAMLDEP  tools/coqdoc/index.mli
OCAMLDEP  tools/coqdoc/output.mli
OCAMLDEP  tools/coqdoc/alpha.mli
OCAMLDEP  tools/coqdoc/tokens.mli
OCAMLDEP  proofs/tactic_debug.mli
OCAMLDEP  proofs/proof_trees.mli
OCAMLDEP  proofs/decl_expr.mli
OCAMLDEP  proofs/tacmach.mli
OCAMLDEP  proofs/logic.mli
OCAMLDEP  proofs/pfedit.mli
OCAMLDEP  proofs/clenvtac.mli
OCAMLDEP  proofs/proof_type.mli
OCAMLDEP  proofs/decl_mode.mli
OCAMLDEP  proofs/evar_refiner.mli
OCAMLDEP  proofs/refiner.mli
OCAMLDEP  proofs/redexpr.mli
OCAMLDEP  parsing/pcoq.mli
OCAMLDEP  parsing/printmod.mli
OCAMLDEP  parsing/ppconstr.mli
OCAMLDEP  parsing/tactic_printer.mli
OCAMLDEP  parsing/lexer.mli
OCAMLDEP  parsing/pptactic.mli
OCAMLDEP  parsing/g_natsyntax.mli
OCAMLDEP  parsing/g_intsyntax.mli
OCAMLDEP  parsing/ppvernac.mli
OCAMLDEP  parsing/egrammar.mli
OCAMLDEP  parsing/printer.mli
OCAMLDEP  parsing/extrawit.mli
OCAMLDEP  parsing/q_util.mli
OCAMLDEP  parsing/prettyp.mli
OCAMLDEP  parsing/g_zsyntax.mli
OCAMLDEP  parsing/extend.mli
OCAMLDEP  parsing/ppdecl_proof.mli
OCAMLDEP  toplevel/cerrors.mli
OCAMLDEP  toplevel/autoinstance.mli
OCAMLDEP  toplevel/indschemes.mli
OCAMLDEP  toplevel/usage.mli
OCAMLDEP  toplevel/classes.mli
OCAMLDEP  toplevel/mltop.mli
OCAMLDEP  toplevel/auto_ind_decl.mli
OCAMLDEP  toplevel/command.mli
OCAMLDEP  toplevel/whelp.mli
OCAMLDEP  toplevel/vernacentries.mli
OCAMLDEP  toplevel/discharge.mli
OCAMLDEP  toplevel/ind_tables.mli
OCAMLDEP  toplevel/vernacinterp.mli
OCAMLDEP  toplevel/himsg.mli
OCAMLDEP  toplevel/vernac.mli
OCAMLDEP  toplevel/toplevel.mli
OCAMLDEP  toplevel/lemmas.mli
OCAMLDEP  toplevel/coqinit.mli
OCAMLDEP  toplevel/metasyntax.mli
OCAMLDEP  toplevel/libtypes.mli
OCAMLDEP  toplevel/search.mli
OCAMLDEP  toplevel/class.mli
OCAMLDEP  toplevel/record.mli
OCAMLDEP  toplevel/coqtop.mli
OCAMLDEP  interp/constrintern.mli
OCAMLDEP  interp/coqlib.mli
OCAMLDEP  interp/topconstr.mli
OCAMLDEP  interp/constrextern.mli
OCAMLDEP  interp/implicit_quantifiers.mli
OCAMLDEP  interp/smartlocate.mli
OCAMLDEP  interp/reserve.mli
OCAMLDEP  interp/syntax_def.mli
OCAMLDEP  interp/modintern.mli
OCAMLDEP  interp/notation.mli
OCAMLDEP  interp/dumpglob.mli
OCAMLDEP  interp/ppextend.mli
OCAMLDEP  interp/genarg.mli
OCAMLDEP  ide/preferences.mli
OCAMLDEP  ide/undo_lablgtk_ge26.mli
OCAMLDEP  ide/utils/configwin.mli
OCAMLDEP  ide/utils/okey.mli
OCAMLDEP  ide/utils/config_file.mli
OCAMLDEP  ide/undo_lablgtk_ge212.mli
OCAMLDEP  ide/command_windows.mli
OCAMLDEP  ide/undo_lablgtk_lt26.mli
OCAMLDEP  ide/coq_tactics.mli
OCAMLDEP  ide/ideutils.mli
OCAMLDEP  ide/coqide.mli
OCAMLDEP  ide/coq.mli
OCAMLDEP  config/coq_config.mli
OCAMLDEP  tactics/tactic_option.mli
OCAMLDEP  tactics/decl_proof_instr.mli
OCAMLDEP  tactics/tacinterp.mli
OCAMLDEP  tactics/decl_interp.mli
OCAMLDEP  tactics/dhyp.mli
OCAMLDEP  tactics/dn.mli
OCAMLDEP  tactics/termdn.mli
OCAMLDEP  tactics/evar_tactics.mli
OCAMLDEP  tactics/tacticals.mli
OCAMLDEP  tactics/contradiction.mli
OCAMLDEP  tactics/eauto.mli
OCAMLDEP  tactics/tactics.mli
OCAMLDEP  tactics/equality.mli
OCAMLDEP  tactics/refine.mli
OCAMLDEP  tactics/elimschemes.mli
OCAMLDEP  tactics/extratactics.mli
OCAMLDEP  tactics/extraargs.mli
OCAMLDEP  tactics/autorewrite.mli
OCAMLDEP  tactics/leminv.mli
OCAMLDEP  tactics/nbtermdn.mli
OCAMLDEP  tactics/btermdn.mli
OCAMLDEP  tactics/auto.mli
OCAMLDEP  tactics/hipattern.mli
OCAMLDEP  tactics/elim.mli
OCAMLDEP  tactics/inv.mli
OCAMLDEP  tactics/hiddentac.mli
OCAMLDEP  tactics/eqschemes.mli
OCAMLDEP  kernel/copcodes.ml
OCAMLDEP  scripts/tolink.ml
OCAMLDEP  dev/ocamlweb-doc/syntax.ml
OCAMLDEP  ide/config_parser.ml
OCAMLDEP  plugins/dp/dp_zenon.ml
OCAMLDEP  tools/coqwc.ml
OCAMLDEP  tools/coqdep_lexer.ml
OCAMLDEP  tools/coqdoc/cpretty.ml
OCAMLDEP  tools/gallina_lexer.ml
OCAMLDEP  dev/ocamlweb-doc/lex.ml
OCAMLDEP  ide/utf8_convert.ml
OCAMLDEP  ide/coq_lex.ml
OCAMLDEP  ide/config_lexer.ml
OCAMLDEP  ide/highlight.ml
OCAMLDEP  scripts/coqmktop.ml
OCAMLDEP  scripts/coqc.ml
OCAMLDEP  kernel/reduction.ml
OCAMLDEP  kernel/environ.ml
OCAMLDEP  kernel/closure.ml
OCAMLDEP  kernel/univ.ml
OCAMLDEP  kernel/declarations.ml
OCAMLDEP  kernel/cbytecodes.ml
OCAMLDEP  kernel/cooking.ml
OCAMLDEP  kernel/term.ml
OCAMLDEP  kernel/mod_subst.ml
OCAMLDEP  kernel/pre_env.ml
OCAMLDEP  kernel/cemitcodes.ml
OCAMLDEP  kernel/conv_oracle.ml
OCAMLDEP  kernel/esubst.ml
OCAMLDEP  kernel/type_errors.ml
OCAMLDEP  kernel/safe_typing.ml
OCAMLDEP  kernel/retroknowledge.ml
OCAMLDEP  kernel/indtypes.ml
OCAMLDEP  kernel/sign.ml
OCAMLDEP  kernel/entries.ml
OCAMLDEP  kernel/cbytegen.ml
OCAMLDEP  kernel/term_typing.ml
OCAMLDEP  kernel/vconv.ml
OCAMLDEP  kernel/names.ml
OCAMLDEP  kernel/csymtable.ml
OCAMLDEP  kernel/mod_typing.ml
OCAMLDEP  kernel/typeops.ml
OCAMLDEP  kernel/inductive.ml
OCAMLDEP  kernel/subtyping.ml
OCAMLDEP  kernel/vm.ml
OCAMLDEP  kernel/modops.ml
OCAMLDEP  plugins/funind/merge.ml
OCAMLDEP  plugins/funind/recdef.ml
OCAMLDEP  plugins/funind/functional_principles_proofs.ml
OCAMLDEP  plugins/funind/functional_principles_types.ml
OCAMLDEP  plugins/funind/rawterm_to_relation.ml
OCAMLDEP  plugins/funind/indfun_common.ml
OCAMLDEP  plugins/funind/invfun.ml
OCAMLDEP  plugins/funind/rawtermops.ml
OCAMLDEP  plugins/funind/indfun.ml
OCAMLDEP  plugins/cc/cctac.ml
OCAMLDEP  plugins/cc/ccproof.ml
OCAMLDEP  plugins/cc/ccalgo.ml
OCAMLDEP  plugins/nsatz/polynom.ml
OCAMLDEP  plugins/nsatz/utile.ml
OCAMLDEP  plugins/nsatz/ideal.ml
OCAMLDEP  plugins/fourier/fourier.ml
OCAMLDEP  plugins/fourier/fourierR.ml
OCAMLDEP  plugins/romega/refl_omega.ml
OCAMLDEP  plugins/romega/const_omega.ml
OCAMLDEP  plugins/subtac/subtac_command.ml
OCAMLDEP  plugins/subtac/subtac_pretyping_F.ml
OCAMLDEP  plugins/subtac/subtac_cases.ml
OCAMLDEP  plugins/subtac/subtac.ml
OCAMLDEP  plugins/subtac/subtac_coercion.ml
OCAMLDEP  plugins/subtac/subtac_classes.ml
OCAMLDEP  plugins/subtac/subtac_obligations.ml
OCAMLDEP  plugins/subtac/subtac_utils.ml
OCAMLDEP  plugins/subtac/eterm.ml
OCAMLDEP  plugins/subtac/subtac_errors.ml
OCAMLDEP  plugins/subtac/subtac_pretyping.ml
OCAMLDEP  plugins/xml/cic2acic.ml
OCAMLDEP  plugins/xml/acic.ml
OCAMLDEP  plugins/xml/doubleTypeInference.ml
OCAMLDEP  plugins/xml/proof2aproof.ml
OCAMLDEP  plugins/xml/unshare.ml
OCAMLDEP  plugins/xml/cic2Xml.ml
OCAMLDEP  plugins/xml/xmlcommand.ml
OCAMLDEP  plugins/rtauto/refl_tauto.ml
OCAMLDEP  plugins/rtauto/proof_search.ml
OCAMLDEP  plugins/syntax/ascii_syntax.ml
OCAMLDEP  plugins/syntax/nat_syntax.ml
OCAMLDEP  plugins/syntax/string_syntax.ml
OCAMLDEP  plugins/syntax/numbers_syntax.ml
OCAMLDEP  plugins/syntax/r_syntax.ml
OCAMLDEP  plugins/syntax/z_syntax.ml
OCAMLDEP  plugins/micromega/micromega.ml
OCAMLDEP  plugins/micromega/sos.ml
OCAMLDEP  plugins/micromega/sos_lib.ml
OCAMLDEP  plugins/micromega/mfourier.ml
OCAMLDEP  plugins/micromega/sos_types.ml
OCAMLDEP  plugins/micromega/coq_micromega.ml
OCAMLDEP  plugins/micromega/mutils.ml
OCAMLDEP  plugins/micromega/certificate.ml
OCAMLDEP  plugins/micromega/persistent_cache.ml
OCAMLDEP  plugins/micromega/csdpcert.ml
OCAMLDEP  plugins/quote/quote.ml
OCAMLDEP  plugins/extraction/modutil.ml
OCAMLDEP  plugins/extraction/table.ml
OCAMLDEP  plugins/extraction/haskell.ml
OCAMLDEP  plugins/extraction/ocaml.ml
OCAMLDEP  plugins/extraction/extract_env.ml
OCAMLDEP  plugins/extraction/mlutil.ml
OCAMLDEP  plugins/extraction/scheme.ml
OCAMLDEP  plugins/extraction/big.ml
OCAMLDEP  plugins/extraction/common.ml
OCAMLDEP  plugins/extraction/extraction.ml
OCAMLDEP  plugins/dp/dp.ml
OCAMLDEP  plugins/dp/dp_why.ml
OCAMLDEP  plugins/omega/coq_omega.ml
OCAMLDEP  plugins/omega/omega.ml
OCAMLDEP  plugins/firstorder/unify.ml
OCAMLDEP  plugins/firstorder/rules.ml
OCAMLDEP  plugins/firstorder/formula.ml
OCAMLDEP  plugins/firstorder/sequent.ml
OCAMLDEP  plugins/firstorder/instances.ml
OCAMLDEP  plugins/firstorder/ground.ml
OCAMLDEP  plugins/ring/ring.ml
OCAMLDEP  theories/Numbers/Natural/BigN/NMake_gen.ml
OCAMLDEP  library/states.ml
OCAMLDEP  library/declaremods.ml
OCAMLDEP  library/global.ml
OCAMLDEP  library/summary.ml
OCAMLDEP  library/libnames.ml
OCAMLDEP  library/library.ml
OCAMLDEP  library/goptions.ml
OCAMLDEP  library/nametab.ml
OCAMLDEP  library/dischargedhypsmap.ml
OCAMLDEP  library/impargs.ml
OCAMLDEP  library/nameops.ml
OCAMLDEP  library/declare.ml
OCAMLDEP  library/heads.ml
OCAMLDEP  library/lib.ml
OCAMLDEP  library/libobject.ml
OCAMLDEP  library/decls.ml
OCAMLDEP  library/decl_kinds.ml
OCAMLDEP  checker/reduction.ml
OCAMLDEP  checker/environ.ml
OCAMLDEP  checker/check.ml
OCAMLDEP  checker/closure.ml
OCAMLDEP  checker/declarations.ml
OCAMLDEP  checker/validate.ml
OCAMLDEP  checker/term.ml
OCAMLDEP  checker/main.ml
OCAMLDEP  checker/type_errors.ml
OCAMLDEP  checker/mod_checking.ml
OCAMLDEP  checker/safe_typing.ml
OCAMLDEP  checker/indtypes.ml
OCAMLDEP  checker/checker.ml
OCAMLDEP  checker/check_stat.ml
OCAMLDEP  checker/typeops.ml
OCAMLDEP  checker/inductive.ml
OCAMLDEP  checker/subtyping.ml
OCAMLDEP  checker/modops.ml
OCAMLDEP  pretyping/evarconv.ml
OCAMLDEP  pretyping/pretype_errors.ml
OCAMLDEP  pretyping/unification.ml
OCAMLDEP  pretyping/evarutil.ml
OCAMLDEP  pretyping/classops.ml
OCAMLDEP  pretyping/vnorm.ml
OCAMLDEP  pretyping/typeclasses_errors.ml
OCAMLDEP  pretyping/indrec.ml
OCAMLDEP  pretyping/cases.ml
OCAMLDEP  pretyping/cbv.ml
OCAMLDEP  pretyping/evd.ml
OCAMLDEP  pretyping/reductionops.ml
OCAMLDEP  pretyping/term_dnet.ml
OCAMLDEP  pretyping/detyping.ml
OCAMLDEP  pretyping/pattern.ml
OCAMLDEP  pretyping/recordops.ml
OCAMLDEP  pretyping/tacred.ml
OCAMLDEP  pretyping/termops.ml
OCAMLDEP  pretyping/pretyping.ml
OCAMLDEP  pretyping/retyping.ml
OCAMLDEP  pretyping/clenv.ml
OCAMLDEP  pretyping/typing.ml
OCAMLDEP  pretyping/coercion.ml
OCAMLDEP  pretyping/matching.ml
OCAMLDEP  pretyping/rawterm.ml
OCAMLDEP  pretyping/inductiveops.ml
OCAMLDEP  pretyping/typeclasses.ml
OCAMLDEP  pretyping/namegen.ml
OCAMLDEP  lib/rtree.ml
OCAMLDEP  lib/gmapl.ml
OCAMLDEP  lib/system.ml
OCAMLDEP  lib/unicodetable.ml
OCAMLDEP  lib/pp_control.ml
OCAMLDEP  lib/profile.ml
OCAMLDEP  lib/edit.ml
OCAMLDEP  lib/dyn.ml
OCAMLDEP  lib/gmap.ml
OCAMLDEP  lib/heap.ml
OCAMLDEP  lib/util.ml
OCAMLDEP  lib/bigint.ml
OCAMLDEP  lib/flags.ml
OCAMLDEP  lib/fmap.ml
OCAMLDEP  lib/fset.ml
OCAMLDEP  lib/dnet.ml
OCAMLDEP  lib/segmenttree.ml
OCAMLDEP  lib/tries.ml
OCAMLDEP  lib/envars.ml
OCAMLDEP  lib/tlm.ml
OCAMLDEP  lib/explore.ml
OCAMLDEP  lib/gset.ml
OCAMLDEP  lib/bstack.ml
OCAMLDEP  lib/hashcons.ml
OCAMLDEP  lib/predicate.ml
OCAMLDEP  lib/option.ml
OCAMLDEP  tools/coqdep.ml
OCAMLDEP  tools/coqdep_boot.ml
OCAMLDEP  tools/gallina.ml
OCAMLDEP  tools/coqdoc/tokens.ml
OCAMLDEP  tools/coqdoc/output.ml
OCAMLDEP  tools/coqdoc/main.ml
OCAMLDEP  tools/coqdoc/index.ml
OCAMLDEP  tools/coqdoc/alpha.ml
OCAMLDEP  tools/coqdoc/cdglobals.ml
OCAMLDEP  tools/coqdep_common.ml
OCAMLDEP  proofs/evar_refiner.ml
OCAMLDEP  proofs/pfedit.ml
OCAMLDEP  proofs/logic.ml
OCAMLDEP  proofs/tacexpr.ml
OCAMLDEP  proofs/redexpr.ml
OCAMLDEP  proofs/clenvtac.ml
OCAMLDEP  proofs/tacmach.ml
OCAMLDEP  proofs/proof_type.ml
OCAMLDEP  proofs/decl_mode.ml
OCAMLDEP  proofs/refiner.ml
OCAMLDEP  proofs/tactic_debug.ml
OCAMLDEP  proofs/proof_trees.ml
OCAMLDEP  myocamlbuild.ml
OCAMLDEP  parsing/ppvernac.ml
OCAMLDEP  parsing/extrawit.ml
OCAMLDEP  parsing/printmod.ml
OCAMLDEP  parsing/tactic_printer.ml
OCAMLDEP  parsing/extend.ml
OCAMLDEP  parsing/egrammar.ml
OCAMLDEP  parsing/pptactic.ml
OCAMLDEP  parsing/prettyp.ml
OCAMLDEP  parsing/ppdecl_proof.ml
OCAMLDEP  parsing/ppconstr.ml
OCAMLDEP  parsing/printer.ml
OCAMLDEP  toplevel/himsg.ml
OCAMLDEP  toplevel/command.ml
OCAMLDEP  toplevel/classes.ml
OCAMLDEP  toplevel/lemmas.ml
OCAMLDEP  toplevel/vernacinterp.ml
OCAMLDEP  toplevel/coqinit.ml
OCAMLDEP  toplevel/autoinstance.ml
OCAMLDEP  toplevel/usage.ml
OCAMLDEP  toplevel/cerrors.ml
OCAMLDEP  toplevel/search.ml
OCAMLDEP  toplevel/vernacentries.ml
OCAMLDEP  toplevel/ind_tables.ml
OCAMLDEP  toplevel/class.ml
OCAMLDEP  toplevel/discharge.ml
OCAMLDEP  toplevel/coqtop.ml
OCAMLDEP  toplevel/toplevel.ml
OCAMLDEP  toplevel/metasyntax.ml
OCAMLDEP  toplevel/auto_ind_decl.ml
OCAMLDEP  toplevel/vernacexpr.ml
OCAMLDEP  toplevel/indschemes.ml
OCAMLDEP  toplevel/record.ml
OCAMLDEP  toplevel/libtypes.ml
OCAMLDEP  toplevel/vernac.ml
OCAMLDEP  dev/ocamlweb-doc/ast.ml
OCAMLDEP  dev/ocamlweb-doc/parse.ml
OCAMLDEP  dev/top_printers.ml
OCAMLDEP  dev/db_printers.ml
OCAMLDEP  dev/vm_printers.ml
OCAMLDEP  interp/coqlib.ml
OCAMLDEP  interp/dumpglob.ml
OCAMLDEP  interp/constrextern.ml
OCAMLDEP  interp/implicit_quantifiers.ml
OCAMLDEP  interp/notation.ml
OCAMLDEP  interp/topconstr.ml
OCAMLDEP  interp/constrintern.ml
OCAMLDEP  interp/smartlocate.ml
OCAMLDEP  interp/modintern.ml
OCAMLDEP  interp/genarg.ml
OCAMLDEP  interp/ppextend.ml
OCAMLDEP  interp/reserve.ml
OCAMLDEP  interp/syntax_def.ml
OCAMLDEP  ide/command_windows.ml
OCAMLDEP  ide/coq_tactics.ml
OCAMLDEP  ide/tags.ml
OCAMLDEP  ide/utils/configwin_ihm.ml
OCAMLDEP  ide/utils/configwin_keys.ml
OCAMLDEP  ide/utils/okey.ml
OCAMLDEP  ide/utils/configwin.ml
OCAMLDEP  ide/utils/configwin_messages.ml
OCAMLDEP  ide/utils/configwin_types.ml
OCAMLDEP  ide/utils/editable_cells.ml
OCAMLDEP  ide/utils/config_file.ml
OCAMLDEP  ide/gtk_parsing.ml
OCAMLDEP  ide/ideutils.ml
OCAMLDEP  ide/coq.ml
OCAMLDEP  ide/undo.ml
OCAMLDEP  ide/coq_commands.ml
OCAMLDEP  ide/preferences.ml
OCAMLDEP  ide/coqide.ml
OCAMLDEP  ide/typed_notebook.ml
OCAMLDEP  config/coq_config.ml
OCAMLDEP  tactics/decl_interp.ml
OCAMLDEP  tactics/leminv.ml
OCAMLDEP  tactics/elimschemes.ml
OCAMLDEP  tactics/dhyp.ml
OCAMLDEP  tactics/refine.ml
OCAMLDEP  tactics/auto.ml
OCAMLDEP  tactics/tacticals.ml
OCAMLDEP  tactics/termdn.ml
OCAMLDEP  tactics/contradiction.ml
OCAMLDEP  tactics/tactic_option.ml
OCAMLDEP  tactics/elim.ml
OCAMLDEP  tactics/inv.ml
OCAMLDEP  tactics/decl_proof_instr.ml
OCAMLDEP  tactics/dn.ml
OCAMLDEP  tactics/equality.ml
OCAMLDEP  tactics/autorewrite.ml
OCAMLDEP  tactics/eqschemes.ml
OCAMLDEP  tactics/btermdn.ml
OCAMLDEP  tactics/nbtermdn.ml
OCAMLDEP  tactics/tactics.ml
OCAMLDEP  tactics/hiddentac.ml
OCAMLDEP  tactics/evar_tactics.ml
OCAMLDEP  tactics/tacinterp.ml
CAMLP4DEPS plugins/funind/g_indfun.ml4
CAMLP4DEPS plugins/cc/g_congruence.ml4
CAMLP4DEPS plugins/nsatz/nsatz.ml4
CAMLP4DEPS plugins/fourier/g_fourier.ml4
CAMLP4DEPS plugins/romega/g_romega.ml4
CAMLP4DEPS plugins/subtac/g_subtac.ml4
CAMLP4DEPS plugins/xml/proofTree2Xml.ml4
CAMLP4DEPS plugins/xml/acic2Xml.ml4
CAMLP4DEPS plugins/xml/xml.ml4
CAMLP4DEPS plugins/xml/xmlentries.ml4
CAMLP4DEPS plugins/xml/dumptree.ml4
CAMLP4DEPS plugins/rtauto/g_rtauto.ml4
CAMLP4DEPS plugins/setoid_ring/newring.ml4
CAMLP4DEPS plugins/micromega/g_micromega.ml4
CAMLP4DEPS plugins/field/field.ml4
CAMLP4DEPS plugins/quote/g_quote.ml4
CAMLP4DEPS plugins/extraction/g_extraction.ml4
CAMLP4DEPS plugins/dp/g_dp.ml4
CAMLP4DEPS plugins/omega/g_omega.ml4
CAMLP4DEPS plugins/firstorder/g_ground.ml4
CAMLP4DEPS plugins/ring/g_ring.ml4
CAMLP4DEPS lib/refutpat.ml4
CAMLP4DEPS tools/coq_tex.ml4
CAMLP4DEPS tools/coq_makefile.ml4
CAMLP4DEPS parsing/g_xml.ml4
CAMLP4DEPS parsing/g_decl_mode.ml4
CAMLP4DEPS parsing/g_proofs.ml4
CAMLP4DEPS parsing/g_vernac.ml4
CAMLP4DEPS toplevel/whelp.ml4
CAMLP4DEPS toplevel/mltop.ml4
CAMLP4DEPS tactics/eauto.ml4
CAMLP4DEPS tactics/eqdecide.ml4
CAMLP4DEPS tactics/class_tactics.ml4
CAMLP4DEPS tactics/tauto.ml4
CAMLP4DEPS tactics/rewrite.ml4
CAMLP4DEPS tactics/extraargs.ml4
CAMLP4DEPS tactics/hipattern.ml4
CAMLP4DEPS tactics/extratactics.ml4
rm lib/refutpat.ml tactics/tauto.ml tactics/class_tactics.ml plugins/micromega/g_micromega.ml parsing/g_prim.ml plugins/field/field.ml parsing/vernacextend.ml tools/coq_makefile.ml toplevel/whelp.ml plugins/firstorder/g_ground.ml parsing/q_coqast.ml lib/compat.ml tactics/eauto.ml parsing/g_decl_mode.ml plugins/extraction/g_extraction.ml tactics/hipattern.ml tactics/rewrite.ml plugins/romega/g_romega.ml parsing/g_ltac.ml plugins/xml/xmlentries.ml parsing/g_tactic.ml plugins/fourier/g_fourier.ml plugins/funind/g_indfun.ml parsing/pcoq.ml parsing/tacextend.ml plugins/xml/xml.ml plugins/xml/acic2Xml.ml plugins/ring/g_ring.ml plugins/quote/g_quote.ml parsing/g_vernac.ml parsing/g_constr.ml plugins/rtauto/g_rtauto.ml lib/pp.ml plugins/dp/g_dp.ml plugins/omega/g_omega.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml plugins/xml/proofTree2Xml.ml parsing/lexer.ml parsing/argextend.ml toplevel/mltop.ml parsing/q_constr.ml parsing/g_proofs.ml plugins/setoid_ring/newring.ml plugins/cc/g_congruence.ml parsing/g_xml.ml plugins/nsatz/nsatz.ml plugins/subtac/g_subtac.ml parsing/q_util.ml tactics/eqdecide.ml tools/coq_tex.ml
make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'
make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'
OCAMLOPT -o bin/coqdep_boot
true bin/coqdep_boot
COQDEP  parsing/grammar.mllib
Testing parsing/grammar.cma
>> Fatal error: Ocaml and preprocessor have incompatible versions
Fatal error: exception Misc.Fatal_error
make[1]: *** [parsing/grammar.cma] Error 2
make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'
make: *** [stage1] Error 2
emake failed
 [31;01m*[0m ERROR: sci-mathematics/coq-8.3_p1 failed (compile phase):
 [31;01m*[0m   make failed
 [31;01m*[0m 
 [31;01m*[0m Call stack:
 [31;01m*[0m     ebuild.sh, line  56:  Called src_compile
 [31;01m*[0m   environment, line 2155:  Called die
 [31;01m*[0m The specific snippet of code:
 [31;01m*[0m       emake STRIP="true" -j1 || die "make failed"
 [31;01m*[0m 
 [31;01m*[0m If you need support, post the output of 'emerge --info =sci-mathematics/coq-8.3_p1',
 [31;01m*[0m the complete build log and the output of 'emerge -pqv =sci-mathematics/coq-8.3_p1'.
 [31;01m*[0m The complete build log is located at '/var/tmp/portage/sci-mathematics/coq-8.3_p1/temp/build.log'.
 [31;01m*[0m The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/coq-8.3_p1/temp/environment'.
 [31;01m*[0m S: '/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'