Spacetime on Windows Subsystem for LInux

Community
1

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.

  1. 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.

Any suggestions?

  1. 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?

  1. Also, is it feasible to use spacetime to profile a 4GB process? How much additional memory might I need for the spacetime data?
2

Might be good to eliminate some variables:

(1) can you build Coq on WSL with a standard compiler/runtime?
(2) can you build Coq on Linux with Spacetime ?

3

(1) can you build Coq on WSL with a standard compiler/runtime?

All the time.

(2) can you build Coq on Linux with Spacetime ?

Not having a Linux system, no.

In the meantime, I was advised that memprof, a statistical memory profiler, is a better choice for a process using so much memory (4GB). See https://ocaml.org/meetings/ocaml/2016/Jourdan-statistically_profiling_memory_in_OCaml.pdf. You need to switch to a modified OCaml in opam, such as 4.06.1+statistical-memprof and then add something to your code to turn it on, such as GitHub - ppedrot/coq at jh-memprof-new.

4

Have you been able to build a bunch of other packages on WSL, with spacetime? Assuming so, then (sigh) looks like something specific to the Coq build. And the next step would be to find out which file, when compiled with which args, blows up. Or if it’s some bootstrap/init step.