Testing behavior as if in Mathlib?

Stream: mathlib4

[Thomas Murrills]

Do we have something like the following #in_module to simulate being within Mathlib when testing Mathlib-only behavior in MathlibTest? (If not, should we?)

import Lean

open Lean Elab Command

elab "#in_module " mod:ident cmd:command : command => do
  withEnv ((← getEnv).setMainModule mod.getId) do
    elabCommandTopLevel cmd

elab "#command_which_violates_mathlib_style" : command => do
  if (← getMainModule).getRoot == `Mathlib then logWarning "I shouldn't be used in Mathlib!"

#in_module Mathlib.Foo
/-- warning: I shouldn't be used in Mathlib! -/
#guard_msgs in
#command_which_violates_mathlib_style

I could have sworn there was a thread about this very thing at one point, but I can no longer find it.

[Robin Arnez]

The only mathlib specific thing I think is the linter.style.header linter. Everything else is linter.mathlibStandardSet and other options in the lakefile.

[Robin Arnez]

So I don't think there's a reason to change the module name (just set the relevant options)

[Thomas Murrills]

Ah, okay. I’m deprecating some syntax (only) within mathlib by modifying its elaboration, and I suppose the real takeaway here is that metaprograms generally should not check if they are in Mathlib (unless necessary to the actual function of the program), and should instead check or introduce a mathlib-specific option in case downstream projects want to maintain mathlib standards.