coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Timing and space benchmarks

From: "John Wiegley" <johnw AT newartisans.com>
To: "Paul A. Steckler" <steck AT stecksoft.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Timing and space benchmarks
Date: Mon, 18 Apr 2016 09:29:30 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f179.google.com
Ironport-phdr: 9a23:JDRZbxMaiPHebetPT2Al6mtUPXoX/o7sNwtQ0KIMzox0KPT9rarrMEGX3/hxlliBBdydsKIUzbSM+Pm4ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTnkb7osMSLO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGEG372YYGkxQ2iFUDgPG6BzgFN+lqTf3velVwzWXNs7tSr4oHz+l6vE4ZgXvjXJNFTk59inoi8F/iK9K6lr1pRt/xZH8ZoyKPeBif7jUe8hcTm1ECJUCHxddC5+xOtNcR9EKOvxV+syk/wMD
Organization: New Artisans LLC

>>>>> Paul A Steckler
>>>>> <steck AT stecksoft.com>
>>>>> writes:

> At the Working Group meeting on Friday, I suggested that it would be a good
> idea to have benchmarks for individual tactics. My original thought was to
> have timing benchmarks, and others suggested space benchmarks would be
> useful as well. Such benchmarks could be used as the basis of regression
> tests. The attendees seemed to agree that benchmarks would be a good idea. I
> hope others agree.

This is a great idea, Paul, and it's something I've been trying to get started
for Emacs Lisp as well, so I'd be interested to learn what kind of tooling you
build to make this project happen.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/18/2016
- Re: [Coq-Club] Timing and space benchmarks, John Wiegley, 04/18/2016
  - Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/19/2016
    - Message not available
      - Re: [Coq-Club] Timing and space benchmarks, François Bobot, 04/20/2016
        
        Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/20/2016
        
        Message not available
        
        Re: [Coq-Club] Timing and space benchmarks, Jason Gross, 04/20/2016
        
        Re: [Coq-Club] Timing and space benchmarks, Paul A. Steckler, 04/21/2016
        
        Re: [Coq-Club] Timing and space benchmarks, Hugo Herbelin, 04/21/2016