Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Timing and space benchmarks

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Timing and space benchmarks


Chronological Thread 
  • From: "Paul A. Steckler" <steck AT stecksoft.com>
  • To: Jason Gross <jasongross9 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>, John Wiegley <johnw AT newartisans.com>
  • Subject: Re: [Coq-Club] Timing and space benchmarks
  • Date: Thu, 21 Apr 2016 11:55:32 +0200
  • Authentication-results: mail3-smtp-sop.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-f67.google.com
  • Ironport-phdr: 9a23:S9wPfBToO6PaxKOsC0YHPMQGENpsv+yvbD5Q0YIujvd0So/mwa64bBWN2/xhgRfzUJnB7Loc0qyN4/CmBzxLuMfJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uNM04R1XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1kVSWIQ2jVSBBPepEX4V4z2tCTgsfFmiQGVOMT3SfY/XjH0vIlxTxq9wh8OKjpx2SefsdB9h6FfrQjr70hk34PfY6mOKPd1fbjac89cTm1ECJUCHxddC5+xOtNcR9EKOvxV+syk/wMD

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
>
>



Archive powered by MHonArc 2.6.18.

Top of Page