coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Timing and space benchmarks

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>, "Paul A. Steckler" <steck AT stecksoft.com>
Cc: John Wiegley <johnw AT newartisans.com>
Subject: Re: [Coq-Club] Timing and space benchmarks
Date: Wed, 20 Apr 2016 15:17:27 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f48.google.com
Ironport-phdr: 9a23:p8M7JxTJoSe/f+DuGtXlRSslT9psv+yvbD5Q0YIujvd0So/mwa65ZReN2/xhgRfzUJnB7Loc0qyN4/CmBzJLuM3a+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VPVsD3WHmKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayV+0CQLdZFDUrNXwurI2u7EGbDFjH2nxJWWIP1xFMHgKNuBr9R9L6tjbwnut7wiiTe8PsG/R8Ewyr8qMjYVmgszsKPD09/XudwphrkK9Qozq6uxF0wJXTbp3TP/17KPDzZ9QfEEhIRcFXHwNbBZinJ98NBvEGO+lCqJLm9nMBqBK/AU+nA+a5mWwAvWP/waBvi7dpKgrBxgF1WotW6Hk=

Here is a script that exercises the unfortunate dependence of tactics on the size of the goal. (Here is an example of a tactic which should be constant in the size of the goal but is instead linear: [lazymatch goal with |- ?f ?a = ?g ?b => idtac end].)
https://gist.github.com/JasonGross/e494d8f9fcf8c4239815bdcfa7e22fc8

On Wed, Apr 20, 2016 at 9:54 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