feat: safer #eval, and #eval!

previously, `#eval` would happily evaluate expressions that contain
`sorry`, either explicitly or because of failing tactics. In conjunction
with operations like array access this can lead to the lean process
crashing, which isn't particularly great.

So how `#eval` will refuse to run code that (transitively) depends on
the `sorry` axiom (using the same code as `#print axioms`).

If the user really wants to run it, they can use `#eval!`.

Author: nomeata

src/Lean/Elab/BuiltinCommand.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.CollectLevelParams
+import Lean.Util.CollectAxioms
 import Lean.Meta.Reduce
 import Lean.Elab.DeclarationRange
 import Lean.Elab.Eval
@@ -340,8 +341,7 @@ private def mkRunEval (e : Expr) : MetaM Expr := do
   let instVal ← mkEvalInstCore ``Lean.Eval e
   instantiateMVars (mkAppN (mkConst ``Lean.runEval [u]) #[α, instVal, mkSimpleThunk e])
 
-unsafe def elabEvalUnsafe : CommandElab
-  | `(#eval%$tk $term) => do
+unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Unit := do
     let declName := `_eval
     let addAndCompile (value : Expr) : TermElabM Unit := do
       let value ← Term.levelMVarToParam (← instantiateMVars value)
@@ -358,6 +358,13 @@ unsafe def elabEvalUnsafe : CommandElab
       }
       Term.ensureNoUnassignedMVars decl
       addAndCompile decl
+    -- Check for sorry axioms
+    let checkSorry (declName : Name) : MetaM Unit := do
+      unless bang do
+        let axioms ← collectAxioms declName
+        if axioms.contains ``sorryAx then
+          throwError ("Cannot evaluate expression that depends on the `sorry` axiom.\nUse `#eval!` to " ++
+            "evaluate nevertheless (which may cause lean to crash).")
     -- Elaborate `term`
     let elabEvalTerm : TermElabM Expr := do
       let e ← Term.elabTerm term none
@@ -386,6 +393,7 @@ unsafe def elabEvalUnsafe : CommandElab
           else
             let e ← mkRunMetaEval e
             addAndCompile e
+            checkSorry declName
             let act ← evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName
             pure <| Sum.inr act
       match act with
@@ -402,6 +410,7 @@ unsafe def elabEvalUnsafe : CommandElab
       -- modify e to `runEval e`
       let e ← mkRunEval (← elabEvalTerm)
       addAndCompile e
+      checkSorry declName
       let act ← evalConst (IO (String × Except IO.Error Unit)) declName
       let (out, res) ← liftM (m := IO) act
       logInfoAt tk out
@@ -412,10 +421,19 @@ unsafe def elabEvalUnsafe : CommandElab
       elabMetaEval
     else
       elabEval
