Global var in MetaM

Stream: lean4

[Cody Roux]

I want to be very naughty, and introduce a global variable somewhere in my MetaM code. Can this be done?

[Thomas Murrills]

I think you might be looking for IO.Ref (and IO.mkRef, .get, .modify, .set), but don't tell anyone I told you...

However, you do need to have access to the ref. If you want to introduce it somewhere and read it somewhere completely different, where it's not in scope, you're out of luck—but you can introduce it via initialize myRef : IO.Ref _ <- IO.mkRef _ at the start of elaboration, and then everything has access to it. But note that this will not behave well interactively, as it's never reset when you edit part of a file!

[Chris Henson]

Can you (ab)use Lean.EnvExtension maybe?

[Thomas Murrills]

You might also want to consider running in a StateRefT MyState MetaM _ monad depending on how global the variable should be exactly.

[Cody Roux]

Sweet! I'll try this. Not sure I understand the scope comment though. Can't I declare the Ref as a def? (That was fun to say)

[Thomas Murrills]

Using initialize will be what you want there! That declares it as a def (in the file it's written) and sets it up when elaboration starts (in any downstream files). Note the <-: that monadically creates the ref in IO ("setting it up"), which is what you need. A def couldn't do that.

[Cody Roux]

I see. I'll try this, but I'd also love to hear about the EnvExtension abuse.

[Thomas Murrills]

EnvExtension (ab)use would probably work too! I think it would have the advantage of working correctly interactively, but the potential disadvantage of destroying async performance if this env extension had to be accessed on the global environment branch (to be truly "global"). (Note that this also involves initializing the env extension itself in a similar way, but the updates/accesses are different in nature.)

[Chris Henson]

Yeah, I basically had in mind that depending on the complexity of your use case it eventually boils down to something using IO.Ref, so it could be simpler.