Elaborator for reading current environment

Stream: lean4

[Anne Baanen]

Is there an elaborator that allows me to read values from the currently-being-elaborated environment? Ideally I want to do something like withEnv% (fun env => myEnvironmentExtension.getState env).

Context: the lint-style script is controlled by the linter options from a project's lakefile. To support linter sets, we need to look in the corresponding environment extension which linters belong to which set. We currently do this by importing a specific file (Mathlib.Tactic.Linter.TextBased) and reading out its environment. But this does not work anymore since lean4#6325, which disables loading extensions in docs#Lean.withImportModules. We can work around this by calling docs#Lean.importModules directly. But maybe there is a better way to do this?

[Sebastian Ullrich]

I would probably suggest writing a one-off elaborator that persists the information into e.g. a generated def?

[Anne Baanen]

Thanks! For future reference, I ended up going with:

/-- Return the linter sets defined at this point of elaborating the current file. -/
elab "linter_sets%" : term => do
  return toExpr <| linterSetsExt.getState (← getEnv)

(After defining a ToExpr LinterSets instance.)