+
+@[implemented_by elabEvalCoreUnsafe]
+opaque elabEvalCore (bang : Bool) (tk term : Syntax): CommandElabM Unit
+
+@[builtin_command_elab «eval»]
+def elabEval : CommandElab
+  | `(#eval%$tk $term) => elabEvalCore false tk term
   | _ => throwUnsupportedSyntax
 
-@[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
-opaque elabEval : CommandElab
+@[builtin_command_elab evalBang]
+def elabEvalBang : CommandElab
+  | `(#eval!%$tk $term) => elabEvalCore true tk term
+  | _ => throwUnsupportedSyntax
 
 private def checkImportsForRunCmds : CommandElabM Unit := do
   unless (← getEnv).contains ``CommandElabM do

src/Lean/Elab/Print.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Util.FoldConsts
 import Lean.Meta.Eqns
+import Lean.Util.CollectAxioms
 import Lean.Elab.Command
 
 namespace Lean.Elab.Command
@@ -120,40 +120,12 @@ private def printId (id : Syntax) : CommandElabM Unit := do
   | `(#print%$tk $s:str)    => logInfoAt tk s.getString
   | _                       => throwError "invalid #print command"
 
-namespace CollectAxioms
-
-structure State where
-  visited : NameSet    := {}
-  axioms  : Array Name := #[]
-
-abbrev M := ReaderT Environment $ StateM State
-
-partial def collect (c : Name) : M Unit := do
-  let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
-  let s ← get
-  unless s.visited.contains c do
-    modify fun s => { s with visited := s.visited.insert c }
-    let env ← read
-    match env.find? c with
-    | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push c }
-    | some (ConstantInfo.defnInfo v)   => collectExpr v.type *> collectExpr v.value
-    | some (ConstantInfo.thmInfo v)    => collectExpr v.type *> collectExpr v.value
-    | some (ConstantInfo.opaqueInfo v) => collectExpr v.type *> collectExpr v.value
-    | some (ConstantInfo.quotInfo _)   => pure ()
-    | some (ConstantInfo.ctorInfo v)   => collectExpr v.type
-    | some (ConstantInfo.recInfo v)    => collectExpr v.type
-    | some (ConstantInfo.inductInfo v) => collectExpr v.type *> v.ctors.forM collect
-    | none                             => pure ()
-
-end CollectAxioms
-
 private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
-  let env ← getEnv
-  let (_, s) := ((CollectAxioms.collect constName).run env).run {}
-  if s.axioms.isEmpty then
+  let axioms ← collectAxioms constName
+  if axioms.isEmpty then
     logInfo m!"'{constName}' does not depend on any axioms"
   else
-    logInfo m!"'{constName}' depends on axioms: {s.axioms.qsort Name.lt |>.toList}"
+    logInfo m!"'{constName}' depends on axioms: {axioms.qsort Name.lt |>.toList}"
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do

src/Lean/Parser/Command.lean

@@ -437,6 +437,8 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
 @[builtin_command_parser] def eval           := leading_parser
   "#eval " >> termParser
+@[builtin_command_parser] def evalBang       := leading_parser
+  "#eval! " >> termParser
 @[builtin_command_parser] def synth          := leading_parser
   "#synth " >> termParser
 @[builtin_command_parser] def exit           := leading_parser

src/Lean/Util/CollectAxioms.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.MonadEnv
+import Lean.Util.FoldConsts
+
+namespace Lean
+
+namespace CollectAxioms
+
+
+structure State where
+  visited : NameSet    := {}
+  axioms  : Array Name := #[]
+
+abbrev M := ReaderT Environment $ StateM State
+
+partial def collect (c : Name) : M Unit := do
+  let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
+  let s ← get
+  unless s.visited.contains c do
+    modify fun s => { s with visited := s.visited.insert c }
+    let env ← read
+    match env.find? c with
+    | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push c }
+    | some (ConstantInfo.defnInfo v)   => collectExpr v.type *> collectExpr v.value
+    | some (ConstantInfo.thmInfo v)    => collectExpr v.type *> collectExpr v.value
+    | some (ConstantInfo.opaqueInfo v) => collectExpr v.type *> collectExpr v.value
+    | some (ConstantInfo.quotInfo _)   => pure ()
+    | some (ConstantInfo.ctorInfo v)   => collectExpr v.type
+    | some (ConstantInfo.recInfo v)    => collectExpr v.type
+    | some (ConstantInfo.inductInfo v) => collectExpr v.type *> v.ctors.forM collect
+    | none                             => pure ()
+
+end CollectAxioms
+
+def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) := do
+  let env ← getEnv
+  let (_, s) := ((CollectAxioms.collect constName).run env).run {}
+  pure s.axioms
+
+end Lean

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/run/1697.lean

@@ -0,0 +1,42 @@
+
+/--
+error: tactic 'decide' proved that the proposition
+  False
+is false
+---
+error: Cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
+-/
+#guard_msgs in
+#eval show Nat from False.rec (by decide)
+
+/--
+warning: declaration uses 'sorry'
+---
+error: Cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
+-/
+#guard_msgs in
+#eval #[1,2,3][2]'sorry
+
+/-
+
+Uncomment after stage0 update
+
+/--
+warning: declaration uses 'sorry'
+---
+info: 3
+-/
+#guard_msgs in
+#eval! #[1,2,3][2]'sorry
+
+/--
+warning: declaration uses 'sorry'
+---
+info: 3
+-/
+#guard_msgs in
+#eval! (#[1,2,3].pop)[2]'sorry
+
+-/