chore: do not interpret meta as noncomputable (#8668)

To be replaced by actual handling of `meta`

Author: Kha

src/Lean/Elab/DeclModifiers.lean

@@ -132,7 +132,13 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
   let docCommentStx := stx.raw[0]
   let attrsStx      := stx.raw[1]
   let visibilityStx := stx.raw[2]
-  let noncompStx    := stx.raw[3]
+  let isNoncomputable :=
+    if stx.raw[3].isNone then
+      false
+    else if stx.raw[3][0].getKind == ``Parser.Command.meta then
+      false  -- TODO: handle `meta` declarations
+    else
+      true
   let unsafeStx     := stx.raw[4]
   let recKind       :=
     if stx.raw[5].isNone then
@@ -155,7 +161,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
   return {
     stx, docString?, visibility, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
-    isNoncomputable := !noncompStx.isNone
+    isNoncomputable
   }
 
 /--

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear bot, please update stage 0
+
 namespace lean {
 options get_default_options() {
     options opts;