The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

On Wed, Apr 20, 2016 at 03:17:27PM -0400, Jason Gross 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

This is probably more a discussion for coqdev, but fyi the linear code
is here the usual suspect, namely the ensurance that existential
variables are expanded using an eager normalization algorithm before
applying the tactic (in nf_enter).

Hugo

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