tactic.trace

Stream: Is there code for X?

[Frédéric Le Roux]

Is there a code to intercept the result of tactic.trace? More specifically, I would like a tactic that turns a tactic unit into a tactic string, the output string being the (maybe empty) string that is traced by the original tactic.

[Scott Morrison]

I think there isn't.

[Ashley Blacquiere]

@Frédéric Le Roux I'm currently learning about metaprogramming and stumbled across this thread while looking for recent tactic feature requests that I could try my hand at. I'm not 100% sure I can help, but I'm willing to give it a go. Can you be more specific about the use case that you're trying to address?

[Rob Lewis]

Unfortunately I don't think this is solveable with a Lean metaprogram, you'd have to dig into the C++ source.

[Rob Lewis]

Maybe there's a very hackish way to do it but it won't be pretty...

[Ashley Blacquiere]

Ya, I kinda wondered - I did some initial exploration but couldn't see how best to grab a hold of the necessary objects. Thought I might have been misinterpreting the request tho.

[Frédéric Le Roux]

Thanks for your answer. I have actually modified all my tactics into tactic string "by hand", i.e. without using tactic.trace.
The original motivation was to be able to compose various tactics with the or else connector and retrieve the code that actually worked (like in the "Try" message). I ended up rewriting all the tactics so that they return their own code. If you are interested, you can have a look at
https://github.com/dEAduction/dEAduction-lean/blob/master/src/lean_src_deaduction_synchro/compute3.lean
which contains a bunch of tactics for solving inequalities. (Mostly inefficient for the moment, unfortunately. I would love to have something usable...).