fix: meta should trump noncomputable section

Author: Kha

src/Lean/Elab/PreDefinition/Basic.lean

@@ -135,7 +135,10 @@ private def shouldGenCodeFor (preDef : PreDefinition) : Bool :=
   !preDef.kind.isTheorem && !preDef.modifiers.isNoncomputable
 
 private def compileDecl (decl : Declaration) : TermElabM Unit := do
-  Lean.compileDecl (logErrors := !(← read).isNoncomputableSection) decl
+  Lean.compileDecl
+    -- `meta` should disregard `noncomputable section`
+    (logErrors := !(← read).isNoncomputableSection || decl.getTopLevelNames.any (isMeta (← getEnv)))
+    decl
 
 register_builtin_option diagnostics.threshold.proofSize : Nat := {
   defValue := 16384

tests/pkg/module/Module/Basic.lean

@@ -496,3 +496,7 @@ Note: A private declaration `S.s` (from the current module) exists but would nee
 -/
 #guard_msgs in
 @[expose] public def useS (s : S) := s.s
+
+noncomputable section
+meta def m := S.s
+end