non-persistent attributes

Stream: general

[Simon Hudon]

I'm trying to set an attribute inside a proof script and as soon as the proof is done, the attribute seems to disappear. Is this the desired behavior? Is there a way to make the attribute persistent?

[Mario Carneiro]

Theorems can't make permanent modifications to the environment, because they are executed out of order

[Simon Hudon]

Arrrrgh! I'm trying to generate unique file names for caching proof witnesses

[Simon Hudon]

Maybe I should just hash the goal