From 59b4d977b59ce217617c3284a35f414d502b2de9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Sep 2022 15:04:06 -0700 Subject: [PATCH] chore: fix tests --- tests/lean/CompilerFindJoinPoints.lean.expected.out | 1 + tests/lean/run/inlineApp.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/lean/CompilerFindJoinPoints.lean.expected.out b/tests/lean/CompilerFindJoinPoints.lean.expected.out index 9b58e211af..4df1bda51c 100644 --- a/tests/lean/CompilerFindJoinPoints.lean.expected.out +++ b/tests/lean/CompilerFindJoinPoints.lean.expected.out @@ -1,3 +1,4 @@ + [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 [Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 successful [Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurence 0 diff --git a/tests/lean/run/inlineApp.lean b/tests/lean/run/inlineApp.lean index edc720fbdb..85f8377ca7 100644 --- a/tests/lean/run/inlineApp.lean +++ b/tests/lean/run/inlineApp.lean @@ -10,7 +10,7 @@ def h (x : Nat) := open Lean Compiler LCNF in @[cpass] def simpInline : PassInstaller := - Testing.assertDoesNotContainConstAfter `simp `simpInlinesInline ``inline "simp did not inline `inline`" + Testing.assertDoesNotContainConstAfter ``inline "simp did not inline `inline`" |>.install `simp `simpInlinesInline set_option trace.Compiler.result true #eval Lean.Compiler.compile #[``h]