Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] running out of memory with big proof objects

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] running out of memory with big proof objects


chronological Thread 
  • From: Adam Chlipala <adam AT chlipala.net>
  • To: Aaron Bohannon <bohannon AT cis.upenn.edu>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] running out of memory with big proof objects
  • Date: Tue, 19 Oct 2010 18:12:16 -0400

Aaron Bohannon wrote:
Hi, I am running into a performance issue.  I have a moderately large
but straightforward proof.  Basically, it breaks down into 256 cases,
almost all of which are solved by one use of the "inversion" tactic
(that does not generate additional subgoals), followed by a use of the
"congruence" tactic.  It is easy to write a tactic definition to
finish the whole proof at once.  It takes about 20 seconds on my
machine to run the tactic in CoqIDE, and get "Proof completed."  If I
type "Qed," it takes about another 20 seconds to complete the proof.
If I say "Defined," CoqIDE will crash after about 20 seconds (coqc on
the command-line does not crash but doesn't work any faster).

Have you tried wrapping each case-solving tactic with the [abstract] tactical? This can have a dramatic effect on the amount of memory used for intermediate data structures.



Archive powered by MhonArc 2.6.16.

Top of Page