Attaching information to tactics

Stream: general

[Jason Rute]

I’m experimenting with some stuff, and I’d like to know if it is possible to attach arbitrary information (say a list of natural numbers) to the tactic state, so that later tactics can read it. (I see the tactic state has some sort of user data so maybe it is possible with that. It might also be magically possible with meta variables.)

[Jason Rute]

Also, I’m doing something hacky here (for proof recording), so (1) I have to use the built in tactic state instead of passing information in the usual tactic way, and (2) this isn’t something that is supposed to be PRed.

[Bryan Gin-ge Chen]

This isn't exactly what you're asking for, but there are some examples of custom tactic modes linked in this thread, including some where you can store extra data with the tactic state; in particular, rb_map_ts from the Lean tests seems relevant.

[Jason Rute]

Yeah, I trying to avoid that. I want to work with the current tactics (slightly modifying some library code like istep). I want to see some information about what has been run before in that proof.

[Jason Rute]

Actually, I think I can do it with tactic.get_options/tactic.set_options. I can store nat, bool, or string associated with names. I think that should work for my use case. (But I still need to test it out.)

[Jason Rute]

Yes, that works exactly as I want. (Or at least good enough. I can't directly store a list, but I can make a linked list using names as pointers, or serialize a list into a string.)