diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 75e3664cc3..b1fa482a50 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -535,24 +535,21 @@ syntax (name := includeStr) "include_str " term : term /-- The `run_cmd doSeq` command executes code in `CommandElabM Unit`. -This is almost the same as `#eval show CommandElabM Unit from do doSeq`, -except that it doesn't print an empty diagnostic. +This is the same as `#eval show CommandElabM Unit from discard do doSeq`. -/ syntax (name := runCmd) "run_cmd " doSeq : command /-- The `run_elab doSeq` command executes code in `TermElabM Unit`. -This is almost the same as `#eval show TermElabM Unit from do doSeq`, -except that it doesn't print an empty diagnostic. +This is the same as `#eval show TermElabM Unit from discard do doSeq`. -/ syntax (name := runElab) "run_elab " doSeq : command /-- The `run_meta doSeq` command executes code in `MetaM Unit`. -This is almost the same as `#eval show MetaM Unit from do doSeq`, -except that it doesn't print an empty diagnostic. +This is the same as `#eval show MetaM Unit from do discard doSeq`. -(This is effectively a synonym for `run_elab`.) +(This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.) -/ syntax (name := runMeta) "run_meta " doSeq : command diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b8e8472c08..784a7f5e85 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2869,6 +2869,32 @@ instance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where instance (m) : MonadLiftT m m where monadLift x := x +/-- +Typeclass used for adapting monads. This is similar to `MonadLift`, but instances are allowed to +make use of default state for the purpose of synthesizing such an instance, if necessary. +Every `MonadLift` instance gives a `MonadEval` instance. + +The purpose of this class is for the `#eval` command, +which looks for a `MonadEval m CommandElabM` or `MonadEval m IO` instance. +-/ +class MonadEval (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where + /-- Evaluates a value from monad `m` into monad `n`. -/ + monadEval : {α : Type u} → m α → n α + +instance [MonadLift m n] : MonadEval m n where + monadEval := MonadLift.monadLift + +/-- The transitive closure of `MonadEval`. -/ +class MonadEvalT (m : Type u → Type v) (n : Type u → Type w) where + /-- Evaluates a value from monad `m` into monad `n`. -/ + monadEval : {α : Type u} → m α → n α + +instance (m n o) [MonadEval n o] [MonadEvalT m n] : MonadEvalT m o where + monadEval x := MonadEval.monadEval (m := n) (MonadEvalT.monadEval x) + +instance (m) : MonadEvalT m m where + monadEval x := x + /-- A functor in the category of monads. Can be used to lift monad-transforming functions. Based on [`MFunctor`] from the `pipes` Haskell package, but not restricted to diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index ca61bb9b16..f391dedec4 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -928,41 +928,6 @@ def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m end FS end IO -universe u - -namespace Lean - -/-- Typeclass used for presenting the output of an `#eval` command. -/ -class Eval (α : Type u) where - -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval` - -- so that `()` output is hidden in chained instances such as for some `IO Unit`. - -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`) - eval : (Unit → α) → (hideUnit : Bool := true) → IO Unit - -instance instEval [ToString α] : Eval α where - eval a _ := IO.println (toString (a ())) - -instance [Repr α] : Eval α where - eval a _ := IO.println (repr (a ())) - -instance : Eval Unit where - eval u hideUnit := if hideUnit then pure () else IO.println (repr (u ())) - -instance [Eval α] : Eval (IO α) where - eval x _ := do - let a ← x () - Eval.eval fun _ => a - -instance [Eval α] : Eval (BaseIO α) where - eval x _ := do - let a ← x () - Eval.eval fun _ => a - -def runEval [Eval α] (a : Unit → α) : IO (String × Except IO.Error Unit) := - IO.FS.withIsolatedStreams (Eval.eval a false |>.toBaseIO) - -end Lean - syntax "println! " (interpolatedStr(term) <|> term) : term macro_rules diff --git a/src/Lean.lean b/src/Lean.lean index 5da1bb9c24..dd3eccd7e9 100644 --- a/src/Lean.lean +++ b/src/Lean.lean @@ -20,7 +20,6 @@ import Lean.MetavarContext import Lean.AuxRecursor import Lean.Meta import Lean.Util -import Lean.Eval import Lean.Structure import Lean.PrettyPrinter import Lean.CoreM diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 4e1d393c8c..7bd939c233 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -7,7 +7,6 @@ prelude import Lean.Util.RecDepth import Lean.Util.Trace import Lean.Log -import Lean.Eval import Lean.ResolveName import Lean.Elab.InfoTree.Types import Lean.MonadEnv @@ -277,12 +276,6 @@ def mkFreshUserName (n : Name) : CoreM Name := | Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx | Except.ok a => return a -instance [MetaEval α] : MetaEval (CoreM α) where - eval env opts x _ := do - let x : CoreM α := do try x finally printTraces - let (a, s) ← (withConsistentCtx x).toIO { fileName := "", fileMap := default, options := opts } { env := env } - MetaEval.eval s.env opts a (hideUnit := true) - -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]` protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α := controlAt CoreM fun runInBase => withIncRecDepth (runInBase x) diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index 273224b1ac..663f64823c 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -42,6 +42,7 @@ import Lean.Elab.Notation import Lean.Elab.Mixfix import Lean.Elab.MacroRules import Lean.Elab.BuiltinCommand +import Lean.Elab.BuiltinEvalCommand import Lean.Elab.RecAppSyntax import Lean.Elab.Eval import Lean.Elab.Calc diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index e9923af769..5f47d772a4 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -311,167 +311,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do failIfSucceeds <| elabCheckCore (ignoreStuckTC := false) (← `(#check $term)) | _ => throwUnsupportedSyntax -private def mkEvalInstCore (evalClassName : Name) (e : Expr) : MetaM Expr := do - let α ← inferType e - let u ← getDecLevel α - let inst := mkApp (Lean.mkConst evalClassName [u]) α - try - synthInstance inst - catch _ => - -- Put `α` in WHNF and try again - try - let α ← whnf α - synthInstance (mkApp (Lean.mkConst evalClassName [u]) α) - catch _ => - -- Fully reduce `α` and try again - try - let α ← reduce (skipTypes := false) α - synthInstance (mkApp (Lean.mkConst evalClassName [u]) α) - catch _ => - throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class" - -private def mkRunMetaEval (e : Expr) : MetaM Expr := - withLocalDeclD `env (mkConst ``Lean.Environment) fun env => - withLocalDeclD `opts (mkConst ``Lean.Options) fun opts => do - let α ← inferType e - let u ← getDecLevel α - let instVal ← mkEvalInstCore ``Lean.MetaEval e - let e := mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e] - instantiateMVars (← mkLambdaFVars #[env, opts] e) - -private def mkRunEval (e : Expr) : MetaM Expr := do - let α ← inferType e - let u ← getDecLevel α - let instVal ← mkEvalInstCore ``Lean.Eval e - instantiateMVars (mkAppN (mkConst ``Lean.runEval [u]) #[α, instVal, mkSimpleThunk e]) - -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) - let type ← inferType value - let us := collectLevelParams {} value |>.params - let value ← instantiateMVars value - let decl := Declaration.defnDecl { - name := declName - levelParams := us.toList - type := type - value := value - hints := ReducibilityHints.opaque - safety := DefinitionSafety.unsafe - } - 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 - Term.synthesizeSyntheticMVarsNoPostponing - if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then throwAbortTerm - if (← isProp e) then - mkDecide e - else - return e - -- Evaluate using term using `MetaEval` class. - let elabMetaEval : CommandElabM Unit := do - -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure - -- we don't pollute the environment with auxliary declarations. - -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands - -- that modify `CommandElabM` state not just the `Environment`. - let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ← - runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do - let e ← elabEvalTerm - let eType ← instantiateMVars (← inferType e) - if eType.isAppOfArity ``CommandElabM 1 then - let mut stx ← Term.exprToSyntax e - unless (← isDefEq eType.appArg! (mkConst ``Unit)) do - stx ← `($stx >>= fun v => IO.println (repr v)) - let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx - pure <| Sum.inl act - 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 - | .inl act => act - | .inr act => - let (out, res) ← act (← getEnv) (← getOptions) - logInfoAt tk out - match res with - | Except.error e => throwError e.toString - | Except.ok env => setEnv env; pure () - -- Evaluate using term using `Eval` class. - let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do - -- fall back to non-meta eval if MetaEval hasn't been defined yet - -- 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 - match res with - | Except.error e => throwError e.toString - | Except.ok _ => pure () - if (← getEnv).contains ``Lean.MetaEval then do - 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 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 - throwError "to use this command, include `import Lean.Elab.Command`" - -@[builtin_command_elab runCmd] -def elabRunCmd : CommandElab - | `(run_cmd $elems:doSeq) => do - checkImportsForRunCmds - (← liftTermElabM <| Term.withDeclName `_run_cmd <| - unsafe Term.evalTerm (CommandElabM Unit) - (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) - (← `(discard do $elems))) - | _ => throwUnsupportedSyntax - -@[builtin_command_elab runElab] -def elabRunElab : CommandElab - | `(run_elab $elems:doSeq) => do - checkImportsForRunCmds - (← liftTermElabM <| Term.withDeclName `_run_elab <| - unsafe Term.evalTerm (CommandElabM Unit) - (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) - (← `(Command.liftTermElabM <| discard do $elems))) - | _ => throwUnsupportedSyntax - -@[builtin_command_elab runMeta] -def elabRunMeta : CommandElab := fun stx => - match stx with - | `(run_meta $elems:doSeq) => do - checkImportsForRunCmds - let stxNew ← `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems)) - withMacroExpansion stx stxNew do elabCommand stxNew - | _ => throwUnsupportedSyntax - @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do let term := stx[1] withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean new file mode 100644 index 0000000000..f5cb0179ba --- /dev/null +++ b/src/Lean/Elab/BuiltinEvalCommand.lean @@ -0,0 +1,283 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Lean.Util.CollectLevelParams +import Lean.Util.CollectAxioms +import Lean.Meta.Reduce +import Lean.Elab.Eval +import Lean.Elab.Deriving.Basic + +/-! +# Implementation of `#eval` command +-/ + +namespace Lean.Elab.Command +open Meta + +register_builtin_option eval.pp : Bool := { + defValue := true + descr := "('#eval' command) enables using 'ToExpr' instances to pretty print the result, \ + otherwise uses 'Repr' or 'ToString' instances" +} + +register_builtin_option eval.type : Bool := { + defValue := false -- TODO: set to 'true' + descr := "('#eval' command) enables pretty printing the type of the result" +} + +register_builtin_option eval.derive.repr : Bool := { + defValue := true + descr := "('#eval' command) enables auto-deriving 'Repr' instances as a fallback" +} + +builtin_initialize + registerTraceClass `Elab.eval + +/-- +Elaborates the term, ensuring the result has no expression metavariables. +If there would be unsolved-for metavariables, tries hinting that the resulting type +is a monadic value with the `CommandElabM`, `TermElabM`, or `IO` monads. +Throws errors if the term is a proof or a type, but lifts props to `Bool` using `mkDecide`. +-/ +private def elabTermForEval (term : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do + let ty ← expectedType?.getDM mkFreshTypeMVar + let e ← Term.elabTermEnsuringType term ty + synthesizeWithHinting ty + let e ← instantiateMVars e + if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then throwAbortTerm + if ← isProof e then + throwError m!"cannot evaluate, proofs are not computationally relevant" + let e ← if (← isProp e) then mkDecide e else pure e + if ← isType e then + throwError m!"cannot evaluate, types are not computationally relevant" + trace[Elab.eval] "elaborated term:{indentExpr e}" + return e +where + /-- Try different strategies to make `Term.synthesizeSyntheticMVarsNoPostponing` succeed. -/ + synthesizeWithHinting (ty : Expr) : TermElabM Unit := do + Term.synthesizeSyntheticMVarsUsingDefault + let s ← saveState + try + Term.synthesizeSyntheticMVarsNoPostponing + catch ex => + let exS ← saveState + -- Try hinting that `ty` is a monad application. + for m in #[``CommandElabM, ``TermElabM, ``IO] do + s.restore true + try + if ← isDefEq ty (← mkFreshMonadApp m) then + Term.synthesizeSyntheticMVarsNoPostponing + return + catch _ => pure () + -- None of the hints worked, so throw the original error. + exS.restore true + throw ex + mkFreshMonadApp (n : Name) : MetaM Expr := do + let m ← mkConstWithFreshMVarLevels n + let (args, _, _) ← forallMetaBoundedTelescope (← inferType m) 1 + return mkAppN m args + +private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Unit := do + let value ← Term.levelMVarToParam (← instantiateMVars value) + let type ← inferType value + let us := collectLevelParams {} value |>.params + let decl := Declaration.defnDecl { + name := declName + levelParams := us.toList + type := type + value := value + hints := ReducibilityHints.opaque + safety := DefinitionSafety.unsafe + } + Term.ensureNoUnassignedMVars decl + addAndCompile decl + unless allowSorry do + let axioms ← collectAxioms declName + if axioms.contains ``sorryAx then + throwError "\ + aborting evaluation since the expression depends on the 'sorry' axiom, \ + which can lead to runtime instability and crashes.\n\n\ + To attempt to evaluate anyway despite the risks, use the '#eval!' command." + +/-- +Try to make a `@projFn ty inst e` application, even if it takes unfolding the type `ty` of `e` to synthesize the instance `inst`. +-/ +private partial def mkDeltaInstProj (inst projFn : Name) (e : Expr) (ty? : Option Expr := none) (tryReduce : Bool := true) : MetaM Expr := do + let ty ← ty?.getDM (inferType e) + if let .some inst ← trySynthInstance (← mkAppM inst #[ty]) then + mkAppOptM projFn #[ty, inst, e] + else + let ty ← whnfCore ty + let some ty ← unfoldDefinition? ty + | guard tryReduce + -- Reducing the type is a strategy `#eval` used before the refactor of #5627. + -- The test lean/run/hlistOverload.lean depends on it, so we preserve the behavior. + let ty ← reduce (skipTypes := false) ty + mkDeltaInstProj inst projFn e ty (tryReduce := false) + mkDeltaInstProj inst projFn e ty tryReduce + +/-- Try to make a `toString e` application, even if it takes unfolding the type of `e` to find a `ToString` instance. -/ +private def mkToString (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do + mkDeltaInstProj ``ToString ``toString e ty? + +/-- Try to make a `repr e` application, even if it takes unfolding the type of `e` to find a `Repr` instance. -/ +private def mkRepr (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do + mkDeltaInstProj ``Repr ``repr e ty? + +/-- Try to make a `toExpr e` application, even if it takes unfolding the type of `e` to find a `ToExpr` instance. -/ +private def mkToExpr (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do + mkDeltaInstProj ``ToExpr ``toExpr e ty? + +/-- +Returns a representation of `e` using `Format`, or else fails. +If the `eval.derive.repr` option is true, then tries automatically deriving a `Repr` instance first. +Currently auto-derivation does not attempt to derive recursively. +-/ +private def mkFormat (e : Expr) : MetaM Expr := do + mkRepr e <|> (do mkAppM ``Std.Format.text #[← mkToString e]) + <|> do + if eval.derive.repr.get (← getOptions) then + if let .const name _ := (← whnf (← inferType e)).getAppFn then + try + trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{MessageData.ofConstName name}'" + liftCommandElabM do applyDerivingHandlers ``Repr #[name] none + resetSynthInstanceCache + return ← mkRepr e + catch ex => + trace[Elab.eval] "Failed to use derived 'Repr' instance. Exception: {ex.toMessageData}" + throwError m!"could not synthesize a 'Repr' or 'ToString' instance for type{indentExpr (← inferType e)}" + +/-- +Returns a representation of `e` using `MessageData`, or else fails. +Tries `mkFormat` if a `ToExpr` instance can't be synthesized. +-/ +private def mkMessageData (e : Expr) : MetaM Expr := do + (do guard <| eval.pp.get (← getOptions); mkAppM ``MessageData.ofExpr #[← mkToExpr e]) + <|> (return mkApp (mkConst ``MessageData.ofFormat) (← mkFormat e)) + <|> do throwError m!"could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type{indentExpr (← inferType e)}" + +private structure EvalAction where + eval : CommandElabM MessageData + /-- Whether to print the result of evaluation. + If `some`, the expression is what type to use for the type ascription when `pp.type` is true. -/ + printVal : Option Expr + +unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit := withRef tk do + let declName := `_eval + -- `t` is either `MessageData` or `Format`, and `mkT` is for synthesizing an expression that yields a `t`. + -- The `toMessageData` function adapts `t` to `MessageData`. + let mkAct {t : Type} [Inhabited t] (toMessageData : t → MessageData) (mkT : Expr → MetaM Expr) (e : Expr) : TermElabM EvalAction := do + -- Create a monadic action given the name of the monad `mc`, the monad `m` itself, + -- and an expression `e` to evaluate in this monad. + -- A trick here is that `mkMAct?` makes use of `MonadEval` instances are currently available in this stage, + -- and we do not need them to be available in the target environment. + let mkMAct? (mc : Name) (m : Type → Type) [Monad m] [MonadEvalT m CommandElabM] (e : Expr) : TermElabM (Option EvalAction) := do + let some e ← observing? (mkAppOptM ``MonadEvalT.monadEval #[none, mkConst mc, none, none, e]) + | return none + let eType := e.appFn!.appArg! + if ← isDefEq eType (mkConst ``Unit) then + addAndCompileExprForEval declName e (allowSorry := bang) + let mf : m Unit ← evalConst (m Unit) declName + return some { eval := do MonadEvalT.monadEval mf; pure "", printVal := none } + else + let rf ← withLocalDeclD `x eType fun x => do mkLambdaFVars #[x] (← mkT x) + let r ← mkAppM ``Functor.map #[rf, e] + addAndCompileExprForEval declName r (allowSorry := bang) + let mf : m t ← evalConst (m t) declName + return some { eval := toMessageData <$> MonadEvalT.monadEval mf, printVal := some eType } + if let some act ← mkMAct? ``CommandElabM CommandElabM e + -- Fallbacks in case we are in the Lean package but don't have `CommandElabM` yet + <||> mkMAct? ``TermElabM TermElabM e <||> mkMAct? ``MetaM MetaM e <||> mkMAct? ``CoreM CoreM e + -- Fallback in case nothing is imported + <||> mkMAct? ``IO IO e then + return act + else + -- Otherwise, assume this is a pure value. + -- There is no need to adapt pure values to `CommandElabM`. + -- This enables `#eval` to work on pure values even when `CommandElabM` is not available. + let r ← try mkT e catch ex => do + -- Diagnose whether the value is monadic for a representable value, since it's better to mention `MonadEval` in that case. + try + let some (m, ty) ← isTypeApp? (← inferType e) | failure + guard <| (← isMonad? m).isSome + -- Verify that there is a way to form some representation: + discard <| withLocalDeclD `x ty fun x => mkT x + catch _ => + throw ex + throwError m!"unable to synthesize '{MessageData.ofConstName ``MonadEval}' instance \ + to adapt{indentExpr (← inferType e)}\n\ + to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'." + addAndCompileExprForEval declName r (allowSorry := bang) + -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below. + let r ← toMessageData <$> evalConst t declName + return { eval := pure r, printVal := some (← inferType e) } + let (output, exOrRes) ← IO.FS.withIsolatedStreams do + try + -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure + -- we don't pollute the environment with auxiliary declarations. + let act : EvalAction ← liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do + let e ← elabTermForEval term expectedType? + -- If there is an elaboration error, don't evaluate! + if e.hasSyntheticSorry then throwAbortTerm + -- We want `#eval` to work even in the core library, so if `ofFormat` isn't available, + -- we fall back on a `Format`-based approach. + if (← getEnv).contains ``Lean.MessageData.ofFormat then + mkAct id (mkMessageData ·) e + else + mkAct Lean.MessageData.ofFormat (mkFormat ·) e + let res ← act.eval + return Sum.inr (res, act.printVal) + catch ex => + return Sum.inl ex + if !output.isEmpty then logInfoAt tk output + match exOrRes with + | .inl ex => logException ex + | .inr (_, none) => pure () + | .inr (res, some type) => + if eval.type.get (← getOptions) then + logInfo m!"{res} : {type}" + else + logInfo res + +@[implemented_by elabEvalCoreUnsafe] +opaque elabEvalCore (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit + +@[builtin_command_elab «eval»] +def elabEval : CommandElab + | `(#eval%$tk $term) => elabEvalCore false tk term none + | _ => throwUnsupportedSyntax + +@[builtin_command_elab evalBang] +def elabEvalBang : CommandElab + | `(#eval!%$tk $term) => elabEvalCore true tk term none + | _ => throwUnsupportedSyntax + +@[builtin_command_elab runCmd] +def elabRunCmd : CommandElab + | `(run_cmd%$tk $elems:doSeq) => do + unless (← getEnv).contains ``CommandElabM do + throwError "to use this command, include `import Lean.Elab.Command`" + elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) + | _ => throwUnsupportedSyntax + +@[builtin_command_elab runElab] +def elabRunElab : CommandElab + | `(run_elab%$tk $elems:doSeq) => do + unless (← getEnv).contains ``TermElabM do + throwError "to use this command, include `import Lean.Elab.Term`" + elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``TermElabM) (mkConst ``Unit)) + | _ => throwUnsupportedSyntax + +@[builtin_command_elab runMeta] +def elabRunMeta : CommandElab := fun stx => + match stx with + | `(run_meta%$tk $elems:doSeq) => do + unless (← getEnv).contains ``MetaM do + throwError "to use this command, include `import Lean.Meta.Basic`" + elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``MetaM) (mkConst ``Unit)) + | _ => throwUnsupportedSyntax + +end Lean.Elab.Command diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 073ec1258a..47bc7dbdba 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -619,6 +619,9 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do let ((ea, _), _) ← runCore x MonadExcept.ofExcept ea +instance : MonadEval TermElabM CommandElabM where + monadEval := liftTermElabM + /-- Execute the monadic action `elabFn xs` as a `CommandElabM` monadic action, where `xs` are free variables corresponding to all active scoped variables declared using the `variable` command. @@ -727,6 +730,12 @@ Commands that modify the processing of subsequent commands, such as `open` and `namespace` commands, only have an effect for the remainder of the `CommandElabM` computation passed here, and do not affect subsequent commands. + +*Warning:* when using this from `MetaM` monads, the caches are *not* reset. +If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache` +to reset the instance cache. +While the `modifyEnv` function for `MetaM` clears its caches entirely, +`liftCommandElabM` has no way to reset these caches. -/ def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do let (a, commandState) ← diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 78593be5d0..75e44d8256 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -2047,13 +2047,6 @@ def TermElabM.toIO (x : TermElabM α) let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta return (a, sCore, sMeta, s) -instance [MetaEval α] : MetaEval (TermElabM α) where - eval env opts x _ := do - let x : TermElabM α := do - try x finally - (← Core.getMessageLog).forM fun msg => do IO.println (← msg.toString) - MetaEval.eval env opts (hideUnit := true) <| x.run' {} - /-- Execute `x` and then tries to solve pending universe constraints. Note that, stuck constraints will not be discarded. diff --git a/src/Lean/Eval.lean b/src/Lean/Eval.lean deleted file mode 100644 index 26795484d6..0000000000 --- a/src/Lean/Eval.lean +++ /dev/null @@ -1,27 +0,0 @@ -/- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Sebastian Ullrich --/ -prelude -import Lean.Environment - -namespace Lean - -universe u - -/-- -`Eval` extension that gives access to the current environment & options. -The basic `Eval` class is in the prelude and should not depend on these -types. --/ -class MetaEval (α : Type u) where - eval : Environment → Options → α → (hideUnit : Bool) → IO Environment - -instance {α : Type u} [Eval α] : MetaEval α := - ⟨fun env _ a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env⟩ - -def runMetaEval {α : Type u} [MetaEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) := - IO.FS.withIsolatedStreams (MetaEval.eval env opts a false |>.toBaseIO) - -end Lean diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 0cefdfd8c8..f5f9c79ad1 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -456,9 +456,6 @@ instance : MonadBacktrack SavedState MetaM where let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore pure (a, sCore, s) -instance [MetaEval α] : MetaEval (MetaM α) := - ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩ - protected def throwIsDefEqStuck : MetaM α := throw <| Exception.internal isDefEqStuckExceptionId @@ -501,6 +498,9 @@ variable [MonadControlT MetaM n] [Monad n] @[inline] def resetDefEqPermCaches : MetaM Unit := modifyDefEqPermCache fun _ => {} +@[inline] def resetSynthInstanceCache : MetaM Unit := + modifyCache fun c => {c with synthInstance := {}} + @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do if (← isDiagnosticsEnabled) then modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag } diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index d8336c56d2..f409144336 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -462,9 +462,33 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where "#check " >> termParser @[builtin_command_parser] def check_failure := leading_parser "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check -@[builtin_command_parser] def eval := leading_parser +/-- +`#eval e` evaluates the expression `e` by compiling and evaluating it. + +* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. +* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` + to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. + Users can define `MonadEval` instances to extend the list of supported monads. + +The `#eval` command gracefully degrades in capability depending on what is imported. +Importing the `Lean.Elab.Command` module provides full capabilities. + +Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, +since the presence of `sorry` can lead to runtime instability and crashes. +This check can be overridden with the `#eval! e` command. + +Options: +* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the + usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. +* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. +* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance + when there is no other way to print the result. + +See also: `#reduce e` for evaluation by term reduction. +-/ +@[builtin_command_parser, builtin_doc] def eval := leading_parser "#eval " >> termParser -@[builtin_command_parser] def evalBang := leading_parser +@[builtin_command_parser, inherit_doc eval] def evalBang := leading_parser "#eval! " >> termParser @[builtin_command_parser] def synth := leading_parser "#synth " >> termParser diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out index d5026a3c44..f104f23ad6 100644 --- a/tests/lean/1021.lean.expected.out +++ b/tests/lean/1021.lean.expected.out @@ -1,8 +1,8 @@ -some { range := { pos := { line := 194, column := 42 }, - charUtf16 := 42, - endPos := { line := 200, column := 31 }, - endCharUtf16 := 31 }, - selectionRange := { pos := { line := 194, column := 46 }, - charUtf16 := 46, - endPos := { line := 194, column := 58 }, - endCharUtf16 := 58 } } +some + { + range := + { pos := { line := 194, column := 42 }, charUtf16 := 42, endPos := { line := 200, column := 31 }, + endCharUtf16 := 31 }, + selectionRange := + { pos := { line := 194, column := 46 }, charUtf16 := 46, endPos := { line := 194, column := 58 }, + endCharUtf16 := 58 } } diff --git a/tests/lean/1240.lean.expected.out b/tests/lean/1240.lean.expected.out index da063cf845..c0819fedf5 100644 --- a/tests/lean/1240.lean.expected.out +++ b/tests/lean/1240.lean.expected.out @@ -1,2 +1 @@ - -1240.lean:4:0-5:65: error: import failed, trying to import module with anonymous name +1240.lean:4:0-4:5: error: import failed, trying to import module with anonymous name diff --git a/tests/lean/277a.lean.expected.out b/tests/lean/277a.lean.expected.out index a9c99c3109..37aa68a463 100644 --- a/tests/lean/277a.lean.expected.out +++ b/tests/lean/277a.lean.expected.out @@ -1,3 +1 @@ 277a.lean:4:7-4:15: error: unknown identifier 'nonexistent' -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). diff --git a/tests/lean/277b.lean.expected.out b/tests/lean/277b.lean.expected.out index 34b17b676d..c3aa9d6792 100644 --- a/tests/lean/277b.lean.expected.out +++ b/tests/lean/277b.lean.expected.out @@ -1,4 +1,2 @@ 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 expression that depends on the `sorry` axiom. -Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/440.lean.expected.out b/tests/lean/440.lean.expected.out index 720305265c..73302decb6 100644 --- a/tests/lean/440.lean.expected.out +++ b/tests/lean/440.lean.expected.out @@ -6,5 +6,6 @@ context: x : Nat ⊢ Nat f (x : Nat) : Nat -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). +440.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes. + +To attempt to evaluate anyway despite the risks, use the '#eval!' command. diff --git a/tests/lean/474.lean b/tests/lean/474.lean index cd0df285d5..bcfb62ed44 100644 --- a/tests/lean/474.lean +++ b/tests/lean/474.lean @@ -1,6 +1,13 @@ import Lean open Lean Meta +open PrettyPrinter Delaborator SubExpr in +@[delab fvar] +def delabFVar : Delab := do + let Expr.fvar fvarId ← getExpr | unreachable! + let none := (← getLCtx).find? fvarId | failure + return mkIdent `FREE + #eval do let e ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do let m ← mkFreshExprMVar (mkConst ``Nat) diff --git a/tests/lean/474.lean.expected.out b/tests/lean/474.lean.expected.out index b29a7dccf6..b656f5c6b1 100644 --- a/tests/lean/474.lean.expected.out +++ b/tests/lean/474.lean.expected.out @@ -1,7 +1,7 @@ let y := Nat.zero; y.add y fun y_1 => y.add y_1 -fun y => Nat.add _fvar.1 y +fun y => Nat.add FREE y fun (y : Nat) => Nat.add y y ?m.add y Nat.add (?m #0) #0 diff --git a/tests/lean/casesOnCases.lean.expected.out b/tests/lean/casesOnCases.lean.expected.out index 139597f9cb..e69de29bb2 100644 --- a/tests/lean/casesOnCases.lean.expected.out +++ b/tests/lean/casesOnCases.lean.expected.out @@ -1,2 +0,0 @@ - - diff --git a/tests/lean/coe.lean.expected.out b/tests/lean/coe.lean.expected.out index 647f684b6a..1aa791f9b4 100644 --- a/tests/lean/coe.lean.expected.out +++ b/tests/lean/coe.lean.expected.out @@ -1,5 +1,3 @@ - - ↑n : Nat ↑n : Nat ⇑f : Nat → Nat diff --git a/tests/lean/evalInstMessage.lean.expected.out b/tests/lean/evalInstMessage.lean.expected.out index 54f52a0ba6..8b195ffcfe 100644 --- a/tests/lean/evalInstMessage.lean.expected.out +++ b/tests/lean/evalInstMessage.lean.expected.out @@ -1,7 +1,2 @@ -evalInstMessage.lean:3:0-3:12: error: expression - double -has type +evalInstMessage.lean:3:0-3:5: error: could not synthesize a 'Repr' or 'ToString' instance for type Nat → Nat -but instance - Lean.Eval (Nat → Nat) -failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out index ecd7abad97..a564755b9a 100644 --- a/tests/lean/evalSorry.lean.expected.out +++ b/tests/lean/evalSorry.lean.expected.out @@ -7,7 +7,9 @@ has type String : Type but is expected to have type Nat : Type -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). +evalSorry.lean:7:0-7:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes. + +To attempt to evaluate anyway despite the risks, use the '#eval!' command. +evalSorry.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes. + +To attempt to evaluate anyway despite the risks, use the '#eval!' command. diff --git a/tests/lean/eval_except.lean.expected.out b/tests/lean/eval_except.lean.expected.out index 69f0a21a69..c142018fca 100644 --- a/tests/lean/eval_except.lean.expected.out +++ b/tests/lean/eval_except.lean.expected.out @@ -1,5 +1,3 @@ - -eval_except.lean:4:0-4:57: error: this is my error - -eval_except.lean:5:0-5:80: error: no such file or directory (error code: 31) +eval_except.lean:4:0-4:5: error: this is my error +eval_except.lean:5:0-5:5: error: no such file or directory (error code: 31) file: file.ext diff --git a/tests/lean/file_not_found.lean.expected.out b/tests/lean/file_not_found.lean.expected.out index d93b7eb447..4881e077fb 100644 --- a/tests/lean/file_not_found.lean.expected.out +++ b/tests/lean/file_not_found.lean.expected.out @@ -1,9 +1,5 @@ - -file_not_found.lean:6:0-6:77: error: no such file or directory (error code: 2) +file_not_found.lean:6:0-6:5: error: no such file or directory (error code: 2) file: non-existent-file.txt - - -file_not_found.lean:13:0-13:69: error: permission denied (error code: 13) +file_not_found.lean:13:0-13:5: error: permission denied (error code: 13) file: readonly.txt - -file_not_found.lean:14:0-18:9: error: invalid argument (error code: 9, bad file descriptor) +file_not_found.lean:14:0-14:5: error: invalid argument (error code: 9, bad file descriptor) diff --git a/tests/lean/implicitArgumentError.lean b/tests/lean/implicitArgumentError.lean index a99d38a237..e0f7cbcf93 100644 --- a/tests/lean/implicitArgumentError.lean +++ b/tests/lean/implicitArgumentError.lean @@ -9,9 +9,10 @@ def foo {n : Nat} := 2*n /-- error: don't know how to synthesize implicit argument 'n' - @foo ?m.64 + @foo ?_ context: ⊢ Nat -/ #guard_msgs in +set_option pp.mvars false in #eval foo diff --git a/tests/lean/inlineIssue.lean.expected.out b/tests/lean/inlineIssue.lean.expected.out index 139597f9cb..e69de29bb2 100644 --- a/tests/lean/inlineIssue.lean.expected.out +++ b/tests/lean/inlineIssue.lean.expected.out @@ -1,2 +0,0 @@ - - diff --git a/tests/lean/interactive/incrementalCommand.lean.expected.out b/tests/lean/interactive/incrementalCommand.lean.expected.out index da0491b780..73d7361e34 100644 --- a/tests/lean/interactive/incrementalCommand.lean.expected.out +++ b/tests/lean/interactive/incrementalCommand.lean.expected.out @@ -10,7 +10,7 @@ w "severity": 3, "range": {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}, - "message": "\"import\"\n", + "message": "\"import\"", "fullRange": {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]} {"version": 2, @@ -20,7 +20,7 @@ w "severity": 3, "range": {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}, - "message": "\"import\"\n", + "message": "\"import\"", "fullRange": {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]} {"version": 2, diff --git a/tests/lean/lcnfTypes.lean.expected.out b/tests/lean/lcnfTypes.lean.expected.out index 421747b562..a0a17428e9 100644 --- a/tests/lean/lcnfTypes.lean.expected.out +++ b/tests/lean/lcnfTypes.lean.expected.out @@ -6,8 +6,8 @@ Eq.rec : {α : Sort u_1} → {a : α} → {motive : α → ◾ → Sort u} → m GetElem.getElem : {coll : Type u} → {idx : Type v} → {elem : Type w} → {valid : coll → idx → Prop} → [self : GetElem coll idx elem ◾] → coll → idx → ◾ → elem -Term.constFold : {ctx : List Ty} → {ty : Ty} → Term ◾ ◾ → Term ◾ ◾ -Term.denote : {ctx : List Ty} → {ty : Ty} → Term ◾ ◾ → HList ◾ ◾ → ◾ +Term.constFold : {ctx : List Ty} → {ty : Ty} → _root_.Term ◾ ◾ → _root_.Term ◾ ◾ +Term.denote : {ctx : List Ty} → {ty : Ty} → _root_.Term ◾ ◾ → HList ◾ ◾ → ◾ HList.get : {α : Type u_1} → {β : α → Type u_2} → {is : List α} → {i : α} → HList β ◾ → Member ◾ ◾ → β ◾ Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member ◾ ◾ Ty.denote : Ty → Type @@ -15,32 +15,26 @@ MonadControl.liftWith : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → (({β : Type u} → n β → m ◾) → m α) → n α MonadControl.restoreM : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → m ◾ → n α Decidable.casesOn : {p : Prop} → {motive : Decidable ◾ → Sort u} → Decidable ◾ → (◾ → motive ◾) → (◾ → motive ◾) → motive ◾ -Lean.getConstInfo : {m : Type → Type} → - [inst : Monad m] → [inst : Lean.MonadEnv m] → [inst : Lean.MonadError m] → Lean.Name → m Lean.ConstantInfo +Lean.getConstInfo : {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstantInfo Lean.Meta.instMonadMetaM : Monad fun α => - Lean.Meta.Context → - ST.Ref PUnit Lean.Meta.State → - Lean.Core.Context → ST.Ref PUnit Lean.Core.State → PUnit → EStateM.Result Lean.Exception PUnit α -Lean.Meta.inferType : Lean.Expr → - Lean.Meta.Context → - ST.Ref PUnit Lean.Meta.State → - Lean.Core.Context → ST.Ref PUnit Lean.Core.State → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr -Lean.Elab.Term.elabTerm : Lean.Syntax → - Option Lean.Expr → + Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit α +Lean.Meta.inferType : Expr → + Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr +Lean.Elab.Term.elabTerm : Syntax → + Option Expr → Bool → Bool → - Lean.Elab.Term.Context → - ST.Ref PUnit Lean.Elab.Term.State → - Lean.Meta.Context → - ST.Ref PUnit Lean.Meta.State → - Lean.Core.Context → ST.Ref PUnit Lean.Core.State → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr + Elab.Term.Context → + ST.Ref PUnit Elab.Term.State → + Context → + ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr Nat.add : Nat → Nat → Nat Magma.mul : Magma → ◾ → ◾ → ◾ weird1 : Bool → ◾ lamAny₁ : Bool → Monad ◾ lamAny₂ : Bool → Monad ◾ -Term.constFold : List Ty → Ty → Term lcErased lcErased → Term lcErased lcErased -Term.denote : List Ty → Ty → Term lcErased lcErased → HList Ty lcErased lcErased → lcErased +Term.constFold : List Ty → Ty → _root_.Term lcErased lcErased → _root_.Term lcErased lcErased +Term.denote : List Ty → Ty → _root_.Term lcErased lcErased → HList Ty lcErased lcErased → lcErased HList.get : lcErased → lcErased → List lcErased → lcErased → HList lcErased lcErased lcErased → Member lcErased lcErased lcErased → lcErased Member.head : lcErased → lcErased → List lcErased → Member lcErased lcErased lcErased @@ -49,18 +43,15 @@ MonadControl.liftWith : lcErased → lcErased → MonadControl lcErased lcErased → lcErased → ((lcErased → lcErased → lcErased) → lcErased) → lcErased MonadControl.restoreM : lcErased → lcErased → MonadControl lcErased lcErased → lcErased → lcErased → lcErased Decidable.casesOn : lcErased → lcErased → Bool → (lcErased → lcErased) → (lcErased → lcErased) → lcErased -Lean.getConstInfo : lcErased → Monad lcErased → Lean.MonadEnv lcErased → Lean.MonadError lcErased → Lean.Name → lcErased +Lean.getConstInfo : lcErased → Monad lcErased → MonadEnv lcErased → MonadError lcErased → Name → lcErased Lean.Meta.instMonadMetaM : Monad lcErased -Lean.Meta.inferType : Lean.Expr → - Lean.Meta.Context → lcErased → Lean.Core.Context → lcErased → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr -Lean.Elab.Term.elabTerm : Lean.Syntax → - Option Lean.Expr → +Lean.Meta.inferType : Expr → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr +Lean.Elab.Term.elabTerm : Syntax → + Option Expr → Bool → Bool → - Lean.Elab.Term.Context → - lcErased → - Lean.Meta.Context → - lcErased → Lean.Core.Context → lcErased → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr + Elab.Term.Context → + lcErased → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr Nat.add : Nat → Nat → Nat Fin.add : Nat → Nat → Nat → Nat Lean.HashSetBucket.update : lcErased → Array (List lcErased) → USize → List lcErased → lcErased → Array (List lcErased) diff --git a/tests/lean/metaEvalInstMessage.lean.expected.out b/tests/lean/metaEvalInstMessage.lean.expected.out index deca4dde75..193a0cfad8 100644 --- a/tests/lean/metaEvalInstMessage.lean.expected.out +++ b/tests/lean/metaEvalInstMessage.lean.expected.out @@ -1,7 +1,2 @@ -metaEvalInstMessage.lean:5:0-5:12: error: expression - double -has type +metaEvalInstMessage.lean:5:0-5:5: error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type Nat → Nat -but instance - Lean.MetaEval (Nat → Nat) -failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class diff --git a/tests/lean/mkProjStx.lean.expected.out b/tests/lean/mkProjStx.lean.expected.out index 1a93f58c5b..5fdd564176 100644 --- a/tests/lean/mkProjStx.lean.expected.out +++ b/tests/lean/mkProjStx.lean.expected.out @@ -1,6 +1,3 @@ A.x (B.toA (C.toB c)) - B.y (C.toB c) - C.z c - diff --git a/tests/lean/moduleOf.lean.expected.out b/tests/lean/moduleOf.lean.expected.out index d6367fdfcb..561cf0e8da 100644 --- a/tests/lean/moduleOf.lean.expected.out +++ b/tests/lean/moduleOf.lean.expected.out @@ -4,4 +4,4 @@ (some Lean.Data.HashMap) none none -moduleOf.lean:16:0-16:9: error: unknown constant 'foo' +moduleOf.lean:16:0-16:5: error: unknown constant 'foo' diff --git a/tests/lean/partialIssue.lean.expected.out b/tests/lean/partialIssue.lean.expected.out index 8f7d2f7be8..96c3fe9e1b 100644 --- a/tests/lean/partialIssue.lean.expected.out +++ b/tests/lean/partialIssue.lean.expected.out @@ -1,2 +1 @@ - partialIssue.lean:12:8-12:19: error: (kernel) invalid declaration, safe declaration must not contain partial declaration 'False_intro' diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index 4f213ccb44..b916606b2f 100644 --- a/tests/lean/phashmap_inst_coherence.lean.expected.out +++ b/tests/lean/phashmap_inst_coherence.lean.expected.out @@ -6,5 +6,3 @@ 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 expression that depends on the `sorry` axiom. -Use `#eval!` to evaluate nevertheless (which may cause lean to crash). diff --git a/tests/lean/promise.lean.expected.out b/tests/lean/promise.lean.expected.out index 139597f9cb..e69de29bb2 100644 --- a/tests/lean/promise.lean.expected.out +++ b/tests/lean/promise.lean.expected.out @@ -1,2 +0,0 @@ - - diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out index 6493d7e393..3b61b9f603 100644 --- a/tests/lean/prvCtor.lean.expected.out +++ b/tests/lean/prvCtor.lean.expected.out @@ -1,8 +1,5 @@ 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 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 diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean index bb8d15715c..7f0013e2c2 100644 --- a/tests/lean/run/1697.lean +++ b/tests/lean/run/1697.lean @@ -3,9 +3,6 @@ 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.elim (by decide) @@ -13,8 +10,10 @@ Use `#eval!` to evaluate nevertheless (which may cause lean to crash). /-- 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). +error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to +runtime instability and crashes. + +To attempt to evaluate anyway despite the risks, use the '#eval!' command. -/ #guard_msgs in #eval #[1,2,3][2]'sorry diff --git a/tests/lean/run/2291.lean b/tests/lean/run/2291.lean index 5ed21647f0..d3520cb313 100644 --- a/tests/lean/run/2291.lean +++ b/tests/lean/run/2291.lean @@ -7,7 +7,107 @@ The following example would cause the pretty printer to panic. -/ set_option trace.compiler.simp true in -/-- info: [0] -/ +/-- +info: [compiler.simp] >> _eval +let _x_21 := `Nat; +let _x_22 := []; +let _x_23 := Lean.Expr.const _x_21 _x_22; +let _x_24 := `List.nil; +let _x_25 := Lean.levelZero :: _x_22; +let _x_26 := Lean.Expr.const _x_24 _x_25; +let _x_27 := _x_26.app _x_23; +let _x_28 := `List.cons; +let _x_29 := Lean.Expr.const _x_28 _x_25; +let _x_30 := _x_29.app _x_23; +let _x_31 := []; +let _x_32 := 0 :: _x_31; +let _x_33 := Lean.List.toExprAux _x_27 _x_30 _x_32; +Lean.MessageData.ofExpr _x_33 +[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1 +fun nilFn consFn x => + List.casesOn fun head tail => + let _x_1 := Lean.mkNatLit head; + let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail; + Lean.mkAppB consFn _x_1 _x_2 +>> _eval +let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat"; +let _x_15 := List.nil _neutral; +let _x_16 := Lean.Expr.const._override _x_14 _x_15; +let _x_17 := `List.nil; +let _x_18 := List.cons _neutral Lean.levelZero _x_15; +let _x_19 := Lean.Expr.const._override _x_17 _x_18; +let _x_20 := Lean.Expr.app._override _x_19 _x_16; +let _x_21 := `List.cons; +let _x_22 := Lean.Expr.const._override _x_21 _x_18; +let _x_23 := Lean.Expr.app._override _x_22 _x_16; +let _x_24 := List.cons _neutral 0 _x_15; +let _x_25 := Lean.List.toExprAux._at._eval._spec_1 _x_20 _x_23 _x_24; +Lean.MessageData.ofExpr _x_25 +[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1 +fun nilFn consFn x => + List.casesOn fun head tail => + let _x_1 := Lean.mkNatLit head; + let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail; + Lean.mkAppB consFn _x_1 _x_2 +>> _eval +let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat"; +let _x_2 := List.nil _neutral; +let _x_3 := Lean.Expr.const._override _x_1 _x_2; +let _x_4 := `List.nil; +let _x_5 := List.cons _neutral Lean.levelZero _x_2; +let _x_6 := Lean.Expr.const._override _x_4 _x_5; +let _x_7 := Lean.Expr.app._override _x_6 _x_3; +let _x_8 := `List.cons; +let _x_9 := Lean.Expr.const._override _x_8 _x_5; +let _x_10 := Lean.Expr.app._override _x_9 _x_3; +let _x_11 := List.cons _neutral 0 _x_2; +let _x_12 := Lean.List.toExprAux._at._eval._spec_1 _x_7 _x_10 _x_11; +Lean.MessageData.ofExpr _x_12 +[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1 +fun nilFn consFn x => + List.casesOn fun head tail => + let _x_1 := Lean.mkNatLit head; + let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail; + Lean.mkAppB consFn _x_1 _x_2 +>> _eval._closed_1 +"Nat" +>> _eval._closed_2 +Lean.Name.str._override Lean.Name.anonymous._impl _eval._closed_1 +>> _eval._closed_3 +let _x_1 := List.nil _neutral; +Lean.Expr.const._override _eval._closed_2 _x_1 +>> _eval._closed_4 +"List" +>> _eval._closed_5 +"nil" +>> _eval._closed_6 +Lean.Name.mkStr2 _eval._closed_4 _eval._closed_5 +>> _eval._closed_7 +let _x_1 := List.nil _neutral; +List.cons _neutral Lean.levelZero _x_1 +>> _eval._closed_8 +Lean.Expr.const._override _eval._closed_6 _eval._closed_7 +>> _eval._closed_9 +Lean.Expr.app._override _eval._closed_8 _eval._closed_3 +>> _eval._closed_10 +"cons" +>> _eval._closed_11 +Lean.Name.mkStr2 _eval._closed_4 _eval._closed_10 +>> _eval._closed_12 +Lean.Expr.const._override _eval._closed_11 _eval._closed_7 +>> _eval._closed_13 +Lean.Expr.app._override _eval._closed_12 _eval._closed_3 +>> _eval._closed_14 +let _x_1 := List.nil _neutral; +List.cons _neutral 0 _x_1 +>> _eval +let _x_1 := + Lean.List.toExprAux._at._eval._spec_1 _eval._closed_9 _eval._closed_13 + _eval._closed_14; +Lean.MessageData.ofExpr _x_1 +--- +info: [0] +-/ #guard_msgs in #eval [0] diff --git a/tests/lean/run/3713.lean b/tests/lean/run/3713.lean index 2a30073249..5884ff62d6 100644 --- a/tests/lean/run/3713.lean +++ b/tests/lean/run/3713.lean @@ -5,12 +5,7 @@ def somethingBad : MetaM Nat := do IO.println "oh no" return 1 -/-- -error: invalid use of `(<- ...)`, must be nested inside a 'do' expression ---- -error: cannot evaluate expression that depends on the `sorry` axiom. -Use `#eval!` to evaluate nevertheless (which may cause lean to crash). --/ +/-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -/ #guard_msgs in #eval show MetaM Unit from do let t := if false then ← somethingBad else 9 @@ -18,12 +13,7 @@ Use `#eval!` to evaluate nevertheless (which may cause lean to crash). def foo : MetaM Bool := return false -/-- -error: invalid use of `(<- ...)`, must be nested inside a 'do' expression ---- -error: cannot evaluate expression that depends on the `sorry` axiom. -Use `#eval!` to evaluate nevertheless (which may cause lean to crash). --/ +/-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -/ #guard_msgs in #eval show MetaM Unit from do let t := if (← foo) then ← somethingBad else 9 diff --git a/tests/lean/run/677.lean b/tests/lean/run/677.lean index f214af63ae..a966a9b790 100644 --- a/tests/lean/run/677.lean +++ b/tests/lean/run/677.lean @@ -5,7 +5,7 @@ def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do let json := toJson x fromJson? json -/-- info: Lean.Name.mkNum Lean.Name.anonymous 5 -/ +/-- info: Name.anonymous.num 5 -/ #guard_msgs in #eval IO.ofExcept <| encodeDecode (Name.mkNum Name.anonymous 5) diff --git a/tests/lean/run/DefEqAssignBug.lean b/tests/lean/run/DefEqAssignBug.lean index 3ecb3642e8..ecc71a259f 100644 --- a/tests/lean/run/DefEqAssignBug.lean +++ b/tests/lean/run/DefEqAssignBug.lean @@ -26,10 +26,8 @@ withLocalDeclD `x nat fun x => do set_option trace.Meta true -/-- info: -/ #guard_msgs in #eval tst1 -/-- info: -/ #guard_msgs in #eval tst2 diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean index 628680e854..b8a0f1f9fc 100644 --- a/tests/lean/run/ExprLens.lean +++ b/tests/lean/run/ExprLens.lean @@ -79,7 +79,6 @@ def testTraversal if not (← liftM $ isDefEq e e') then throwError "\n{e} \nand \n{e'} are different!" -/-- info: -/ #guard_msgs in #eval ((do testTraversal traverseLambdaWithPos 1 diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean index c942e12668..1150b2b71e 100644 --- a/tests/lean/run/IO_test.lean +++ b/tests/lean/run/IO_test.lean @@ -32,7 +32,6 @@ withFile "foo.txt" Mode.read fun h => do check_eq "5" [] ys.toList pure () -/-- info: -/ #guard_msgs in #eval test @@ -135,6 +134,5 @@ check_eq "1" [] ys.toList let ys ← withFile fn4 Mode.read $ fun h => h.read 1; check_eq "2" [] ys.toList -/-- info: -/ #guard_msgs in #eval test4 diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean index 844d64d5d5..5b047f4e72 100644 --- a/tests/lean/run/array1.lean +++ b/tests/lean/run/array1.lean @@ -62,7 +62,8 @@ info: 1 2 3 4 -[12, 14] +--- +info: [12, 14] -/ #guard_msgs in #eval tst diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean index 7b66206b44..4e6376af04 100644 --- a/tests/lean/run/catchThe.lean +++ b/tests/lean/run/catchThe.lean @@ -21,7 +21,6 @@ def g1 : M Nat := (tryCatchThe String act1 (fun ex => pure 100)) (fun ex => pure 200) -/-- info: -/ #guard_msgs in #eval testM g1 200 @@ -33,7 +32,6 @@ tryCatchThe Exception (tryCatchThe String act2 (fun ex => pure 100)) (fun ex => pure 200) -/-- info: -/ #guard_msgs in #eval testM g2 100 diff --git a/tests/lean/run/core.lean b/tests/lean/run/core.lean index c861dee682..bf8fa849b3 100644 --- a/tests/lean/run/core.lean +++ b/tests/lean/run/core.lean @@ -15,7 +15,8 @@ pure 10; /-- info: ([mdata borrowed:1 Nat]) -> ([mdata borrowed:1 Nat]) -> Nat testing... -10 +--- +info: 10 -/ #guard_msgs in #eval f @@ -25,8 +26,10 @@ set_option trace.Elab true /-- info: ([mdata borrowed:1 Nat]) -> ([mdata borrowed:1 Nat]) -> Nat testing... -[Elab] trace message -10 +--- +info: 10 +--- +info: [Elab] trace message -/ #guard_msgs in #eval f diff --git a/tests/lean/run/csimpAttrFn.lean b/tests/lean/run/csimpAttrFn.lean index 15331a32d5..5160cabbed 100644 --- a/tests/lean/run/csimpAttrFn.lean +++ b/tests/lean/run/csimpAttrFn.lean @@ -3,14 +3,11 @@ import Lean open Lean open Lean.Compiler -/-- info: -/ #guard_msgs in #eval (do assert! hasCSimpAttribute (← getEnv) ``List.map_eq_mapTR : MetaM Unit) -/-- info: -/ #guard_msgs in #eval (do assert! hasCSimpAttribute (← getEnv) ``List.append_eq_appendTR : MetaM Unit) -/-- info: -/ #guard_msgs in #eval (do assert! !hasCSimpAttribute (← getEnv) ``List.append : MetaM Unit) diff --git a/tests/lean/run/doElemAsTermNotation.lean b/tests/lean/run/doElemAsTermNotation.lean index 342a5f5672..9424f43f25 100644 --- a/tests/lean/run/doElemAsTermNotation.lean +++ b/tests/lean/run/doElemAsTermNotation.lean @@ -6,7 +6,6 @@ def f1 (x : Nat) : IO Unit := #guard_msgs in #eval f1 0 -/-- info: -/ #guard_msgs in #eval f1 100 @@ -28,7 +27,8 @@ def f3 (x : Nat) : IO Nat := /-- info: 5 at catch: failed -0 +--- +info: 0 -/ #guard_msgs in #eval f3 5 diff --git a/tests/lean/run/doLetElse.lean b/tests/lean/run/doLetElse.lean index bf6f692c05..fd676182cd 100644 --- a/tests/lean/run/doLetElse.lean +++ b/tests/lean/run/doLetElse.lean @@ -10,7 +10,6 @@ def testFoo (input : Option Nat) (expected : Nat) : IO Unit := do #guard_msgs in #eval testFoo (some 10) 10 -/-- info: -/ #guard_msgs in #eval testFoo none 0 @@ -27,14 +26,11 @@ def bar (x : Nat) : IO (Fin (x + 1)) := do def testBar (x : Nat) (expected : Fin (x + 1)) : IO Unit := do assert! (← bar x) == expected -/-- info: -/ #guard_msgs in #eval testBar 1 0 -/-- info: -/ #guard_msgs in #eval testBar 2 1 -/-- info: -/ #guard_msgs in #eval testBar 3 0 diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean index 1c78c8c5cd..64d9c58240 100644 --- a/tests/lean/run/doNotation1.lean +++ b/tests/lean/run/doNotation1.lean @@ -121,7 +121,8 @@ else /-- info: first field is zero -((), 0, 2) +--- +info: ((), 0, 2) -/ #guard_msgs in #eval tst7.run (0, 2) diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean index 9d746d9bd8..b5f361a3db 100644 --- a/tests/lean/run/doNotation2.lean +++ b/tests/lean/run/doNotation2.lean @@ -22,7 +22,8 @@ aux started y: 10, z: 10 aux started y: 10, z: 10 -20 +--- +info: 20 -/ #guard_msgs in #eval f 10 @@ -36,14 +37,16 @@ return xs.length /-- info: >>> xs: [1, 2, 3] -3 +--- +info: 3 -/ #guard_msgs in #eval g [1, 2, 3] |>.run' 10 /-- info: >>> xs: [10] -1 +--- +info: 1 -/ #guard_msgs in #eval g [] |>.run' 10 @@ -86,7 +89,8 @@ return sum info: >> x: 1 >> x: 3 >> x: 5 -16 +--- +info: 16 -/ #guard_msgs in #eval sumOdd [1, 2, 3, 4, 5, 6, 7, 9, 11, 101] 10 @@ -193,7 +197,8 @@ def f5 (x y : Nat) : Nat × Nat := Id.run <| do /-- info: z: 4 -(11, 6) +--- +info: (11, 6) -/ #guard_msgs in #eval f5 5 6 diff --git a/tests/lean/run/doNotation5.lean b/tests/lean/run/doNotation5.lean index c131fc2304..5b1852fda8 100644 --- a/tests/lean/run/doNotation5.lean +++ b/tests/lean/run/doNotation5.lean @@ -24,14 +24,16 @@ catch ex : Nat => /-- info: nat exception 1010 -(Except.ok (Except.ok 1010), 1000) +--- +info: (Except.ok (Except.ok 1010), 1000) -/ #guard_msgs in #eval (f 10 20).run 1000 /-- info: string exception balance is zero -(Except.ok (Except.ok 1000), 20) +--- +info: (Except.ok (Except.ok 1000), 20) -/ #guard_msgs in #eval (f 10 200).run 10 diff --git a/tests/lean/run/doNotation6.lean b/tests/lean/run/doNotation6.lean index 21ecc65b5f..9098081718 100644 --- a/tests/lean/run/doNotation6.lean +++ b/tests/lean/run/doNotation6.lean @@ -80,7 +80,8 @@ return sum info: 1 2 3 -6 +--- +info: 6 -/ #guard_msgs in #eval f4 #[1, 2, 3] @@ -97,7 +98,8 @@ info: 2 3 4 5 -14 +--- +info: 14 -/ #guard_msgs in #eval f5 #[1, 2, 3, 4, 5, 6] diff --git a/tests/lean/run/eval.lean b/tests/lean/run/eval.lean new file mode 100644 index 0000000000..f098698cb6 --- /dev/null +++ b/tests/lean/run/eval.lean @@ -0,0 +1,179 @@ +import Lean +/-! +# Tests of the `#eval` command +-/ + +set_option eval.type true + +/-! +Basic values +-/ +/-- info: 2 : Nat -/ +#guard_msgs in #eval 2 +/-- info: some 2 : Option Nat -/ +#guard_msgs in #eval some 2 +/-- info: [2, 3, 4] : List Nat -/ +#guard_msgs in #eval [1,2,3].map (· + 1) + +/-! +Deciding a proposition +-/ +/-- info: true : Bool -/ +#guard_msgs in #eval True + +/-! +Can't evaluate proofs +-/ +/-- error: cannot evaluate, proofs are not computationally relevant -/ +#guard_msgs in #eval trivial + +/-! +Can't evaluate types +-/ +/-- error: cannot evaluate, types are not computationally relevant -/ +#guard_msgs in #eval Nat + + +/-! +Capturing `dbg_trace` output +-/ +def Nat.choose : Nat → Nat → Nat + | _, 0 => dbg_trace "(_, 0)"; 1 + | 0, _ + 1 => dbg_trace "(0, _ + 1)"; 0 + | n + 1, k + 1 => dbg_trace "(_ + 1, _ + 1)"; choose n k + choose n (k + 1) +/-- +info: (_ + 1, _ + 1) +(_ + 1, _ + 1) +(_, 0) +(0, _ + 1) +(_ + 1, _ + 1) +(0, _ + 1) +(0, _ + 1) +--- +info: 1 : Nat +-/ +#guard_msgs in #eval Nat.choose 2 2 + +/-! +Custom monad +-/ + +abbrev MyMonad := ReaderT Nat IO +/-- +error: unable to synthesize 'MonadEval' instance to adapt + MyMonad Nat +to 'IO' or 'Lean.Elab.Command.CommandElabM'. +-/ +#guard_msgs in #eval (pure 2 : MyMonad Nat) + +-- Note that there is no "this is due to..." diagonostic in this case. +/-- +error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type + MyMonad (Nat → Nat) +-/ +#guard_msgs in #eval (pure id : MyMonad (Nat → _)) + +instance : MonadEval MyMonad IO where + monadEval m := m.run 0 + +/-- info: 2 : Nat -/ +#guard_msgs in #eval (pure 2 : MyMonad Nat) + +-- Note that now we have a MonadEval instance, it doesn't mention MyMonad in the error. +/-- +error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type + Nat → Nat +-/ +#guard_msgs in #eval (pure id : MyMonad (Nat → _)) + +/-! +Elaboration error, does not attempt to evaluate. +-/ +/-- error: unknown identifier 'x' -/ +#guard_msgs in #eval 2 + x + +/-! +Defaulting to the CommandElabM monad +-/ +/-- info: 2 : Nat -/ +#guard_msgs in #eval do pure 2 +/-- info: true : Bool -/ +#guard_msgs in #eval do return (← Lean.getEnv).contains ``Lean.MessageData + +/-! +Defaulting does not affect postponed elaborators. +-/ +/-- info: 1 : Nat -/ +#guard_msgs in #eval if True then 1 else 2 + +/-! +Testing that dbg_trace and logs carry over from all the major meta monads. +-/ +/-- +info: hi +--- +info: dbg +-/ +#guard_msgs in #eval show Lean.Elab.Term.TermElabM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi" +/-- +info: hi +--- +info: dbg +-/ +#guard_msgs in #eval show Lean.MetaM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi" +/-- +info: hi +--- +info: dbg +-/ +#guard_msgs in #eval show Lean.CoreM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi" + +/-! +Testing delta deriving +-/ +def Foo := List Nat +def Foo.mk (l : List Nat) : Foo := l + +/-- info: [1, 2, 3] : Foo -/ +#guard_msgs in #eval Foo.mk [1,2,3] + +/-- info: [1, 2, 3] : Foo -/ +#guard_msgs in #eval do return Foo.mk [1,2,3] + +/-! +Testing auto-deriving +-/ + +inductive Baz + | a | b + +/-- info: Baz.a : Baz -/ +#guard_msgs in #eval Baz.a + +/-! +Returning after printing +-/ +def returns : Lean.CoreM Nat := do + IO.println "hi" + return 2 + +/-- +info: hi +--- +info: 2 : Nat +-/ +#guard_msgs in #eval returns + +/-! +Throwing an exception after printing +-/ +def throwsEx : Lean.CoreM Nat := do + IO.println "hi" + throwError "ex" + +/-- +info: hi +--- +error: ex +-/ +#guard_msgs in #eval throwsEx diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean index ebad7d7525..d1f6bb1fa1 100644 --- a/tests/lean/run/expr1.lean +++ b/tests/lean/run/expr1.lean @@ -74,7 +74,6 @@ do let f := mkConst `f []; unless (!t2.hasLooseBVar 1) do throw $ IO.userError "failed-6"; pure () -/-- info: -/ #guard_msgs in #eval tst4 diff --git a/tests/lean/run/finally.lean b/tests/lean/run/finally.lean index 0f6d64563b..516ef1ecbd 100644 --- a/tests/lean/run/finally.lean +++ b/tests/lean/run/finally.lean @@ -23,7 +23,8 @@ match r with /-- info: finisher executed -Except.ok 100 +--- +info: Except.ok 100 -/ #guard_msgs in #eval (tst1.run).run' 0 @@ -39,7 +40,8 @@ tryCatchThe IO.Error /-- info: finisher executed -Except.ok 100 +--- +info: Except.ok 100 -/ #guard_msgs in #eval (tst2.run).run' 0 @@ -58,7 +60,8 @@ tryCatchThe IO.Error /-- info: inner finisher executed outer finisher executed -Except.ok 101 +--- +info: Except.ok 101 -/ #guard_msgs in #eval (tst3.run).run' 0 @@ -80,7 +83,8 @@ pure (a + s) /-- info: inner finisher executed outer finisher executed -Except.ok 143 +--- +info: Except.ok 143 -/ #guard_msgs in #eval (tst4.run).run' 0 @@ -98,7 +102,8 @@ pure a /-- info: finalizer received: (some 42) -Except.ok 42 +--- +info: Except.ok 42 -/ #guard_msgs in #eval (tst5.run).run' 0 diff --git a/tests/lean/run/float_from_bignum.lean b/tests/lean/run/float_from_bignum.lean index 78330724c3..9acdded94f 100644 --- a/tests/lean/run/float_from_bignum.lean +++ b/tests/lean/run/float_from_bignum.lean @@ -9,6 +9,5 @@ def tst1 : IO Unit := do check (Nat.toFloat (10^80) > Nat.toFloat (10^40)); pure () -/-- info: -/ #guard_msgs in #eval tst1 diff --git a/tests/lean/run/forInPArray.lean b/tests/lean/run/forInPArray.lean index f94119d395..4ee973dab8 100644 --- a/tests/lean/run/forInPArray.lean +++ b/tests/lean/run/forInPArray.lean @@ -19,7 +19,8 @@ return sum info: x: 2 x: 4 x: 10 -16 +--- +info: 16 -/ #guard_msgs in #eval f1 [1, 2, 3, 4, 5, 10, 20].toPArray' 10 diff --git a/tests/lean/run/getline_crash.lean b/tests/lean/run/getline_crash.lean index 4bbe148c1c..16009aa296 100644 --- a/tests/lean/run/getline_crash.lean +++ b/tests/lean/run/getline_crash.lean @@ -146,18 +146,14 @@ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa #guard_msgs in #eval tstGetLine ("".pushn 'a' 128) -/-- info: -/ #guard_msgs in #eval tstGetLine2 ("".pushn 'α' 20) ("".pushn 'β' 20) -/-- info: -/ #guard_msgs in #eval tstGetLine2 ("".pushn 'α' 40) ("".pushn 'β' 40) -/-- info: -/ #guard_msgs in #eval tstGetLine2 ("".pushn 'a' 61) ("".pushn 'b' 61) -/-- info: -/ #guard_msgs in #eval tstGetLine2 ("".pushn 'a' 61) ("".pushn 'b' 62) diff --git a/tests/lean/run/handleLocking.lean b/tests/lean/run/handleLocking.lean index 4bc157d94a..0548480abe 100644 --- a/tests/lean/run/handleLocking.lean +++ b/tests/lean/run/handleLocking.lean @@ -17,7 +17,6 @@ def test1 : IO Unit := do unless (← h2.tryLock) do throw <| IO.userError "failed to unlock exclusive lock and then lock" -/-- info: -/ #guard_msgs in #eval test1 @@ -29,7 +28,6 @@ def test2 : IO Unit := do unless (← h.tryLock) do throw <| IO.userError "handle free failed to unlock" -/-- info: -/ #guard_msgs in #eval test2 @@ -47,6 +45,5 @@ def test3 : IO Unit := do unless (← h2.tryLock) do throw <| IO.userError "failed to unlock shared locks and then lock" -/-- info: -/ #guard_msgs in #eval test3 diff --git a/tests/lean/run/kernelInterrupt.lean b/tests/lean/run/kernelInterrupt.lean index f81b1f0110..2cca0d3b96 100644 --- a/tests/lean/run/kernelInterrupt.lean +++ b/tests/lean/run/kernelInterrupt.lean @@ -7,7 +7,6 @@ In particular, runtime exceptions such as `interrupted_exception` should properl -/ open Lean -/-- info: -/ #guard_msgs in #eval show CoreM _ from do let env ← getEnv diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean index 22f57da36d..4e90d65de1 100644 --- a/tests/lean/run/match1.lean +++ b/tests/lean/run/match1.lean @@ -23,7 +23,6 @@ xs.map fun | 0 => true | _ => false -/-- info: -/ #guard_msgs in #eval checkWithMkMatcherInput ``f.match_1 diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index 6151fc2d40..26b9130d7c 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -2,6 +2,8 @@ import Lean.Meta open Lean open Lean.Meta +set_option pp.mvars false + -- set_option trace.Meta true --set_option trace.Meta.isDefEq.step false -- set_option trace.Meta.isDefEq.delta false @@ -181,7 +183,11 @@ do print "----- tst7 -----"; checkM $ pure $ v == x; pure () -/-- info: [Meta.debug] ----- tst7 ----- -/ +/-- +error: check failed +--- +info: [Meta.debug] ----- tst7 ----- +-/ #guard_msgs in #eval tst7 @@ -591,9 +597,9 @@ withLocalDeclD `x nat $ fun x => do /-- info: [Meta.debug] ----- tst30 ----- -[Meta.debug] (?m.2 x).succ -[Meta.debug] ?m.4.succ -[Meta.debug] fun x => ?m.4 +[Meta.debug] (?_ x).succ +[Meta.debug] ?_.succ +[Meta.debug] fun x => ?_ -/ #guard_msgs in #eval tst30 @@ -670,7 +676,7 @@ withLocalDeclD `α type $ fun α => do /-- info: [Meta.debug] ----- tst34 ----- -[Meta.debug] fun α => ?m.3 α → ?m.3 α +[Meta.debug] fun α => ?_ α → ?_ α -/ #guard_msgs in #eval tst34 @@ -694,7 +700,7 @@ withLocalDeclD `α type $ fun α => do /-- info: [Meta.debug] ----- tst35 ----- -[Meta.debug] fun α => ?m.4 α → ?m.4 α +[Meta.debug] fun α => ?_ α → ?_ α [Meta.debug] fun α => α → α -/ #guard_msgs in @@ -730,7 +736,7 @@ withLocalDeclD `v nat $ fun v => do /-- info: [Meta.debug] ----- tst37 ----- -[Meta.debug] ?m.1 v (?m.2 v) +[Meta.debug] ?_ v (?_ v) [Meta.debug] StateM Nat Nat -/ #guard_msgs in diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean index e7181fa4d7..f9f7dc391b 100644 --- a/tests/lean/run/meta5.lean +++ b/tests/lean/run/meta5.lean @@ -19,19 +19,20 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do { trace[Meta.debug] m!"?{mvarId.name} : {mvarDecl.type}" } +set_option pp.mvars false set_option trace.Meta.debug true /-- -info: [Meta.debug] ?m.3 +info: [Meta.debug] ?_ [Meta.debug] x.add y [Meta.debug] fun y => let x := 0; x.add y -[Meta.debug] ?_uniq.4 : Nat → +[Meta.debug] ?_uniq.3014 : Nat +[Meta.debug] ?_uniq.3015 : Nat → Nat → let x := 0; Nat -[Meta.debug] ?_uniq.3 : Nat -/ #guard_msgs in #eval tst1 diff --git a/tests/lean/run/meta7.lean b/tests/lean/run/meta7.lean index 6951f08004..6e968a6a7d 100644 --- a/tests/lean/run/meta7.lean +++ b/tests/lean/run/meta7.lean @@ -259,7 +259,6 @@ def tst10 : MetaM Unit := do assert! (← getConstInfoInduct `Foo).isNested assert! !(← getConstInfoInduct `Prod).isNested -/-- info: -/ #guard_msgs in #eval tst10 diff --git a/tests/lean/run/monadControl.lean b/tests/lean/run/monadControl.lean index d27819610b..2270434ec4 100644 --- a/tests/lean/run/monadControl.lean +++ b/tests/lean/run/monadControl.lean @@ -20,7 +20,8 @@ pure a info: started hello ended -((Except.error "ERROR", "world"), 1011) +--- +info: ((Except.error "ERROR", "world"), 1011) -/ #guard_msgs in #eval (((tst.run true).run "world").run 1000).run 11 @@ -44,7 +45,8 @@ pure a info: started hello ended -((Except.ok (1015, true), "world"), 1016) +--- +info: ((Except.ok (1015, true), "world"), 1016) -/ #guard_msgs in #eval (((tst2.run true).run "world").run 1000).run 10 diff --git a/tests/lean/run/nicerNestedDos.lean b/tests/lean/run/nicerNestedDos.lean index db0b6e6430..d952a57568 100644 --- a/tests/lean/run/nicerNestedDos.lean +++ b/tests/lean/run/nicerNestedDos.lean @@ -7,7 +7,8 @@ def f (x : Nat) : IO Nat := do /-- info: hello -3 +--- +info: 3 -/ #guard_msgs in #eval f 2 @@ -16,7 +17,8 @@ info: hello info: hello x: 10 done -11 +--- +info: 11 -/ #guard_msgs in #eval f 10 diff --git a/tests/lean/run/ptrAddr.lean b/tests/lean/run/ptrAddr.lean index d2755f972e..04901e5ee2 100644 --- a/tests/lean/run/ptrAddr.lean +++ b/tests/lean/run/ptrAddr.lean @@ -14,7 +14,8 @@ def y := x /-- info: >> (1, 2) == (1, 2) -true +--- +info: true -/ #guard_msgs in #eval withPtrEq x (mk 1) (fun _ => dbgTrace (">> " ++ toString x ++ " == " ++ toString y) $ fun _ => x == y) TrustMe -- should print message diff --git a/tests/lean/run/readerThe.lean b/tests/lean/run/readerThe.lean index cbf3dfb27c..937b3db369 100644 --- a/tests/lean/run/readerThe.lean +++ b/tests/lean/run/readerThe.lean @@ -14,7 +14,8 @@ pure s /-- info: hello true -10 +--- +info: 10 -/ #guard_msgs in #eval (f "hello").run' 10 true @@ -26,7 +27,8 @@ withReader (fun s => s ++ " world") a /-- info: hello world false -10 +--- +info: 10 -/ #guard_msgs in #eval (g "hello").run' 10 true diff --git a/tests/lean/run/returnOptIssue.lean b/tests/lean/run/returnOptIssue.lean index d920457038..9e2e6f285b 100644 --- a/tests/lean/run/returnOptIssue.lean +++ b/tests/lean/run/returnOptIssue.lean @@ -4,6 +4,5 @@ if x > 10 then return throw $ IO.userError "x ≤ 10" -/-- info: -/ #guard_msgs in #eval f 11 diff --git a/tests/lean/run/stateRef.lean b/tests/lean/run/stateRef.lean index e12fcb8623..803330b67c 100644 --- a/tests/lean/run/stateRef.lean +++ b/tests/lean/run/stateRef.lean @@ -8,14 +8,16 @@ f 5 |>.run' 20 /-- info: hello -15 +--- +info: 15 -/ #guard_msgs in #eval (f 5).run' 20 /-- info: hello -95 +--- +info: 95 -/ #guard_msgs in #eval (do set 100; f 5 : StateRefT Nat IO Nat).run' 0 @@ -27,7 +29,8 @@ get /-- info: context 10 -30 +--- +info: 30 -/ #guard_msgs in #eval (f2.run 10).run' 20 @@ -43,7 +46,8 @@ getThe Nat /-- info: test, 10 -11 +--- +info: 11 -/ #guard_msgs in #eval (f3.run' "test").run' 10 @@ -74,7 +78,8 @@ pure (a0 + a1 + a2) info: state0 10 state1 20 state1 30 -60 +--- +info: 60 -/ #guard_msgs in #eval f4.run' ⟨10⟩ |>.run' ⟨20⟩ |>.run' ⟨30⟩ diff --git a/tests/lean/run/task_test.lean b/tests/lean/run/task_test.lean index 0facf13a70..71bdfc673b 100644 --- a/tests/lean/run/task_test.lean +++ b/tests/lean/run/task_test.lean @@ -23,7 +23,8 @@ pure 0 /-- info: 12 11 -0 +--- +info: 0 -/ #guard_msgs in #eval tst 10 diff --git a/tests/lean/run/task_test2.lean b/tests/lean/run/task_test2.lean index 890dca9350..10683a38cc 100644 --- a/tests/lean/run/task_test2.lean +++ b/tests/lean/run/task_test2.lean @@ -15,7 +15,8 @@ pure 0 /-- info: >> [100, 100, 100, 100, 100, 100, 100, 100, 100, 100] -0 +--- +info: 0 -/ #guard_msgs in #eval tst 10 diff --git a/tests/lean/run/termElab.lean b/tests/lean/run/termElab.lean index 0d9da58f26..c3eb954341 100644 --- a/tests/lean/run/termElab.lean +++ b/tests/lean/run/termElab.lean @@ -29,6 +29,5 @@ let e ← elabTermAndSynthesize stx none; trace[Elab.debug] m!">>> {e}"; throwErrorIfErrors -/-- info: -/ #guard_msgs in #eval tst2 diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index de028219c2..139c7444db 100644 --- a/tests/lean/run/trace.lean +++ b/tests/lean/run/trace.lean @@ -59,7 +59,8 @@ info: [module] message world [bughunt] at test2 ERROR -[module] message +--- +info: [module] message [module] hello world [bughunt] at test2 @@ -76,11 +77,13 @@ info: [module] message [module] hello world [bughunt] at end of tst3 -[module] message +--- +info: [module] message [module] hello world [bughunt] at test2 - [module] hello world + [module] hello + world [module] hello world [bughunt] at end of tst3 diff --git a/tests/lean/run_meta1.lean.expected.out b/tests/lean/run_meta1.lean.expected.out index 77e37d99ee..c3b0981ad3 100644 --- a/tests/lean/run_meta1.lean.expected.out +++ b/tests/lean/run_meta1.lean.expected.out @@ -1 +1 @@ -run_meta1.lean:1:0-1:19: error: to use this command, include `import Lean.Elab.Command` +run_meta1.lean:1:0-1:19: error: to use this command, include `import Lean.Meta.Basic` diff --git a/tests/lean/scientific.lean.expected.out b/tests/lean/scientific.lean.expected.out index 4c3f8880e8..4ead38b973 100644 --- a/tests/lean/scientific.lean.expected.out +++ b/tests/lean/scientific.lean.expected.out @@ -15,8 +15,6 @@ 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 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 @@ -25,9 +23,5 @@ 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 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 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 diff --git a/tests/lean/updateExprIssue.lean.expected.out b/tests/lean/updateExprIssue.lean.expected.out index 5e550af5df..10537d1e32 100644 --- a/tests/lean/updateExprIssue.lean.expected.out +++ b/tests/lean/updateExprIssue.lean.expected.out @@ -1,5 +1,4 @@ - [init] def sefFn (x_1 : obj) (x_2 : obj) : obj := case x_1 : obj of