diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 15 |
3 files changed, 2 insertions, 17 deletions
diff --git a/Makefile.build b/Makefile.build index 513a729e1a..964a4694fd 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) -allocation-tracing +OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) -thread OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -thread diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 5da5688005..0bcd44d0eb 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 -allocation-tracing" + ocamloptexec^" -linkall" 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 d838954e6d..eaa5b75494 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -239,20 +239,6 @@ let display_cmd_header loc com = str (" ["^cmd^"] ")); Pp.flush_all () -let is_profiling = - try ignore (Sys.getenv "CAMLRUNPARAM"); true - with Not_found -> false - -let print_heap = - let idx = ref 0 in - fun () -> - if is_profiling then - 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.Heap_snapshot.dump_allocators_of_major_heap_blocks ~filename - let rec vernac_com verbosely checknav (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> @@ -309,7 +295,6 @@ 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 () |