coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] profiling Gallina computations (vm_compute)

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] profiling Gallina computations (vm_compute)
Date: Thu, 2 Feb 2017 22:17:56 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f177.google.com
Ironport-phdr: 9a23:CocBJhW6eOY/jg2QKWlqQSuRs33V8LGtZVwlr6E/grcLSJyIuqrYbBSDt8tkgFKBZ4jH8fUM07OQ6PG8HzNYqsjb+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG5oAnLtMQanYRuJ6cvxhDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuBKvqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAooThvFQOrRq+BRKsBOzxyT9Dm2P73asg3OQnDA7NwQstEMgVv3TUrdX1L6cSXv62zKXS1zrDaelZ2THg54TScxAhoO2MXb1rfMrezEkgDQLFjlGKpYP5ODOV0/0Avm6G5ORuUuKvjnQoqwB3ojW32sgsjZPJhoQLxVDA8SV12pg6KsClSEN9fNWqE4NQujmEO4dqRs4uWWJltSYgxrEYpJK2fTIGxIklyhPdbfGMbpKG7Qj5VOmLJDd1nHJld6y7hxa16UWgz/fzVsiw0FpTtypFjsXAumkD1xDO6MWKSOFx/kim2TaI2ADT7v9LLVoomqrcLp4t2r8wlpwNvkTfBiL6hln6gauMekgn+uWk8frrbqjnq5OGKoN5iAPzPrwrmsOlAOQ4NgYOX3Kc+eS5zLDs51b2QLVLjv0tkqnWrpPaKd4Bqa6/GQBV1Jss5wy+DzenzNQYkmIKLF1AeB2djojpP0vCL+z/Dfe6m1isiitkx+jaPr39BZXANmTMkLD4fbpk90FczBczwstE6pJPCrABJerzVVXruNzZCB85KQ20zPz9BNVzzINNEV6IV6SeKebZtUKCrrYkJPDJb4sIsh78LeIk7rjglylqt0UaePyA15sWc3C1HbxPJUyfbTK4i90BEHwKswl4RerjjlHEUD9PaF69Wqs94ncwD4fwXtSLfZyknLHUhHTzJZZRfG0TUl0=

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