Skip to content

Latest commit

 

History

History
215 lines (174 loc) · 9.45 KB

README.md

File metadata and controls

215 lines (174 loc) · 9.45 KB
Raw

slow-coq-examples

Preface

My experience with slowness is that slowness is most often caused by Coq doing work it doesn't need to do. Usually, this work comes in the form of retypechecking terms it shouldn't need to retypecheck, and occasionally it comes in the form of (re)doing typeclass search that can be known to be useless. I don't want to have to micro-optimize my tactic scripts to get 1000x speed-ups. In general, I have the sense that I can't trust Coq to be fast, and I can't trust scripts that are fast to remain fast in future versions of Coq unless I'm proactive about reporting bugs and performance regressions.

Specifics

Some examples of Coq being really slow:

Already fixed or partially fixed issues:

All right, I think I'm the responsible here. This is probably because of commit a895b2c0ca that introduced a performance enhancement of auto hints in the non-polymorphic case. The polymorphic case has a nice comment

(** FIXME: We're being inefficient here because we substitute the whole
          evar map instead of just its metas, which are the only ones
          mentioning the old universes. *)

which is exactly the hotspot I'm seeing right there. I'll write a quick fix.

and then, after fixing that, said:

Note that there is still a hotspot that looks suspicious to me. Indeed, the code for Evarsolve.noccur_evar whose goal is essentially to ensure that an evar does not appear in a term repeatedly calls the following snippet of code

    let c =
      try Retyping.expand_projection env evd p c []
      with Retyping.RetypeError _ ->
	(* Can happen when called from w_unify which doesn't assign evars/metas
	   eagerly enough *) c
    in occur_rec acc c

which is responsible for ~50% of the time passed in one of your tactics for no good reason.

  • Bug #3447 - Some Defineds are 30x slower in trunk - most of the time was spent hashconsing universes.

Issues related to Proof General slowness (not Coq slowness per se):

  • Bug #4669 - printing of dependent evars in ProofGeneral can slow emacs interaction to a crawl (because printing of dependent evars in the goal does not respect Set Printing Width) - see slow_dependent_evars_in_pg.v, and make sure to let it set coq-end-goals-regexp-show-subgoals to nil appropriately.

Issues marked WONTFIX:

#4640, Has to do with slow [End Section] in special case of no section variables.

Issues marked MOVED:

  • Bug #4625 - checking Defined/Qed causes coqtop to drop the most recent proof state. This makes it a pain to debug things like:
Definition foo : bar.
Proof.
  some_slow_tactic.
  some_tactic_that_makes_Defined_slow.
Defined.

Issues marked INVALID:

  • Bugs #4643, #4642, and #4779: Defined. sometimes takes 2 minutes; End Section can take 30 seconds, even though there are no section variables, no tactics, no notations, no Lets, and only one or two Definitions; cbv [some identifiers] can run through 64 GB of RAM in 15 minutes; and pose y as x; change y with x in H can be 1300x slower than set (x := y) in H; respectively. See slow_fiat_examples/README.md for more details and instructions on running. (Be warned, some of the examples of slowness themselves take 20 minutes to compile.)