#eval evaluates term with failing tactics

[gebner]

#eval show Nat from False.rec (by decide)

• In the server the file crashes.
• On the command line it prints unreachable code (original report produced incomplete case)

We should probably not eval terms where the elaborator fails.

Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/crash.20when.20using.20.22by.20decide.22/near/301853648

[leodemoura]

We should probably not eval terms where the elaborator fails.

+1

[david-christiansen]

I ran into this today when working on the book. In particular, #eval crashed the LSP server when asked to look up an invalid index in a list. Another example that triggers this:

#eval [1,2,3][9]

[leodemoura]

The following variant also crashes the LSP server

def foo :=
  [1,2,3][9]  -- Produces error here saying it failed to prove `... |- 9 < List.length [1, 2, 3]` as expected

-- `foo` is added to the environment with a `sorry` as a proof for ` ... |- 9 < ...`
-- `sorry` is erased during code generation 

#eval foo

[Kha]

#4745 suggests that we may not want to run terms that transitively depend on sorry either