feat: add compileDecl

cc @kha

src/Init/Lean/Elab/Command.lean

@@ -561,10 +561,15 @@ result ++ remaining.toList
 def addDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
 env ← getEnv;
 match env.addDecl decl with
-| Except.ok    env => modify $ fun s => { env := env, .. s }
-| Except.error kex => do
-  opts ← getOptions;
-  throwError ref (kex.toMessageData opts)
+| Except.ok    env => setEnv env
+| Except.error kex => do opts ← getOptions; throwError ref (kex.toMessageData opts)
+
+def compileDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
+env  ← getEnv;
+opts ← getOptions;
+match env.compileDecl opts decl with
+| Except.ok env    => setEnv env
+| Except.error kex => throwError ref (kex.toMessageData opts)
 
 end Command
 end Elab

src/Init/Lean/Elab/Definition.lean

@@ -150,7 +150,7 @@ withDeclId view.declId $ fun name => do
   | some decl => do
     addDecl ref decl;
     applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
-    -- TODO invoke compiler
+    compileDecl ref decl;
     applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
 
 end Command

tests/lean/run/frontend1.lean

@@ -215,3 +215,7 @@ def three := 3
 #eval run "#check g (y := three)"
 #eval run "#check g (z := three)"
 #eval run "#check g three (z := zero)"
+
+#eval run "open Lean.Parser
+@[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! coe \"hi\"
+#check myParser"