[Bug 216040] math/coq build process hangs with no noticeable activity

[bugzilla-noreply at freebsd.org]

https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=216040

            Bug ID: 216040
           Summary: math/coq build process hangs with no noticeable
                    activity
           Product: Ports & Packages
           Version: Latest
          Hardware: Any
                OS: Any
            Status: New
          Severity: Affects Only Me
          Priority: ---
         Component: Individual Port(s)
          Assignee: hrs at FreeBSD.org
          Reporter: peter.kien at fastmail.co.uk
          Assignee: hrs at FreeBSD.org
             Flags: maintainer-feedback?(hrs at FreeBSD.org)

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!

-- 
You are receiving this mail because:
You are the assignee for the bug.