From ce90e986483329c0128660813bc5cef12dc11f7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2022 05:54:54 -0700 Subject: [PATCH] feat: activate new compiler first phase --- src/Lean/CoreM.lean | 4 +-- .../hidingInaccessibleNames.lean.expected.out | 10 +++--- tests/lean/jason1.lean.expected.out | 32 +++++++++---------- .../linterUnusedVariables.lean.expected.out | 4 +-- tests/lean/run/toDeclEtaBug.lean | 10 ++---- 5 files changed, 28 insertions(+), 32 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 89a1d91a4e..df399ad68b 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -295,7 +295,7 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla opaque compileDeclsNew (declNames : List Name) : CoreM Unit def compileDecl (decl : Declaration) : CoreM Unit := do - -- compileDeclsNew (Compiler.getDeclNamesForCodeGen decl) + compileDeclsNew (Compiler.getDeclNamesForCodeGen decl) match (← getEnv).compileDecl (← getOptions) decl with | Except.ok env => setEnv env | Except.error (KernelException.other msg) => @@ -305,7 +305,7 @@ def compileDecl (decl : Declaration) : CoreM Unit := do throwKernelException ex def compileDecls (decls : List Name) : CoreM Unit := do - -- compileDeclsNew decls + compileDeclsNew decls match (← getEnv).compileDecls (← getOptions) decls with | Except.ok env => setEnv env | Except.error (KernelException.other msg) => diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out index eff68a3c28..cb56bfa2a1 100644 --- a/tests/lean/hidingInaccessibleNames.lean.expected.out +++ b/tests/lean/hidingInaccessibleNames.lean.expected.out @@ -10,11 +10,6 @@ hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize plac context: : [] ≠ [] ⊢ Nat -hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder -context: -a b x✝¹ : Nat -: [a, b] ≠ [] -⊢ Nat hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder context: x✝¹ : Nat @@ -26,6 +21,11 @@ x✝² : List Nat x✝¹ : Nat : x✝² ≠ [] ⊢ Nat +hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder +context: +a b x✝¹ : Nat +: [a, b] ≠ [] +⊢ Nat case inl p q : Prop : p diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out index 94a575cf04..7022bdeaca 100644 --- a/tests/lean/jason1.lean.expected.out +++ b/tests/lean/jason1.lean.expected.out @@ -1,3 +1,17 @@ +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 +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +Γ✝ : G +⊢ G jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument @TySyntaxLayer.arrow G T EG getCtx (getCtx @@ -30,20 +44,6 @@ 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 Γ✝) -context: -G T Tm : Type -EG : G → G → Type -ET : T → T → Type -ETm : Tm → Tm → Type -EGrfl : {Γ : G} → EG Γ Γ -getCtx : T → G -getTy : Tm → T -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 @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝) context: @@ -108,8 +108,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 diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out index 3c07a0dfe0..2391423ea9 100644 --- a/tests/lean/linterUnusedVariables.lean.expected.out +++ b/tests/lean/linterUnusedVariables.lean.expected.out @@ -1,5 +1,5 @@ -linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x` [linter.unusedVariables] +linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables] @@ -12,8 +12,8 @@ linterUnusedVariables.lean:51:11-51:12: warning: unused variable `z` [linter.unu linterUnusedVariables.lean:56:14-56:15: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:62:20-62:21: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:67:34-67:38: warning: unused variable `inst` [linter.unusedVariables] -linterUnusedVariables.lean:109:6-109:7: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:108:25-108:26: warning: unused variable `x` [linter.unusedVariables] +linterUnusedVariables.lean:109:6-109:7: warning: unused variable `y` [linter.unusedVariables] linterUnusedVariables.lean:115:6-115:7: warning: unused variable `a` [linter.unusedVariables] linterUnusedVariables.lean:125:26-125:27: warning: unused variable `z` [linter.unusedVariables] linterUnusedVariables.lean:133:9-133:10: warning: unused variable `h` [linter.unusedVariables] diff --git a/tests/lean/run/toDeclEtaBug.lean b/tests/lean/run/toDeclEtaBug.lean index a0a0688dbd..2f03606e26 100644 --- a/tests/lean/run/toDeclEtaBug.lean +++ b/tests/lean/run/toDeclEtaBug.lean @@ -8,12 +8,8 @@ open Lean Compiler LCNF Testing else x + 2 +-- TODO: uncomment after the new compiler is executed by default +-- @[cpass] def cseSizeTest : PassInstaller := Testing.assertNoFun |>.install `specialize `noFun + def g (c : Nat) : Nat := f true false c - -#eval Lean.Compiler.compile #[``g] - -@[cpass] def cseSizeTest : PassInstaller := Testing.assertNoFun |>.install `specialize `noFun - -set_option trace.Compiler.result true -#eval Lean.Compiler.compile #[``g]