Bug 216040 - math/coq build process hangs with no noticeable CPU activity
Summary: math/coq build process hangs with no noticeable CPU activity
Status: In Progress
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: Any Any
: --- Affects Only Me
Assignee: Hiroki Sato
: 217530 (view as bug list)
Depends on:
Reported: 2017-01-13 20:43 UTC by Peter Kien
Modified: 2019-08-14 16:28 UTC (History)
3 users (show)

See Also:
bugzilla: maintainer-feedback? (hrs)


Note You need to log in before you can comment on or make changes to this bug.
Description Peter Kien 2017-01-13 20:43:13 UTC
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!
Comment 1 Peter Kien 2017-01-13 21:10:14 UTC

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.
Comment 2 Hiroki Sato freebsd_committer 2017-01-16 10:30:18 UTC
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.
Comment 3 Tobias Kortkamp freebsd_committer 2018-03-14 08:06:29 UTC
*** Bug 217530 has been marked as a duplicate of this bug. ***
Comment 4 Walter Schwarzenfeld freebsd_triage 2019-08-14 16:28:33 UTC
Ocaml is now version 4.05.0. Still problems with math/coq?