QuickChick / QuickChick

Randomized Property-Based Testing Plugin for Coq
Other
250 stars 46 forks source link

Serious performance issue for naive red-black tree generator #20

Open catalin-hritcu opened 9 years ago

catalin-hritcu commented 9 years ago

profile_quickchick741427

catalin-hritcu commented 9 years ago

The PROFILING file in the top folder contains the commands I was using for profiling in the past: https://github.com/QuickChick/QuickChick/blob/master/PROFILING (the QuickChick8baf2f part would need to be generalized, if you wanted to run this as a script)

catalin-hritcu commented 9 years ago

We could also try to use the newly released "OCaml Memory Profiler": http://memprof.typerex.org/

On Thu, Feb 12, 2015 at 9:39 AM, Çagdas Bozman cagdas.bozman@ocamlpro.com wrote:

Hi,

On behalf of the OCamlPro team, I am pleased to announce the public release of the OCaml Memory Profiler. This tool suite inspects the memory of OCaml applications at run-time to produce various offline reports on its usage.

Homepage: http://memprof.typerex.org/ Usage: http://memprof.typerex.org/free-version.php Support: http://memprof.typerex.org/report-a-bug.php Gallery of examples: http://memprof.typerex.org/gallery.php Commercial: http://memprof.typerex.org/commercial-version.php

The OCaml Memory Profiler contains an enhanced OCaml distribution (based on 4.01.0) that is used to build an instrumented version or your OCaml applications. Instrumented programs can inspect their memory on-demand to output memory dumps. These dumps contain the static type and allocation site of all allocated values (among other information). They are analyzed offline (outside of the application process) to produce reports that are displayed in your browser (see the gallery of examples).

The OCaml Memory Profiler comes in two different forms: an Online Version and a Commercial Version.

The Online Version can be used by everyone, it provides an OPAM switch and a tool, ocp-memprof. Once an application has been compiled in the switch, ocp-memprof can be used to trigger the output of memory snapshots, that are locally analyzed to generate a summary. The summary is sent to our online servers to be displayed in the gallery of examples.

The Commercial Version improves on the Online Version by removing the need for the online servers: summaries can be displayed locally, to provide complete development privacy. It also comes with support, to install and execute the tool (Basic Support option), to help understanding the results and fix applications (Advanced Support option) and with access to the sources (Extended Support option). Other additional features are available in the Commercial Version, such as more precise root descriptions and more frequent updates.

Enjoy, The OCamlPro Team