feat: safer #eval, and #eval! (#4810)

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!`.

Closes #1697

doc/examples/interp.lean

@@ -149,4 +149,4 @@ def fact : Expr ctx (Ty.fn Ty.int Ty.int) :=
            (op (·*·) (delay fun _ => app fact (op (·-·) (var stop) (val 1))) (var stop)))
   decreasing_by sorry
 
-#eval fact.interp Env.nil 10
+#eval! fact.interp Env.nil 10

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
+  | `(Parser.Command.evalBang|#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/277a.lean.expected.out

@@ -1,2 +1,3 @@
 277a.lean:4:7-4:15: error: unknown identifier 'nonexistant'
-277a.lean:4:0-4:25: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+277a.lean:4:0-4:25: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/277b.lean.expected.out

@@ -1,3 +1,4 @@
 277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
   List Point
-277b.lean:8:0-8:16: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+277b.lean:8:0-8:16: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/440.lean.expected.out

@@ -6,4 +6,5 @@ context:
 x : Nat
 ⊢ Nat
 f (x : Nat) : Nat
-440.lean:11:0-11:9: error: cannot evaluate code because 'g' uses 'sorry' and/or contains errors
+440.lean:11:0-11:9: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/evalSorry.lean.expected.out

@@ -7,5 +7,7 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-evalSorry.lean:7:0-7:15: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
-evalSorry.lean:11:0-11:15: error: cannot evaluate code because 'h' uses 'sorry' and/or contains errors
+evalSorry.lean:7:0-7:15: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
+evalSorry.lean:11:0-11:15: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -6,4 +6,5 @@ has type
   @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type
 but is expected to have type
   @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type
-phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/prvCtor.lean.expected.out

@@ -1,7 +1,8 @@
 a : Nat
 
 prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private
-prvCtor.lean:23:0-25:61: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+prvCtor.lean:23:0-25:61: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize

tests/lean/run/1697.lean

@@ -0,0 +1,36 @@
+
+/--
+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
+
+/--
+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

tests/lean/run/3713.lean

@@ -8,7 +8,8 @@ def somethingBad : MetaM Nat := do
 /--
 error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
 ---
-info:
+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 MetaM Unit from do
@@ -20,7 +21,8 @@ def foo : MetaM Bool :=
 /--
 error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
 ---
-info:
+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 MetaM Unit from do

tests/lean/run/compiler_proj_bug.lean

@@ -1,9 +1,13 @@
-
-
 structure S :=
 (a : Nat) (h : a > 0) (b : Nat)
 
 def f (s : S) :=
 s.b - s.a
 
-#eval f {a := 5, b := 30, h := sorry }
+/--
+warning: declaration uses 'sorry'
+---
+info: 25
+-/
+#guard_msgs in
+#eval! f {a := 5, b := 30, h := sorry }

tests/lean/run/lcnfEtaExpandBug.lean

@@ -1,3 +1,3 @@
 import Lean
 
-run_meta Lean.Compiler.compile #[``Lean.Elab.Command.elabEvalUnsafe]
+run_meta Lean.Compiler.compile #[``Lean.Elab.Command.elabEvalCoreUnsafe]

tests/lean/scientific.lean.expected.out

@@ -15,7 +15,8 @@ scientific.lean:15:7-15:12: error: unexpected token; expected command
 scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
 scientific.lean:16:7-16:16: error: unexpected token; expected command
 scientific.lean:19:6-19:7: error: unknown identifier 'e'
-scientific.lean:19:0-19:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+scientific.lean:19:0-19:9: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 scientific.lean:20:9: error: missing exponent digits in scientific literal
 scientific.lean:21:9: error: missing exponent digits in scientific literal
 scientific.lean:22:9: error: missing exponent digits in scientific literal
@@ -24,7 +25,9 @@ scientific.lean:24:9: error: missing exponent digits in scientific literal
 scientific.lean:25:9: error: missing exponent digits in scientific literal
 scientific.lean:26:6-26:8: error: invalid dotted identifier notation, unknown identifier `Nat.E` from expected type
   Nat
-scientific.lean:26:0-26:11: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+scientific.lean:26:0-26:11: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 scientific.lean:27:7-27:9: error: unknown identifier 'E3'
-scientific.lean:27:0-27:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+scientific.lean:27:0-27:9: error: cannot evaluate expression that depends on the `sorry` axiom.
+Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 scientific.lean:28:7: error: missing exponent digits in scientific literal

tests/lean/terminationFailure.lean

@@ -11,8 +11,8 @@ where
 #check f
 #check f.g
 
-#eval f 0
-#eval f.g 0
+#eval! f 0
+#eval! f.g 0
 
 inductive Foo where
   | a | b | c
@@ -25,4 +25,4 @@ def h (x : Nat) : Foo :=
 
 #check h
 
-#eval h 0
+#eval! h 0