Introspecting environment extensions

Stream: metaprogramming / tactics

[nrs]

Is it possible to introspect environment extensions from within CoreM? I know that environment extensions can only be registered during initialization, but is any of their data accessible from CoreM? Ultimately the goal is to check the environment extension for parsers to see how to modify it to replace the formatter used by a specific parser.

[nrs]

We can access values of type EnvExtensionState from let env <- getEnv and then considering env.extensions, but I'm not really sure how I could dbg_trace members of the resulting array

[nrs]

import Lean
import Batteries.Tactic.OpenPrivate

open Lean Meta
open private envExtensionsRef from Lean.Environment

abbrev ref := envExtensionsRef -- these are nameless but they are indexed, maybe it has more extensions than persistentEnvExtensionsRef?
abbrev persref := persistentEnvExtensionsRef

def printPersExts : CoreM Unit := do
  for elm in (<- persref.get) do
    println! elm.name
#eval printPersExts

use this to access the state of the extensions in the env