feat: activate new pretty printer

src/Lean/PrettyPrinter.lean

@@ -37,8 +37,7 @@ let pp : MetaM Format := adaptExcept (fun ex => match ex with
 (fmt, _, _) ← pp.toIO { options := ppCtx.opts } { env := ppCtx.env } { lctx := ppCtx.lctx } { mctx := ppCtx.mctx };
 pure fmt
 
--- TODO: activate when ready
-/-@[init]-/ def registerPPTerm : IO Unit := do
+@[init] def registerPPTerm : IO Unit := do
 ppExprFnRef.set ppExprFn
 
 @[init] private def regTraceClasses : IO Unit := do

tests/lean/appParserIssue.lean.expected.out

@@ -1,5 +1,5 @@
-f 1 (fun (x : Nat) => x) : Nat
-f 1 (fun (x : Nat) => x) : Nat
-f 1 (fun (x : Nat) => x) : Nat
-f 1 (fun (x : Nat) => x) : Nat
-f 1 (fun (x : Nat) => x) : Nat
+f 1 fun (x : Nat) => x : Nat
+f 1 fun (x : Nat) => x : Nat
+f 1 fun (x : Nat) => x : Nat
+f 1 fun (x : Nat) => x : Nat
+f 1 fun (x : Nat) => x : Nat

tests/lean/auxDeclIssue.lean.expected.out

@@ -2,7 +2,7 @@ auxDeclIssue.lean:5:3: error: tactic 'assumption' failed,
 ⊢ False
 auxDeclIssue.lean:11:2: error: tactic 'subst' failed, did not find equation for eliminating 'x'
 x y : Nat
-⊢ x=y
+⊢ x = y
 auxDeclIssue.lean:18:3: error: tactic 'assumption' failed, 
 ex1 : False
 ⊢ False

tests/lean/emptyc.lean.expected.out

@@ -1,4 +1,4 @@
 emptyc.lean:19:0: error: ambiguous, possible interpretations 
-  {x := 0}
+  { x := 0 }
   
-  ∅
+  HasEmptyc.emptyc

tests/lean/evalWithMVar.lean.expected.out

@@ -2,10 +2,10 @@ Sum.someRight c : Option Nat
 evalWithMVar.lean:13:6: error: don't know how to synthesize placeholder
   @Sum.someRight ?m … …
 context:
-⊢ Type ?
+⊢ Type _
 evalWithMVar.lean:13:20: error: don't know how to synthesize placeholder
   @c ?m
 context:
-⊢ Type ?
+⊢ Type _
 Sum.someRight c : Option Nat
 Sum.someRight c : Option Nat

tests/lean/holes.lean.expected.out

@@ -3,12 +3,12 @@ holes.lean:11:8: error: don't know how to synthesize placeholder
 context:
 case hole
 x : Nat
-y : Nat := g x+g x
+y : Nat := g x + g x
 ⊢ Nat
 holes.lean:11:4: error: don't know how to synthesize placeholder
 context:
 x : Nat
-y : Nat := g x+g x
+y : Nat := g x + g x
 ⊢ Nat
 holes.lean:10:15: error: don't know how to synthesize placeholder
   @g … ?m …
@@ -23,27 +23,27 @@ x : Nat
 holes.lean:13:7: error: don't know how to synthesize placeholder
 context:
 α : Sort u_1
-⊢ Sort ?
+⊢ Sort _
 holes.lean:15:16: error: don't know how to synthesize placeholder
 context:
 α : Sort u_1
-⊢ Sort ?
+⊢ Sort _
 holes.lean:19:0: error: don't know how to synthesize placeholder
   @_uniq.125 … ?m …
 context:
 a : Nat
-f : ∀ {α : Type} {β : ?m a}, α → α := fun {α : Type} {β : ?m a} (a : α) => a
+f : {α : Type} → {β : ?m a} → α → α := fun {α : Type} (a_1 : α) => a_1
 ⊢ ?m a
 holes.lean:18:6: error: don't know how to synthesize placeholder
 context:
 a : Nat
 α : Type
-⊢ Sort ?
+⊢ Sort _
 holes.lean:21:25: error: don't know how to synthesize placeholder
 context:
 x : Nat
-⊢ Sort ?
+⊢ Sort _
 holes.lean:25:8: error: don't know how to synthesize placeholder
 context:
 x y : Nat
-⊢ Sort ?
+⊢ Sort _

tests/lean/inductive1.lean.expected.out

@@ -27,4 +27,4 @@ inductive1.lean:105:0: error: unexpected constructor resulting type, type expect
 inductive1.lean:108:0: error: unexpected constructor resulting type
   Nat
 inductive1.lean:118:7: error: unknown identifier 'cons'
-(sorryAx ?m) : ?m
+sorryAx ?m : ?m

tests/lean/match1.lean.expected.out

@@ -16,6 +16,6 @@ expected type
   VecPred P tail
 [false, true, true]
 match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found 
-  .(j+j)
+  .(j + j)
 constructor expected
 [false, true, true]

tests/lean/matchErrorLocation.lean.expected.out

@@ -5,4 +5,4 @@ has type
 but it is expected to have type
   α
 failed to synthesize instance
-  CoeT False _ α
+  CoeT False (h he) α

tests/lean/namedHoles.lean.expected.out

@@ -8,13 +8,13 @@ but is expected to have type
   Bool
 failed to synthesize instance
   CoeT Nat ?m Bool
-(sorryAx ?m) : ?m
+sorryAx ?m : ?m
 g ?m ?m : Nat
 20
 foo (fun (x : Nat) => ?m x) ?m : Nat
-bla ?m (fun (x : Nat) => ?m) : Nat
+bla ?m fun (x : Nat) => ?m : Nat
 namedHoles.lean:35:38: error: synthetic hole has already been defined with an incompatible local context
-boo (fun (x : Nat) => ?m x) (fun (y : Bool) => (sorryAx Nat)) : Nat
+boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorryAx Nat : Nat
 11
 12
 namedHoles.lean:58:26: error: synthetic hole has already been defined and assigned to value incompatible with the current context

tests/lean/openExport.lean.expected.out

@@ -1,15 +1,15 @@
-A.x : Nat
-B.y : Nat
-A.x : Nat
-A.x : Nat
+x : Nat
+y : Nat
+B.x : Nat
+B.x : Nat
 B.y : Nat
 openExport.lean:19:7: error: unknown identifier 'x'
-(sorryAx ?m) : ?m
+sorryAx ?m : ?m
 openExport.lean:20:7: error: unknown identifier 'y'
-(sorryAx ?m) : ?m
-A.x : Nat
-B.y : Nat
-A.x : Nat
-B.y : Nat
-B.z : Nat
-B.z : Nat
+sorryAx ?m : ?m
+x : Nat
+y : Nat
+x : Nat
+y : Nat
+z : Nat
+z : Nat

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -1,17 +1,17 @@
 phashmap_inst_coherence.lean:12:6: error: application type mismatch
-  Std.PersistentHashMap.find? m
+  PersistentHashMap.find? m
 argument
   m
 has type
-  Std.PersistentHashMap Nat Nat
+  PersistentHashMap Nat Nat
 but is expected to have type
-  Std.PersistentHashMap Nat Nat
+  PersistentHashMap Nat Nat
 failed to synthesize instance
-  CoeT (Std.PersistentHashMap Nat Nat) m (Std.PersistentHashMap Nat Nat)
+  CoeT (PersistentHashMap Nat Nat) m (PersistentHashMap Nat Nat)
 phashmap_inst_coherence.lean:12:0: error: application type mismatch
   Lean.runEval (sorryAx ?m)
 argument
-  (sorryAx ?m)
+  sorryAx ?m
 has type
   ?m
 but is expected to have type

tests/lean/precissues.lean.expected.out

@@ -1,20 +1,20 @@
-id (fun (x : ?m) => x) : ?m → ?m
+id fun (x : ?m) => x : ?m → ?m
 0 : Nat
-f 1 (fun (x : Nat) => x) : Nat
+f 1 fun (x : Nat) => x : Nat
 0 : Nat
-f 1 (fun (x : Nat) => x) : Nat
+f 1 fun (x : Nat) => x : Nat
 id : ?m → ?m
 precissues.lean:15:10: error: expected command
 1 : Nat
 id ((fun (this : True) => this) True.intro) : True
-0=(fun (this : Nat) => this) 1 : Prop
-0=let x : Nat := 0; x : Prop
-p↔¬q : Prop
-True=¬False : Prop
-p∧¬q : Prop
-¬p∧q : Prop
-¬p↔q : Prop
-¬p=q : Prop
-¬p=q : Prop
-id (¬p) : Prop
-Nat → ∀ (a : Nat), a=a : Prop
+0 = (fun (this : Nat) => this) 1 : Prop
+0 = let x  : Nat := 0; x : Prop
+p ↔ ¬q : Prop
+True = ¬False : Prop
+p ∧ ¬q : Prop
+¬p ∧ q : Prop
+¬p ↔ q : Prop
+¬p = q : Prop
+¬p = q : Prop
+id ¬p : Prop
+(a a_1 : Nat) → a_1 = a_1 : Prop

tests/lean/private.lean.expected.out

@@ -1,13 +1,13 @@
-Bla.foo=="world" : Bool
+Bla.foo == "world" : Bool
 private.lean:14:12: error: private declaration 'Bla.foo' has already been declared
-foo==0 : Bool
+foo == 0 : Bool
 Bla.foo : String
-Boo.Bla.boo=="world" : Bool
-Boo.Bla.boo++"world" : String
-Boo.Bla.boo=="world" : Bool
-Boo.boo==100 : Bool
-Boo.Bla.boo=="world" : Bool
-Boo.boo==100 : Bool
+Boo.Bla.boo == "world" : Bool
+Boo.Bla.boo ++ "world" : String
+Boo.Bla.boo == "world" : Bool
+boo == 100 : Bool
+Boo.Bla.boo == "world" : Bool
+Boo.boo == 100 : Bool
 Nat.mul10 x : Nat
 private.lean:65:12: error: a non-private declaration 'y' has already been declared
 private.lean:68:4: error: a private declaration 'z' has already been declared

tests/lean/protected.lean.expected.out

@@ -1,10 +1,10 @@
 protected.lean:10:7: error: unknown identifier 'x'
-(sorryAx ?m) : ?m
+sorryAx ?m : ?m
 Foo.x : Nat
-Bla.Foo.y : Nat
+Foo.y : Nat
 protected.lean:22:7: error: unknown identifier 'y'
-(sorryAx ?m) : ?m
-Bla.Foo.z : Nat
+sorryAx ?m : ?m
+z : Nat
 protected.lean:25:14: error: protected declarations must be in a namespace
 protected.lean:28:14: error: unknown identifier 'f'
 8
@@ -13,7 +13,7 @@ protected.lean:47:6: error: unknown identifier 'g'
 protected.lean:47:0: error: application type mismatch
   Lean.runEval (sorryAx ?m)
 argument
-  (sorryAx ?m)
+  sorryAx ?m
 has type
   ?m
 but is expected to have type

tests/lean/server/edits.lean.expected.out

@@ -36,9 +36,9 @@ Content-Length: 221
 
 {"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"expected term"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
 
-{"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 1211
+{"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 1209
 
-{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":16,"character":0},"end":{"line":16,"character":0}},"message":"expected term"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":20,"character":0},"end":{"line":20,"character":0}},"message":"invalid 'end', insufficient scopes"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":22,"character":7},"end":{"line":22,"character":7}},"message":"unknown identifier 'MyNs.u'"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"(sorryAx ?m) : ?m"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 185
+{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":16,"character":0},"end":{"line":16,"character":0}},"message":"expected term"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":20,"character":0},"end":{"line":20,"character":0}},"message":"invalid 'end', insufficient scopes"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":22,"character":7},"end":{"line":22,"character":7}},"message":"unknown identifier 'MyNs.u'"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"sorryAx ?m : ?m"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 185
 
 {"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 740
 

tests/lean/shadow.lean.expected.out

@@ -1,33 +1,33 @@
 shadow.lean:6:0: error: type mismatch
   h
 has type
-  x✝¹=x✝¹
+  x✝¹ = x✝¹
 but it is expected to have type
-  x=x
+  x = x
 failed to synthesize instance
-  CoeT (x✝¹=x✝¹) _ (x=x)
+  CoeT (x✝¹ = x✝¹) h (x = x)
 shadow.lean:10:0: error: type mismatch
   h
 has type
-  x=x
+  x = x
 but it is expected to have type
-  x=x
+  x = x
 failed to synthesize instance
-  CoeT (x=x) _ (x=x)
+  CoeT (x = x) h (x = x)
 shadow.lean:13:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
 inst✝² : Inhabited α
 inst✝¹ inst : α
 β✝¹ δ✝¹ : Type
-⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
+⊢ α → β✝¹ → δ✝¹ → α × β✝¹ × δ✝¹
 shadow.lean:17:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
 inst.16 : Inhabited α
 inst inst : α
 β.41 δ.42 : Type
-⊢ α → β.41 → δ.42 → α×β.41×δ.42
+⊢ α → β._@.shadow._hyg.41 → δ._@.shadow._hyg.42 → α × β._@.shadow._hyg.41 × δ._@.shadow._hyg.42
 shadow.lean:20:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
@@ -37,4 +37,4 @@ b : β
 inst : α
 inst✝¹ : Inhabited α
 β✝¹ δ✝¹ : Type
-⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
+⊢ α → β✝¹ → δ✝¹ → α × β✝¹ × δ✝¹