Łukasz Czajka

You need 'predict' on the path. This is mentioned in the documentation, but maybe the error message from CoqHammer should clearly state that it's the most probable reason. Perhaps you...

This seems to be related to issue #64 but now it is in "hammer" instead of in "sauto". The "CoqHammer bug: Not_found" error occurs when trying to compile a whole...

The proofs are very much the issue. `hammer` needs access to the proof objects to do premise selection. Now, one could try to treat theorems without proof objects like axioms,...

Thank you for this example, but even after a brief look I see it is probably one of the examples that "sauto" will have problems with. I would say the...

In fact, the following works, which suggests that forward reasoning is the problem: intro k. specialize (B1 k). specialize (B2 k). specialize (B3 k). specialize (B4 k). sauto inv: -...

The slow runtime is indeed not acceptable in this case. I'll leave this issue open as an enhancement, because fixing this requires more fundamental work on efficient forward-reasoning proof search...

> I also tried to use the `hecrush` that worked on the isolated standalone example in the actual context, and there it didn't finish for several minutes. That's something I...

Yes, it would make sense to have this as a separate option. There would be a performance penalty, however, so this should be an option. I think it shouldn't be...

If you have the desire to do it, read a Coq plugin tutorial (https://github.com/coq/coq/tree/master/doc/plugin_tutorial), and then look at the "sauto" tactic implementation in: https://github.com/lukaszcz/coqhammer/blob/coq8.14/src/tactics/sauto.ml The implementation already does things like...

Thank you for pointing this out. I'll leave it for now, because it's a bit complicated to change. The problem is that libexec is typically not on the path. So...