Hello Hiroki, hello everyone! :) the summary says it all. Here are the last build messages (I can of course post more): ------------------------------------------- "/usr/local/bin/ocamlfind" ocamlc -rectypes -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I stm -I toplevel -I parsing -I printing -I intf -I engine -I ltac -I tools -I tools/coqdoc -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/setoid_ring -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/derive -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I plugins/decl_mode -I plugins/btauto -I plugins/ssrmatching -I "+camlp5" -thread -pack -o plugins/romega/romega_plugin.cmo plugins/romega/const_omega.cmo plugins/romega/refl_omega.cmo plugins/romega/g_romega.cmo cp bin/coqtop.byte bin/coqtop rm -f theories/Init/Notations.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Notations.v -noinit -R theories Coq rm -f theories/Init/Logic.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Logic.v -noinit -R theories Coq rm -f theories/Init/Datatypes.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Datatypes.v -noinit -R theories Coq rm -f theories/Init/Wf.glob rm -f theories/Init/Tauto.glob rm -f theories/Init/Nat.glob rm -f theories/Init/Specif.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Tauto.v -noinit -R theories Coq env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Nat.v -noinit -R theories Coq env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Wf.v -noinit -R theories Coq rm -f theories/Init/Logic_Type.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Specif.v -noinit -R theories Coq env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Logic_Type.v -noinit -R theories Coq rm -f theories/Init/Peano.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Peano.v -noinit -R theories Coq rm -f theories/Init/Tactics.glob env CAML_LD_LIBRARY_PATH=${PWD}/kernel/byterun bin/coqtop -boot -native-compiler -compile theories/Init/Tactics.v -noinit -R theories Coq ------------------------------------------- Thanks for your help!
Addendum: I was still able to build math/coq on January 6. (I rebuilt my entire Ports system, including math/coq, on January 6.) My current ports Tree is dated from January 12.
OCaml 4.02.3 (the version in the ports tree, lang/ocaml) seems to have a deadlock problem with compilation of math/coq. Because I am working on upgrading it to 4.04.0 and it works fine, I am planning to fix this issue by upgrading the related ports including lang/ocaml. Please be patient until it finishes.
*** Bug 217530 has been marked as a duplicate of this bug. ***
Ocaml is now version 4.05.0. Still problems with math/coq?