max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: activate new compiler first phase

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-23 05:54:54 -07:00
parent 33fdde9b22
commit ce90e98648
5 changed files with 28 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/CoreM.lean
View file

@ -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) =>

10
tests/lean/hidingInaccessibleNames.lean.expected.out
View file

@ -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

32
tests/lean/jason1.lean.expected.out
View file

@ -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

4
tests/lean/linterUnusedVariables.lean.expected.out
View file

@ -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]

10
tests/lean/run/toDeclEtaBug.lean
View file

@ -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]