I’m trying to build Coq with spacetime so I can profile it.
I was able to set up OCaml 4.06.0+spacetime with opam.
- When opam tries to compile Coq, I see enormous memory usage for Coq (~20GB) and an eventual segfault on one of the files that Coq compiles even though the profiling should AFAIU not be turned on at that point.
- I also tried building Coq from sources. That produced linker errors on a few files, such as:
OCAMLOPT tools/coqdep_boot.ml OCAMLBEST -o bin/coqdep_boot /tmp/camlstartupb3909a.o: In function `caml_spacetime_shapes': :(.data+0x14b8): undefined reference to `camlUnix__spacetime_shapes' :(.data+0x14c0): undefined reference to `camlUnixLabels__spacetime_shapes' :(.data+0x14c8): undefined reference to `camlThread__spacetime_shapes' :(.data+0x14d0): undefined reference to `camlMutex__spacetime_shapes' :(.data+0x14d8): undefined reference to `camlCondition__spacetime_shapes' :(.data+0x14e0): undefined reference to `camlEvent__spacetime_shapes' :(.data+0x14e8): undefined reference to `camlThreadUnix__spacetime_shapes' :(.data+0x14f0): undefined reference to `camlStr__spacetime_shapes'
What am I missing here?
- Also, is it feasible to use spacetime to profile a 4GB process? How much additional memory might I need for the spacetime data?