The Coq mailing list

["Michal Moskal" <michal.moskal AT gmail.com>]

Hi again,

it seems mailman didn't like to attachment (see below). I've put it
online, here:

 http://nemerle.org/~malekith/temp/just-defs.v
 http://nemerle.org/~malekith/temp/proof.v

We've did some profiling and it seems that functions checking for list
uniqueness were taking a lot of time. Here's a patch to fix that:

 http://nemerle.org/~malekith/temp/uniq.patch

This makes it go about 10x faster through the initial definitions,
until it hits the giant AND over terms. Then it seems
Sign.lookup_named takes a lot of time. Unfortunately it's not easy to
change the data structure used there (a list, that is searched
linearly), because it's not abstract.

Any chances someone will fix that soon?

Thanks!

---------- Forwarded message ----------
From: Michal Moskal 
<michal.moskal AT gmail.com>
Date: Mar 30, 2007 12:48 AM
Subject: coq performance
To: 
coq-club AT pauillac.inria.fr
Cc: Mikolá¹ Janota 
<mikolas.janota AT gmail.com>,
 Joseph Kiniry 
<kiniry AT acm.org>


Hi,

We're trying to use Coq for checking proofs produced by a SMT checker.
It seems that even for very small proofs (with a hundred or so clauses
and 2000 subterms in the formula) coqtop takes a very long time to
parse the proof.

Currently we're using /\, \/, ->, forall etc for representing formulas
we'd like to prove. We also thought about defining datatype in Coq to
describe formulas and functions to apply rules, proving their
properties and then possibly extracting OCaml source, but I would
rather not do it as it seems way more complicated.

I understand Coq was not optimized to handle large files, but is
switching to proofs at the object level done by extracted code the way
to go? Maybe we're just hitting some non-optimized corner case in Coq?

In case somebody is interested, I'm attaching the proof file (which
probably won't typecheck, but it takes ages to parse).

--
  Micha³