The Coq mailing list

["Paul A. Steckler" <steck AT stecksoft.com>]

Thanks, we now have a start for our benchmark suite!

-- Paul

On Wed, Apr 20, 2016 at 9:17 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> 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
>
>