diff options
| author | gareuselesinge | 2013-10-24 15:41:38 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-24 15:41:38 +0000 |
| commit | a2388b6ae2b3bf680d03487abac00787e50976f9 (patch) | |
| tree | caffd66cb61e6f0cdb99c4d7f21e310fb3b33662 /lib | |
| parent | 7bded288b7727625ee353af5a142ecba15d57240 (diff) | |
Ephemeron: add a function to run a collection cycle
This is necessary if one wants to check how much memory
Coq uses after a collection. The idiom is:
Gc.full_major (); Ephemeron.clear (); Gc.full_major ();
since the first collection may just put collected ephemerons
in a to_be_cleared list that is processed by Ephemeron.get/create/clear.
Processing the list may create new garbage (the content of the ephemeron),
Hence a new Gc cycle has to be run afterwards.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16929 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/ephemeron.ml | 2 | ||||
| -rw-r--r-- | lib/ephemeron.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/lib/ephemeron.ml b/lib/ephemeron.ml index ee763086c9..d4ce7b1eac 100644 --- a/lib/ephemeron.ml +++ b/lib/ephemeron.ml @@ -85,3 +85,5 @@ let iter_opt k f = with | None -> () | Some v -> f v + +let clear () = run_collection () diff --git a/lib/ephemeron.mli b/lib/ephemeron.mli index bc34c5c66f..c1ceb3fd97 100644 --- a/lib/ephemeron.mli +++ b/lib/ephemeron.mli @@ -48,3 +48,5 @@ val get : 'a key -> 'a (* These never fail. *) val iter_opt : 'a key -> ('a -> unit) -> unit val default : 'a key -> 'a -> 'a + +val clear : unit -> unit |