fix: mark failed compilations as noncomputable (#12625)

This PR ensures that failure in initial compilation marks the relevant
definitions as `noncomputable`, inside and outside `noncomputable
section`, so that follow-up errors/noncomputable markings are detected
in initial compilation as well instead of somewhere down the pipeline.

This may require additional `noncomputable` markers on definitions that
depend on definitions inside `noncomputable section` but accidentally
passed the new computability check.

Reported at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Cryptic.20error.20message.20in.20new.20lean.20toolchain.3F.

src/Lean/Compiler/NoncomputableAttr.lean

@@ -12,7 +12,8 @@ public section
 
 namespace Lean
 
-builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension
+-- `sync` as it's written to from both main branch and codegen branch
+builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension (asyncMode := .sync)
 
 /-- Mark in the environment extension that the given declaration has been declared by the user as `noncomputable`. -/
 def addNoncomputable (env : Environment) (declName : Name) : Environment :=
@@ -21,7 +22,7 @@ def addNoncomputable (env : Environment) (declName : Name) : Environment :=
 /--
 Returns `true` when the given declaration is tagged `noncomputable`.
 -/
-def isNoncomputable (env : Environment) (declName : Name) : Bool :=
-  noncomputableExt.isTagged env declName
+def isNoncomputable (env : Environment) (declName : Name) (asyncMode := noncomputableExt.toEnvExtension.asyncMode) : Bool :=
+  noncomputableExt.isTagged (asyncMode := asyncMode) env declName
 
 end Lean

src/Lean/CoreM.lean

@@ -10,6 +10,7 @@ public import Lean.Util.RecDepth
 public import Lean.ResolveName
 public import Lean.Language.Basic
 import Init.While
+import Lean.Compiler.NoncomputableAttr
 
 public section
 
@@ -741,6 +742,8 @@ where doCompile := do
       compileDeclsImpl decls
     catch e =>
       state.restore
+      for decl in decls do
+        modifyEnv (addNoncomputable · decl)
       if logErrors then
         throw e
 

src/Lean/Elab/PreDefinition/Basic.lean

@@ -217,7 +217,7 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     match preDef.modifiers.computeKind with
     -- Tags may have been added by `elabMutualDef` already, but that is not the only caller
     | .meta          => if !isMarkedMeta (← getEnv) preDef.declName then modifyEnv (markMeta · preDef.declName)
-    | .noncomputable => if !isNoncomputable (← getEnv) preDef.declName then modifyEnv (addNoncomputable · preDef.declName)
+    | .noncomputable => if !isNoncomputable (asyncMode := .local) (← getEnv) preDef.declName then modifyEnv (addNoncomputable · preDef.declName)
     | _              =>
       if !preDef.kind.isTheorem then
         modifyEnv (markNotMeta · preDef.declName)

src/Lean/EnvExtension.lean

@@ -97,6 +97,8 @@ def mkTagDeclarationExtension (name : Name := by exact decl_name%)
     addEntryFn    := fun s n => s.insert n,
     toArrayFn     := fun es => es.toArray.qsort Name.quickLt
     asyncMode
+    replay?       := some <|
+      SimplePersistentEnvExtension.replayOfFilter (!·.contains ·) (·.insert ·)
   }
 
 namespace TagDeclarationExtension

tests/lean/noncompSection.lean

@@ -1,43 +0,0 @@
-noncomputable section
-
-theorem ex : ∃ x : Nat, x > 0 :=
-  ⟨1, by decide⟩
-
-def a : Nat := Classical.choose ex
-
-def b : Nat := 0
-
-abbrev c : Nat := Classical.choose ex
-
-abbrev d : Nat := 1
-
-/-
-TODO: fix compiler pre check
-
-instance e : Inhabited Nat :=
- ⟨a⟩
--/
-
-instance f : Inhabited Nat :=
- ⟨b⟩
-
-#eval b + d + f.default
-
-section Foo
-
-def g : Nat := Classical.choose ex
-
-/-
-TODO: fix compiler pre-check
-
-def h (x : Nat) : Nat :=
-  match x with
-  | 0 => a
-  | x+1 => h x + 1
--/
-
-end Foo
-
-end
-
-def i : Nat := Classical.choose ex -- Error

tests/lean/run/noncompSection.lean

@@ -0,0 +1,51 @@
+noncomputable section
+
+theorem ex : ∃ x : Nat, x > 0 :=
+  ⟨1, by decide⟩
+
+def a : Nat := Classical.choose ex
+
+def b : Nat := 0
+
+abbrev c : Nat := Classical.choose ex
+
+abbrev d : Nat := 1
+
+instance e : Inhabited Nat :=
+ ⟨a⟩
+
+instance f : Inhabited Nat :=
+ ⟨b⟩
+
+#eval b + d + f.default
+
+section Foo
+
+def g : Nat := Classical.choose ex
+
+def h (x : Nat) : Nat :=
+  match x with
+  | 0 => a
+  | x+1 => h x + 1
+
+end Foo
+
+end
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choose', which is 'noncomputable'
+-/
+#guard_msgs in
+def i : Nat := Classical.choose ex
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'g', which is 'noncomputable'
+-/
+#guard_msgs in
+def j : Nat := g
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'i', which is 'noncomputable'
+-/
+#guard_msgs in
+def k : Nat := i

tests/pkg/module/Module/Basic.lean

@@ -431,6 +431,10 @@ inst✝
 
 public meta def pubMeta := 1
 
+/-- error: Invalid `meta` definition `veryMeta`, `f` not marked `meta` -/
+#guard_msgs in
+meta def veryMeta := f
+
 /-! `#eval` should accept `meta` and non-`meta`. -/
 
 meta def fmeta := 1

tests/pkg/module/Module/MetaImported.lean

@@ -9,10 +9,6 @@ error: Invalid definition `nonMeta`, may not access declaration `f` imported as
 #guard_msgs in
 def nonMeta := f
 
-/-- error: Invalid `meta` definition `veryMeta`, `nonMeta` not marked `meta` -/
-#guard_msgs in
-meta def veryMeta := nonMeta
-
 /--
 error: Invalid public `meta` definition `pubMetaImp`, `pubMeta` is not accessible here; consider adding `public import Module.Basic`
 -/