coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: François Bobot <francois AT bobot.eu>
- To: "Paul A. Steckler" <steck AT stecksoft.com>
- Cc: John Wiegley <johnw AT newartisans.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Timing and space benchmarks
- Date: Wed, 20 Apr 2016 10:44:33 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=francois.bobot.fb AT gmail.com; spf=Pass smtp.mailfrom=francois.bobot.fb AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f66.google.com
- Ironport-phdr: 9a23:PYnjlBCHX0uMHrHSNwwcUyQJP3N1i/DPJgcQr6AfoPdwSP7yosbcNUDSrc9gkEXOFd2CrakU26yI7uu5AjBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6bsptaKOFkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5i/vFlvUoyNGGiVGylsbSzTCuVvCV4r1+gK8/tFh1SKZOcDsB/hgQiiv5KRDUwPlgyQcMDAltmrQj5ojorhcpUePvRV5TInVe7a/M/B5YuuJc8kTQ2FGX915XStLBZ/6YpZZXLlJBvpRs4So/whGlhC5HwT5Qbm3xw==
---------- Forwarded message ----------
From: Paul A. Steckler
<steck AT stecksoft.com>
Date: Tue, Apr 19, 2016 at 4:07 AM
Subject: Re: [Coq-Club] Timing and space benchmarks
To: "Paul A. Steckler"
<steck AT stecksoft.com>,
coq-club AT inria.fr
In the latest OCaml Weekly News, there's an announcement about OCI, a
framework for benchmarking specific commits within a git repo. I'll
look into its suitability for this project.
I would be happy to help you to use OCI.
Remark that OCI is not by itself useful for micro-benchmarking, only macro-benchmarking. For micro-benchmark you need tools that does statistical analysis of multiple run, core_bench [1] is a good one for ocaml. The nice thing with OCI is that it is a framework and that you can gather the timing datas in many ways. So instead of only taking the execution time/memory consumption of the whole program, you could take the output given by core_bench (nanosecond precision, minor/major heap allocation count, ...) for datas.
Before implementing OCI I tried to use jenkins for doing benchmarking but
failed.
[1]: https://blogs.janestreet.com/core_bench-micro-benchmarking-for-ocaml/
--
François
- [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/18/2016
- Re: [Coq-Club] Timing and space benchmarks, John Wiegley, 04/18/2016
- Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/19/2016
- Message not available
- Re: [Coq-Club] Timing and space benchmarks, François Bobot, 04/20/2016
- Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/20/2016
- Message not available
- Re: [Coq-Club] Timing and space benchmarks, Jason Gross, 04/20/2016
- Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/21/2016
- Re: [Coq-Club] Timing and space benchmarks, Hugo Herbelin, 04/21/2016
- Re: [Coq-Club] Timing and space benchmarks, Jason Gross, 04/20/2016
- Re: [Coq-Club] Timing and space benchmarks, François Bobot, 04/20/2016
- Message not available
- Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/19/2016
- Re: [Coq-Club] Timing and space benchmarks, John Wiegley, 04/18/2016
Archive powered by MHonArc 2.6.18.