Stream: Coq devs & plugin devs

Topic: firstorder tactic limitations


view this post on Zulip Karl Palmskog (Jun 04 2020 at 11:30):

This seems like an almost ridiculous limitation of firstorder that came up in the CoqHammer authors' evaluation of his tactics against firstorder:

For firstorder, we did not implement iterative deepening, because the depth limit is a global parameter not changeable at the tactic language level

Shouldn't tactic-level depth limit be quite easy to implement?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 11:33):

Sure, that should be doable.

view this post on Zulip Karl Palmskog (Jun 04 2020 at 11:36):

sounds good. However, since I'm not super invested in this topic myself, maybe I can just open an issue on it and say "this would be nice to have"?


Last updated: Oct 16 2021 at 02:03 UTC