Using hammer

Stream: general

[Alex J. Best]

@Gabriel Ebner I saw your hammer talk (remotely unfortuately) and it was so cool I wanted to try it for myself! I appreciate its not a finished product so feel free to ignore me but I had two problems getting it to work on my machine:

I'm on OSX and the built in grep does not support -oP instead I had to replace it with a perl one-liner https://stackoverflow.com/a/16658690/2105639 it would be nice if this was built in (either perl everywhere? or some case switching depending on the OS) (I can try and send you a patch if you like).

The second is that commit https://github.com/gebner/mathlib/commit/f073946e12676ae0dd0ae87ac4d2a300fd4c082b breaks everything for me, is my version of lean-community/lean:3.5.0 missing something that yours has?

With these two caveats I got it to run both with vampire and eprover-ho in the end, its very cool (and surprisingly the generated proofs are almost readable), thanks for your great work I can't wait till its done!

[Gabriel Ebner]

Thanks for the encouraging words, Alex! If you send me the patch to switch to perl, I'll apply it.

[Gabriel Ebner]

The current version requires you to build lean from this branch here: https://github.com/gebner/lean/tree/feature_search You can use elan toolchain link to register your locally built version of lean with elan and then it should just work.

[Alex J. Best]

Ah cool thanks! I looked but somehow didn't find that branch oops.

[Alex J. Best]

perlpatch.diff should do the trick I think. I'll test it once I have feature_searchloaded