diff options
| author | Pierre-Marie Pédrot | 2015-11-19 18:40:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-19 20:16:45 +0100 |
| commit | 574e510ba069f1747ecb1e5a17cf86c902d79d44 (patch) | |
| tree | 694fa60567202af7e66f71b5a9fb727d2753dc24 /tactics | |
| parent | cfc0fc0075784e75783c9b4482fd3f4b858a44bf (diff) | |
Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.
The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.
Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ee7b94b0d1..20a7448dcb 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -166,6 +166,10 @@ and e_my_find_search db_list local_db hdc concl = in let tac_of_hint = fun (st, {pri = b; pat = p; code = t; poly = poly}) -> + let b = match Hints.repr_hint t with + | Unfold_nth _ -> 1 + | _ -> b + in (b, let tac = function | Res_pf (term,cl) -> unify_resolve poly st (term,cl) @@ -245,8 +249,8 @@ module SearchProblem = struct let d = s'.depth - s.depth in let d' = Int.compare s.priority s'.priority in let nbgoals s = List.length (sig_it s.tacres) in - if not (Int.equal d' 0) then d' - else if not (Int.equal d 0) then d + if not (Int.equal d 0) then d + else if not (Int.equal d' 0) then d' else Int.compare (nbgoals s) (nbgoals s') let branching s = |