Why notations are not pretty-printed?

Stream: Is there code for X?

[Yicheng Tao]

import Lean
import Lean.Data.Json.FromToJson
import Lean.Elab.BuiltinCommand
import Lean.Meta.Basic
import Lean.Message

open Lean Elab Term Meta Std Core

def getTypeStr (n : Name) := do
  let inf ← getConstInfo n
  let t := inf.type
  let dat ← ppExpr t
  println! dat
  return s!"{dat.pretty 100000000000000}"

unsafe def test : IO String :=
  withImportModules #[{module := `Init}] {} fun env => do
  let (str, _, _) ← (TermElabM.run' (getTypeStr `Nat.add_zero)).toIO {fileName := default, fileMap := default} {env := env}
  return str

#eval test
#eval getTypeStr `Nat.add_zero

Why the notations are not pretty-printed when using TermElabM.run'? Are some options being overided here? Where can I set the pretty-print options?

[Kyle Miller]

Pretty printer information is stored in environment extensions, and withImportModules appears to use (loadExts := false). Maybe try making your own version of that function that loads extensions? (Maybe doing this is unsafe for some reason, I'm not sure.)

[Eric Wieser]

docs#Lean.withImportModules explains why things are the way that they are

[Eric Wieser]

This is new in lean4#6325 (4.20.0)

[Yicheng Tao]

Find some information and solution here https://github.com/cmu-l3/ntp-toolkit/blob/main/TrainingData/Utils/WithImports.lean

[Yicheng Tao]

Kyle Miller said:

Pretty printer information is stored in environment extensions, and withImportModules appears to use (loadExts := false). Maybe try making your own version of that function that loads extensions? (Maybe doing this is unsafe for some reason, I'm not sure.)

It seems that set loadExts := true works.