chore: fix tests after hash change

bollu · Dec 2, 2022 · a67a508 · a67a508
1 parent c83e33b
commit a67a508
Show file tree

Hide file tree

Showing 15 changed files with 92 additions and 92 deletions.
diff --git a/tests/compiler/expr.lean.expected.out b/tests/compiler/expr.lean.expected.out
@@ -1,3 +1,3 @@
 f a b
-hash: 3375555335
+hash: 2008687407
 #[a, b]
diff --git a/tests/lean/217.lean.expected.out b/tests/lean/217.lean.expected.out
@@ -1,6 +1,6 @@
-217.lean:5:30-5:31: error: don't know how to synthesize placeholder for argument 'init'
-context:
-⊢ CoreM Unit
 217.lean:5:28-5:29: error: don't know how to synthesize placeholder for argument 'f'
 context:
 ⊢ CoreM Unit → Name → ConstantInfo → CoreM Unit
+217.lean:5:30-5:31: error: don't know how to synthesize placeholder for argument 'init'
+context:
+⊢ CoreM Unit
diff --git a/tests/lean/CompilerElimDeadBranches.lean.expected.out b/tests/lean/CompilerElimDeadBranches.lean.expected.out
@@ -1,17 +1,17 @@
-[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
-      ("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
+[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
+      ("_x.36",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
       ("_x.37",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor
          `Option.some
          #[Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]]),
-      ("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.36",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
+      ("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[])]
 [Compiler.elimDeadBranches] Threw away cases _x.37 branch Option.none
 [Compiler.elimDeadBranches] Threw away cases _x.37 branch Option.none
-[Compiler.elimDeadBranches] Eliminating addSomeVal with #[("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.38",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
+[Compiler.elimDeadBranches] Eliminating addSomeVal with #[("_x.38",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
 [Compiler.elimDeadBranches] size: 11
     def addSomeVal._redArg : Option Nat :=
       let _x.1 := someVal._redArg;
@@ -47,21 +47,21 @@
           let _x.5 := some _ _x.4;
           return _x.5
 [Compiler.result] size: 1 def addSomeVal x : Option Nat := let _x.1 := addSomeVal._redArg; return _x.1
-[Compiler.elimDeadBranches] Eliminating monadic with #[("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+[Compiler.elimDeadBranches] Eliminating monadic with #[("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.205",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
       ("_x.91",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
       ("_x.212",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.211",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
       ("_x.207",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("_x.205",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
+      ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.211",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
 [Compiler.elimDeadBranches] Threw away cases _x.211 branch Option.none
 [Compiler.elimDeadBranches] Threw away cases _x.212 branch Option.none
 [Compiler.elimDeadBranches] Threw away cases _x.205 branch Except.ok

diff --git a/tests/lean/argNameAtPlaceholderError.lean.expected.out b/tests/lean/argNameAtPlaceholderError.lean.expected.out
@@ -1,11 +1,11 @@
-argNameAtPlaceholderError.lean:8:15-8:16: error: don't know how to synthesize placeholder for argument 'catchExPostpone'
-context:
-stx : Syntax
-⊢ Bool
 argNameAtPlaceholderError.lean:8:13-8:14: error: don't know how to synthesize placeholder for argument 'expectedType?'
 context:
 stx : Syntax
 ⊢ Option Expr
+argNameAtPlaceholderError.lean:8:15-8:16: error: don't know how to synthesize placeholder for argument 'catchExPostpone'
+context:
+stx : Syntax
+⊢ Bool
 argNameAtPlaceholderError.lean:8:11-8:12: error: don't know how to synthesize placeholder for argument 'stx'
 context:
 stx : Syntax

diff --git a/tests/lean/derivingHashable.lean.expected.out b/tests/lean/derivingHashable.lean.expected.out
@@ -1,4 +1,4 @@
-10047522373567521337
+12653447106063628298
 18299533346889728271
 5501096720095961210
 6693367456468911342
diff --git a/tests/lean/evalNone.lean.expected.out b/tests/lean/evalNone.lean.expected.out
@@ -2,11 +2,11 @@ evalNone.lean:1:6-1:10: error: don't know how to synthesize implicit argument
   @none ?m
 context:
 ⊢ Type ?u
-evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
-  @List.nil ?m
-context:
-⊢ Type ?u
 evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
   @List.head? ?m []
 context:
 ⊢ Type ?u
+evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+⊢ Type ?u
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
@@ -1,11 +1,11 @@
 Sum.someRight c : Option Nat
-evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
-  @c ?m
-context:
-⊢ Type ?u
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m Nat c
 context:
 ⊢ Type ?u
+evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
+  @c ?m
+context:
+⊢ Type ?u
 Sum.someRight c : Option Nat
 Sum.someRight c : Option Nat
diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out
@@ -14,6 +14,11 @@ context:
 x✝¹ : Nat
 x✝ : [] ≠ []
 ⊢ Nat
+hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
+context:
+a b x✝¹ : Nat
+x✝ : [a, b] ≠ []
+⊢ Nat
 hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
 context:
 x✝¹ : Nat
@@ -25,11 +30,6 @@ x✝² : List Nat
 x✝¹ : Nat
 x✝ : x✝² ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
-context:
-a b x✝¹ : Nat
-x✝ : [a, b] ≠ []
-⊢ Nat
 case inl
 p q : Prop
 h✝ : p

diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
@@ -1,24 +1,24 @@
+holeErrors.lean:3:11-3:20: error: failed to infer definition type
 holeErrors.lean:3:14-3:20: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
-holeErrors.lean:3:11-3:20: error: failed to infer definition type
 holeErrors.lean:5:9-5:10: error: failed to infer definition type
 when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
-holeErrors.lean:7:11-9:1: error: failed to infer definition type
 holeErrors.lean:8:9-8:15: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
+holeErrors.lean:7:11-9:1: error: failed to infer definition type
 holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
-holeErrors.lean:11:8-11:9: error: failed to infer binder type
 holeErrors.lean:11:11-11:15: error: failed to infer definition type
+holeErrors.lean:11:8-11:9: error: failed to infer binder type
 holeErrors.lean:13:12-13:13: error: failed to infer binder type
 holeErrors.lean:13:15-13:19: error: failed to infer definition type
-holeErrors.lean:15:7-16:10: error: failed to infer definition type
 holeErrors.lean:16:4-16:5: error: failed to infer binder type
+holeErrors.lean:15:7-16:10: error: failed to infer definition type
+holeErrors.lean:19:8-19:9: error: failed to infer 'let rec' declaration type
 holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
-holeErrors.lean:19:8-19:9: error: failed to infer 'let rec' declaration type
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
@@ -1,12 +1,6 @@
 holes.lean:4:4-4:7: error: placeholders '_' cannot be used where a function is expected
-holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
-  @g Nat (?m x) x
-context:
-x : Nat
-⊢ Type
-holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
+holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
 context:
-case hole
 x : Nat
 y : Nat := g x + g x
 ⊢ Nat
@@ -15,19 +9,25 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
 context:
 x : Nat
 ⊢ Type
-holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
+holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
+  @g Nat (?m x) x
 context:
 x : Nat
+⊢ Type
+holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
+context:
+case hole
+x : Nat
 y : Nat := g x + g x
 ⊢ Nat
 holes.lean:13:10-13:11: error: failed to infer binder type
 holes.lean:15:16-15:17: error: failed to infer binder type
-holes.lean:18:9-18:10: error: failed to infer binder type
 holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
   @f Nat (?m a) a
 context:
 a : Nat
 f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a
 ⊢ ?m a
+holes.lean:18:9-18:10: error: failed to infer binder type
 holes.lean:21:25-22:4: error: failed to infer definition type
 holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type
diff --git a/tests/lean/interactive/userWidget.lean.expected.out b/tests/lean/interactive/userWidget.lean.expected.out
@@ -4,7 +4,7 @@
     "end": {"line": 13, "character": 31}},
    "props": {},
    "name": "my fancy widget",
-   "javascriptHash": "2248127894",
+   "javascriptHash": "11948876261158841348",
    "id": "widget1"}]}
 {"sourcetext":
  "\n  import * as React from 'react';\n  export default function (props) {\n    return React.createElement('p', {}, 'hello')\n  }"}
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
@@ -1,23 +1,9 @@
-jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.arrow G T EG getCtx
+jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
+  @EGrfl
     (getCtx
       (TAlgebra
         (@TySyntaxLayer.nat G T EG getCtx
           (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -30,12 +16,8 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -48,8 +30,26 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.arrow G T EG getCtx
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -62,8 +62,8 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -76,7 +76,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
@@ -90,7 +90,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
@@ -104,7 +104,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
+jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
   @EGrfl
     (getCtx
       (TAlgebra

diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@@ -13,16 +13,16 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
-syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
-context:
-α β : Type
-x : Fam2 α β
-n a : Nat
-⊢ Nat
 syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
 x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
+syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
+context:
+α β : Type
+x : Fam2 α β
+n a : Nat
+⊢ Nat
diff --git a/tests/pkg/user_ext/UserExt/FooExt.lean b/tests/pkg/user_ext/UserExt/FooExt.lean
@@ -21,5 +21,5 @@ open Lean.Elab.Command
   IO.println s!"inserting {stx[1].getId}"
   modifyEnv fun env => fooExtension.addEntry env stx[1].getId
 
-@[command_elab showFoo] def elabShowFoo : CommandElab := fun stx => do
-  IO.println s!"foo set: {fooExtension.getState (← getEnv) |>.toList}"
+@[command_elab showFoo] def elabShowFoo : CommandElab := fun _ => do
+  IO.println s!"foo set: {fooExtension.getState (← getEnv) |>.toArray |>.qsort Name.lt}"
diff --git a/tests/pkg/user_ext/test.sh b/tests/pkg/user_ext/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 
 rm -rf build
-lake build -v 2>&1 | grep 'hello, world, test'
+lake build -v 2>&1 | grep 'hello, test, world'