coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] profiling Gallina computations (vm_compute)

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] profiling Gallina computations (vm_compute)
Date: Fri, 03 Feb 2017 03:26:14 +0000
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-qt0-f179.google.com
Ironport-phdr: 9a23:hnxNshQzFbuG6j0UKdEXWRWp2Npsv+yvbD5Q0YIujvd0So/mwa67bBaN2/xhgRfzUJnB7Loc0qyN4vymBjRLv8zJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3Ked5KwzzpgHMvOEXh5FjI+A/0E2ajGFPfrF0zHhvIxq8hRHn/Y/k/pd49CJfofU67J9oXqDzfqB+RrtdWmd1e1sp7dHm4EGQBTCE4WERBz0b

There's apparently a way to profile native_compute, according to Pierre-Marie; see https://coq.inria.fr/bugs/show_bug.cgi?id=5170 (I don't actually know how to do it though)

On Thu, Feb 2, 2017 at 10:19 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a way to find out which functions take the most time when computing in Coq using vm_compute?
In the past, I used to approximate this by extracting to Haskell and then using ghc -prof.
However, doing that seems hard it in the current situation.

Thanks
-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] profiling Gallina computations (vm_compute), Abhishek Anand, 02/03/2017
- Re: [Coq-Club] profiling Gallina computations (vm_compute), Jason Gross, 02/03/2017