From cfa4752c4ec89231067f1d701c38bb5d9d1a7ff3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Aug 2024 14:57:46 +0200 Subject: [PATCH] fix tests --- tests/lean/2505.lean.expected.out | 2 +- tests/lean/4089.lean.expected.out | 4 +++- tests/lean/4240.lean.expected.out | 2 +- tests/lean/Process.lean.expected.out | 4 ++-- tests/lean/computedFieldsCode.lean.expected.out | 7 ++++++- tests/lean/csimpAttr.lean.expected.out | 3 ++- tests/lean/csimpAttrAppend.lean.expected.out | 2 +- tests/lean/dbgMacros.lean.expected.out | 4 ++-- tests/lean/doubleReset.lean.expected.out | 2 +- tests/lean/etaReducedMvarAssignments.lean.expected.out | 8 ++++---- tests/lean/listLength.lean.expected.out | 2 +- tests/lean/lit_values.lean.expected.out | 2 +- tests/lean/unboxStruct.lean.expected.out | 2 +- tests/lean/updateExprIssue.lean.expected.out | 1 + 14 files changed, 27 insertions(+), 18 deletions(-) diff --git a/tests/lean/2505.lean.expected.out b/tests/lean/2505.lean.expected.out index 6610d40a3544..98a7adec30c0 100644 --- a/tests/lean/2505.lean.expected.out +++ b/tests/lean/2505.lean.expected.out @@ -1,3 +1,3 @@ +2505.lean:14:0-14:7: warning: declaration uses 'sorry' target : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) target' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) -2505.lean:14:0-14:7: warning: declaration uses 'sorry' diff --git a/tests/lean/4089.lean.expected.out b/tests/lean/4089.lean.expected.out index 9152f7bfa4d2..18c8b0d2e98e 100644 --- a/tests/lean/4089.lean.expected.out +++ b/tests/lean/4089.lean.expected.out @@ -8,6 +8,7 @@ def f (x_1 : obj) : obj := let x_5 : obj := reset[2] x_1; let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2; ret x_4 + [reset_reuse] def Sigma.toProd._rarg (x_1 : obj) : obj := case x_1 : obj of @@ -20,6 +21,7 @@ def Sigma.toProd._rarg (x_1 : obj) : obj := def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj := let x_3 : obj := pap Sigma.toProd._rarg; ret x_3 + [reset_reuse] def foo (x_1 : obj) : obj := case x_1 : obj of @@ -35,4 +37,4 @@ def foo (x_1 : obj) : obj := let x_5 : obj := proj[0] x_3; let x_6 : obj := foo x_4; let x_7 : obj := reuse x_9 in ctor_1[List.cons] x_5 x_6; - ret x_7 \ No newline at end of file + ret x_7 diff --git a/tests/lean/4240.lean.expected.out b/tests/lean/4240.lean.expected.out index 174456c8f3ed..30636e3d3017 100644 --- a/tests/lean/4240.lean.expected.out +++ b/tests/lean/4240.lean.expected.out @@ -23,4 +23,4 @@ def isSomeWithInstanceNat._boxed (x_1 : obj) : obj := let x_2 : u8 := isSomeWithInstanceNat x_1; dec x_1; let x_3 : obj := box x_2; - ret x_3 \ No newline at end of file + ret x_3 diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out index 600e4f2544aa..5d186fa1f4e6 100644 --- a/tests/lean/Process.lean.expected.out +++ b/tests/lean/Process.lean.expected.out @@ -1,6 +1,5 @@ -hi! -:1:0: warning: using 'exit' to interrupt Lean 1 +hi! 0 "ho!\n" "hu!\n" @@ -9,6 +8,7 @@ flush of broken pipe failed 100000 0 0 +:1:0: warning: using 'exit' to interrupt Lean 0 0 none diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out index 10f711f90541..4c2e4c9e17e5 100644 --- a/tests/lean/computedFieldsCode.lean.expected.out +++ b/tests/lean/computedFieldsCode.lean.expected.out @@ -106,6 +106,7 @@ def Exp.hash._override._boxed (x_1 : obj) : obj := dec x_1; let x_3 : obj := box x_2; ret x_3 + [result] def f._closed_1 : obj := let x_1 : u32 := 10; @@ -124,6 +125,7 @@ def f._closed_3 : u64 := def f : u64 := let x_1 : u64 := f._closed_3; ret x_1 + [result] def g (x_1 : @& obj) : u8 := case x_1 : obj of @@ -138,6 +140,7 @@ def g._boxed (x_1 : obj) : obj := dec x_1; let x_3 : obj := box x_2; ret x_3 + [result] def hash' (x_1 : @& obj) : obj := case x_1 : obj of @@ -161,6 +164,7 @@ def hash'._boxed (x_1 : obj) : obj := let x_2 : obj := hash' x_1; dec x_1; ret x_2 + [result] def getAppFn (x_1 : @& obj) : obj := case x_1 : obj of @@ -175,6 +179,7 @@ def getAppFn._boxed (x_1 : obj) : obj := let x_2 : obj := getAppFn x_1; dec x_1; ret x_2 + [result] def Exp.f (x_1 : @& obj) : obj := let x_2 : obj := getAppFn x_1; @@ -182,4 +187,4 @@ def Exp.f (x_1 : @& obj) : obj := def Exp.f._boxed (x_1 : obj) : obj := let x_2 : obj := Exp.f x_1; dec x_1; - ret x_2 \ No newline at end of file + ret x_2 diff --git a/tests/lean/csimpAttr.lean.expected.out b/tests/lean/csimpAttr.lean.expected.out index d69d1215be26..a491585b8c47 100644 --- a/tests/lean/csimpAttr.lean.expected.out +++ b/tests/lean/csimpAttr.lean.expected.out @@ -1,6 +1,7 @@ +csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported. [init] def f (x_1 : obj) : obj := let x_2 : obj := Nat.add x_1 x_1; let x_3 : obj := Nat.add x_2 x_2; - ret x_3csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported. + ret x_3 diff --git a/tests/lean/csimpAttrAppend.lean.expected.out b/tests/lean/csimpAttrAppend.lean.expected.out index 0b7262315971..2e7eac595254 100644 --- a/tests/lean/csimpAttrAppend.lean.expected.out +++ b/tests/lean/csimpAttrAppend.lean.expected.out @@ -3,4 +3,4 @@ def f (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj := let x_4 : obj := List.appendTR._rarg x_1 x_2; let x_5 : obj := List.appendTR._rarg x_4 x_3; - ret x_5 \ No newline at end of file + ret x_5 diff --git a/tests/lean/dbgMacros.lean.expected.out b/tests/lean/dbgMacros.lean.expected.out index 9b70d1b86045..54d6f8756c15 100644 --- a/tests/lean/dbgMacros.lean.expected.out +++ b/tests/lean/dbgMacros.lean.expected.out @@ -1,10 +1,10 @@ PANIC at f dbgMacros:2:14: unexpected zero -PANIC at g dbgMacros:10:14: unreachable code has been reached -PANIC at h dbgMacros:16:0: assertion violation: x != 0 0 9 +PANIC at g dbgMacros:10:14: unreachable code has been reached 0 0 +PANIC at h dbgMacros:16:0: assertion violation: x != 0 0 f2, x: 10 11 diff --git a/tests/lean/doubleReset.lean.expected.out b/tests/lean/doubleReset.lean.expected.out index fce8062bf387..25937761cd2e 100644 --- a/tests/lean/doubleReset.lean.expected.out +++ b/tests/lean/doubleReset.lean.expected.out @@ -34,4 +34,4 @@ def applyProjectionRules._rarg (x_1 : obj) (x_2 : obj) : obj := ret x_5 def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) : obj := let x_4 : obj := pap applyProjectionRules._rarg; - ret x_4 \ No newline at end of file + ret x_4 diff --git a/tests/lean/etaReducedMvarAssignments.lean.expected.out b/tests/lean/etaReducedMvarAssignments.lean.expected.out index 7c743ec28e1d..b85fc4033b1d 100644 --- a/tests/lean/etaReducedMvarAssignments.lean.expected.out +++ b/tests/lean/etaReducedMvarAssignments.lean.expected.out @@ -1,4 +1,4 @@ -Pi.hasLe : LE ((i : ι) → α i) -[Meta.isDefEq.assign] ✅ ?m i := α i - [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i - [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v) +Pi.hasLe : LE ((i : ι) → α i) +[Meta.isDefEq.assign] ✅ ?m i := α i + [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i + [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v) diff --git a/tests/lean/listLength.lean.expected.out b/tests/lean/listLength.lean.expected.out index 311ee817f5b7..ae2f89a73ce5 100644 --- a/tests/lean/listLength.lean.expected.out +++ b/tests/lean/listLength.lean.expected.out @@ -5,4 +5,4 @@ def f (x_1 : obj) : obj := let x_3 : obj := List.lengthTRAux._rarg x_1 x_2; let x_4 : obj := 2; let x_5 : obj := Nat.mul x_4 x_3; - ret x_5 \ No newline at end of file + ret x_5 diff --git a/tests/lean/lit_values.lean.expected.out b/tests/lean/lit_values.lean.expected.out index ee860cc74b8d..20056b796773 100644 --- a/tests/lean/lit_values.lean.expected.out +++ b/tests/lean/lit_values.lean.expected.out @@ -3,10 +3,10 @@ (some 2) (some -2) (some a) +some "hello" (some (⟨5, 3⟩)) (some (⟨12, 0x003#12⟩)) (some 2) (some 2) (some 2) (some 2) -some "hello" diff --git a/tests/lean/unboxStruct.lean.expected.out b/tests/lean/unboxStruct.lean.expected.out index 8d0db228ffe3..feffd3756382 100644 --- a/tests/lean/unboxStruct.lean.expected.out +++ b/tests/lean/unboxStruct.lean.expected.out @@ -7,4 +7,4 @@ def test2._boxed (x_1 : obj) (x_2 : obj) : obj := let x_3 : u32 := unbox x_1; dec x_1; let x_4 : obj := test2 x_3 x_2; - ret x_4 \ No newline at end of file + ret x_4 diff --git a/tests/lean/updateExprIssue.lean.expected.out b/tests/lean/updateExprIssue.lean.expected.out index 10537d1e321f..5e550af5dfa7 100644 --- a/tests/lean/updateExprIssue.lean.expected.out +++ b/tests/lean/updateExprIssue.lean.expected.out @@ -1,4 +1,5 @@ + [init] def sefFn (x_1 : obj) (x_2 : obj) : obj := case x_1 : obj of