Detecting if interactive

Stream: metaprogramming / tactics

[Joe Hendrix]

Is there a way to reliably detect whether the meta program is interactive (i.e., in the IDE)?

I have a pre-caching task for an interactive tactic that I could launch in PersistentEnvExtension.addImportedFn, but I only want to do that if it's an interactive session since otherwise it would unnecessarily slow down the build.

[Mario Carneiro]

in theory that's what (← getInfoState).enabled is for

[Mario Carneiro]

but last I heard it is now always enabled because something breaks without it

[Mario Carneiro]

https://github.com/leanprover/lean4/pull/1146

[Mario Carneiro]

One thing you could do is to use a Thunk to compute the data only when it is first requested. In a noninteractive build it never will be so it's a perf win

[Mario Carneiro]

This trick was recently used in #8199

[Joe Hendrix]

Thanks. I was hoping to use this to experiment with starting cache initialization prior to needing the tactic, but that also means every interactive session would have work that isn't needed.
I'm going to see if I can further speed things up prior to exploring this further.