The Coq mailing list

[Jim Fehrle <jfehrle AT sbcglobal.net>]

Hi Michael,

> Also if eauto is used, one can easily add the debug flag (for typeclasses eauto it is a global option). It is a good idea to have a look at the logs and the branching factors of the proof search.

Logs meaning the console output from Set Debug Auto/Set Debug Eauto?  By the branching factor, you just mean paying attention to the output (e.g. 1.2.3.1 is depth 4) and each digit counts the branches at it's level?

> the core hint database includes hints which can loop to the search depth limit on some goals.

How helpful would it be if auto/eauto detected and avoided looping?  Either by a) detecting that the proof state has already been seen in the current search (e.g. there is a tactic for a commutative property) and/or b) using a queue that ranks various proof states by a size metric and processing the smaller proof states first.  This might give better performance and allow for a higher depth limit.

Thanks,

Jim

count_rev_tree < Set Debug Eauto.

count_rev_tree < eauto.

Debug: (* debug eauto: *)

Debug: 1 depth=5

Debug: 1.1 depth=4 simple apply f_equal_nat

Debug: 1.1.1 depth=3 simple apply f_equal2_nat

Debug: 1.2 depth=4 simple apply f_equal2_nat

Debug: 1.2.1 depth=4 simple apply @eq_refl

Debug: 1.2.1.1 depth=3 simple apply f_equal2_nat

Debug: 1.2.2 depth=4 simple apply eq_add_S ; trivial

Debug: 1.2.2.1 depth=3 simple apply f_equal2_nat

Debug: 1.2.3 depth=4 simple apply eq_sym ; trivial

Debug: 1.2.3.1 depth=3 simple apply f_equal2_nat

---

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Sent: Thursday, November 15, 2018 2:22 AM
Subject: RE: [Coq-Club] Moving away from putting hints in the core hintdb

Dear Armaël,

in my experience including the core hint database frequently leads to bad proof search performance. E.g. the core hint database includes hints which can loop to the  search depth limit on some goals. I would generally recommend to apply proper engineering practices in designing hint databases and to not provide a substantially larger set of hints than required.

I typically use a set of tactics and/or tactic notations to wrap eauto with certain sets of hint databases suitable for specific problems. This wrapping also makes it easier to switch between eauto and typeclasses eauto, which is a good idea to try. Also if eauto is used, one can easily add the debug flag (for typeclasses eauto it is a global option). It is a good idea to have a look at the logs and the branching factors of the proof search.

Best regards,

Michael