coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Danko Ilik <dankoilik AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Programming language shootout for Coq?
- Date: Tue, 2 Mar 2010 11:54:06 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=wAZSfUgOAabiEm6MHlNZX7uKJewQuiRyvImSyULutsprAh4TlukZZWcODtjXFNUWSi /AN32We+dxDkprtuLazP8zctRU9ZR/LmSm+WdykWgz1xfDFt2JrPMc0XjdUcnqKr2b9f f0XmtmMRMTDPFahBFFMZExgYj393GoN9OA35I=
On Tue, Mar 2, 2010 at 10:56 AM, Stéphane Glondu <steph AT glondu.net> wrote:
One could also run all the benchmarks inside one coqtop session, running "Time Eval vm_compute in (program input)", which would be a benchmark of Coq's virtual machine, without the pre-/post-processing overhead.
Another approach would be to wrap IOs in some kind of script, that would
parse the input, generate apropriate Coq input file, run it through
coqtop, then parse the output and turn it into the expected format. It
might be funny to compare Coq to other programming languages this way.
But this would also benchmark the pre/post-processing steps (for which
another language has to be chosen, too).
One could also run all the benchmarks inside one coqtop session, running "Time Eval vm_compute in (program input)", which would be a benchmark of Coq's virtual machine, without the pre-/post-processing overhead.
Danko
- [Coq-Club] Programming language shootout for Coq?, Bas Spitters
- Re: [Coq-Club] Programming language shootout for Coq?,
Stéphane Glondu
- Re: [Coq-Club] Programming language shootout for Coq?, Danko Ilik
- Re: [Coq-Club] Programming language shootout for Coq?,
Bas Spitters
- Re: [Coq-Club] Programming language shootout for Coq?,
Adam Koprowski
- Re: [Coq-Club] Programming language shootout for Coq?,
Greg Morrisett
- Re: [Coq-Club] Programming language shootout for Coq?, Adam Koprowski
- Re: [Coq-Club] Programming language shootout for Coq?,
Greg Morrisett
- Re: [Coq-Club] Programming language shootout for Coq?,
Adam Koprowski
- [Coq-Club] local definitions/proof environments, Vladimir Voevodsky
- Re: [Coq-Club] Programming language shootout for Coq?,
Mathieu Boespflug
- Re: [Coq-Club] Programming language shootout for Coq?,
Bas Spitters
- Re: [Coq-Club] Programming language shootout for Coq?, Mathieu Boespflug
- Re: [Coq-Club] Programming language shootout for Coq?,
Bas Spitters
- Re: [Coq-Club] Programming language shootout for Coq?,
Stéphane Glondu
Archive powered by MhonArc 2.6.16.