diff options
| author | ppedrot | 2013-10-29 17:11:03 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-29 17:11:03 +0000 |
| commit | 776a499245d7bb28bce9a55fa8d0b082801d66b4 (patch) | |
| tree | 3c94841acaaf0633b2e2ab2e94a9f13b883a6f87 | |
| parent | cbbd579354d81f6749d14853a1c6a5cc67728907 (diff) | |
Printing heap on every processed sentence.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 10 |
3 files changed, 12 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 964a4694fd..513a729e1a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -104,7 +104,7 @@ LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS) -OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS) +OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS) -allocation-tracing BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) -thread OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -thread diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 0bcd44d0eb..5da5688005 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -267,7 +267,7 @@ let main () = (* native code *) if !top then failwith "no custom toplevel in native code !"; let ocamloptexec = Filename.quote (Filename.concat camlbin "ocamlopt") in - ocamloptexec^" -linkall" + ocamloptexec^" -linkall -allocation-tracing" end else (* bytecode (we shunt ocamlmktop script which fails on win32) *) let ocamlmktoplib = if is_ocaml4 diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index eaa5b75494..a59460bc54 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -239,6 +239,15 @@ let display_cmd_header loc com = str (" ["^cmd^"] ")); Pp.flush_all () +let print_heap = + let idx = ref 0 in + fun () -> + let pid = Unix.getpid () in + let i = !idx in + let () = incr idx in + let filename = Printf.sprintf "heap.%i.%i" pid i in + Allocation_profiling.Global.dump_allocations_by_address ~filename + let rec vernac_com verbosely checknav (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> @@ -295,6 +304,7 @@ and read_vernac_file verbosely s = (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do + print_heap (); let loc_ast = parse_sentence input in vernac_com verbosely checknav loc_ast; pp_flush () |