Zulip Chat Archive

Stream: general

Topic: Attaching information to tactics


view this post on Zulip Jason Rute (Oct 04 2020 at 01:22):

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.)

view this post on Zulip Jason Rute (Oct 04 2020 at 01:26):

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.

view this post on Zulip Bryan Gin-ge Chen (Oct 04 2020 at 01:38):

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.

view this post on Zulip Jason Rute (Oct 04 2020 at 01:48):

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.

view this post on Zulip Jason Rute (Oct 04 2020 at 01:49):

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.)

view this post on Zulip Jason Rute (Oct 04 2020 at 02:07):

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.)


Last updated: May 13 2021 at 21:12 UTC