feat: add noncomputable sections

See https://github.com/leanprover-community/mathport/issues/71

src/Lean/Elab/BuiltinCommand.lean

@@ -16,25 +16,25 @@ namespace Lean.Elab.Command
      modifyEnv fun env => addMainModuleDoc env doc
    | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
 
-private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
+private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
     env    := s.env.registerNamespace newNamespace,
-    scopes := { s.scopes.head! with header := header, currNamespace := newNamespace } :: s.scopes
+    scopes := { s.scopes.head! with header := header, currNamespace := newNamespace, isNoncomputable := s.scopes.head!.isNoncomputable || isNoncomputable } :: s.scopes
   }
   pushScope
   if isNewNamespace then
     activateScoped newNamespace
 
-private def addScopes (isNewNamespace : Bool) : Name → CommandElabM Unit
+private def addScopes (isNewNamespace : Bool) (isNoncomputable : Bool) : Name → CommandElabM Unit
   | Name.anonymous => pure ()
   | Name.str p header _ => do
-    addScopes isNewNamespace p
+    addScopes isNewNamespace isNoncomputable p
     let currNamespace ← getCurrNamespace
-    addScope isNewNamespace header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace)
+    addScope isNewNamespace isNoncomputable header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace)
   | _ => throwError "invalid scope"
 
 private def addNamespace (header : Name) : CommandElabM Unit :=
-  addScopes (isNewNamespace := true) header
+  addScopes (isNewNamespace := true) (isNoncomputable := false) header
 
 def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
   addNamespace ns
@@ -60,10 +60,16 @@ private def checkEndHeader : Name → List Scope → Bool
   | `(namespace $n) => addNamespace n.getId
   | _               => throwUnsupportedSyntax
 
-@[builtinCommandElab «section»] def elabSection : CommandElab := fun stx =>
+@[builtinCommandElab «section»] def elabSection : CommandElab := fun stx => do
   match stx with
-  | `(section $header:ident) => addScopes (isNewNamespace := false) header.getId
-  | `(section)               => do let currNamespace ← getCurrNamespace; addScope (isNewNamespace := false) "" currNamespace
+  | `(section $header:ident) => addScopes (isNewNamespace := false) (isNoncomputable := false) header.getId
+  | `(section)               => addScope (isNewNamespace := false) (isNoncomputable := false) "" (← getCurrNamespace)
+  | _                        => throwUnsupportedSyntax
+
+@[builtinCommandElab noncomputableSection] def elabNonComputableSection : CommandElab := fun stx => do
+  match stx with
+  | `(noncomputable section $header:ident) => addScopes (isNewNamespace := false) (isNoncomputable := true) header.getId
+  | `(noncomputable section)               => addScope (isNewNamespace := false) (isNoncomputable := true) "" (← getCurrNamespace)
   | _                        => throwUnsupportedSyntax
 
 @[builtinCommandElab «end»] def elabEnd : CommandElab := fun stx => do

src/Lean/Elab/Command.lean

@@ -339,12 +339,13 @@ private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name)
   let mut sectionVars := {}
   for id in scope.varDecls.concatMap getBracketedBinderIds, uid in scope.varUIds do
     sectionVars := sectionVars.insert id uid
-  { macroStack     := ctx.macroStack
-    fileName       := ctx.fileName
-    fileMap        := ctx.fileMap
-    currMacroScope := ctx.currMacroScope
-    declName?      := declName?
-    sectionVars    := sectionVars }
+  { macroStack             := ctx.macroStack
+    fileName               := ctx.fileName
+    fileMap                := ctx.fileMap
+    currMacroScope         := ctx.currMacroScope
+    declName?              := declName?
+    sectionVars            := sectionVars
+    isNoncomputableSection := scope.isNoncomputable }
 
 private def mkTermState (scope : Scope) (s : State) : Term.State := {
   messages          := {}

src/Lean/Elab/PreDefinition/Basic.lean

@@ -80,6 +80,16 @@ def addAsAxiom (preDef : PreDefinition) : MetaM Unit := do
 private def shouldGenCodeFor (preDef : PreDefinition) : Bool :=
   !preDef.kind.isTheorem && !preDef.modifiers.isNoncomputable
 
+private def compileDecl (decl : Declaration) : TermElabM Bool := do
+  try
+    Lean.compileDecl decl
+  catch ex =>
+    if (← read).isNoncomputableSection then
+      return false
+    else
+      throw ex
+  return true
+
 private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs preDef
@@ -104,7 +114,8 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U
       addTermInfo preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     if compile && shouldGenCodeFor preDef then
-      compileDecl decl
+      unless (← compileDecl decl) do
+        return ()
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 def addAndCompileNonRec (preDef : PreDefinition) : TermElabM Unit := do
@@ -128,9 +139,10 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSaf
       for preDef in preDefs do
         addTermInfo preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
-    compileDecl decl
+    unless (← compileDecl decl) do
+      return ()
     applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
-    pure ()
+    return ()
 
 def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit := do
   if preDefs.all shouldGenCodeFor then

src/Lean/Elab/Term.lean

@@ -53,6 +53,8 @@ structure Context where
   sectionFVars       : NameMap Expr    := {}
   /-- Enable/disable implicit lambdas feature. -/
   implicitLambda     : Bool            := true
+  /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for  -/
+  isNoncomputableSection : Bool        := false
 
 /-- Saved context for postponed terms and tactics to be executed. -/
 structure SavedContext where

tests/lean/noncompSection.lean

@@ -0,0 +1,35 @@
+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
+
+def i : Nat := Classical.choose ex -- Error

tests/lean/noncompSection.lean.expected.out

@@ -0,0 +1,2 @@
+1
+noncompSection.lean:35:4-35:5: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choose', and it does not have executable code