coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Timing and space benchmarks

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: François Bobot <francois AT bobot.eu>
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 11:01:58 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f65.google.com
Ironport-phdr: 9a23:v6tUchIYgnGx/lrdW9mcpTZWNBhigK39O0sv0rFitYgUIv7xwZ3uMQTl6Ol3ixeRBMOAu6IC1bed6vu8EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Txib35osaPKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WYxGG4PQbU34huB1CBBSNuB/gV5H6tSrhnuB60i6Ge8DrG+MaQzOnuu1TQQLswA5BfwUl/WrUjsFqxuoPuw6srB9X2JLZa4KOM/RiOKjaeIVJFiJ6Qs9NWnkZUcuHZIwVAr9EZL4Aog==

Thanks, I appreciate the offer.

I don't know yet what the execution times will be for the all the
tactics, so I'm not sure which side of the macro-/micro- divide they
will fall in. We do have examples of tactics that take many seconds to
run, though.

-- Paul

On Wed, Apr 20, 2016 at 10:44 AM, François Bobot
<francois AT bobot.eu>
wrote:
>
>> ---------- 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