Issue with auto.native

[threonorm]

Hi,

I was trying to play around with the different backend solver, and especially the native on. From here I tried to look up how to use the native solver, and after investigation using the same command for emulateNative, it seems auto is not sound (or maybe I am misunderstanding how to use it?):

import Auto.Tactic

set_option auto.native true
attribute [rebind Auto.Native.solverFunc] Auto.Solver.Native.emulateNative

example : False := by auto 
-- It seems to say that it has found a proof in 1ms (but it used sorry to admit the proof)

(Tested with commit 60e546c, Lean v4.11)

[PratherConid]

Sorry for the confusion. emulateNative always uses sorry to close the goal. I've added a paragraph in readme to explain how to use the native solver duper