run_cmd and unsafe

Stream: lean4

[Eric Wieser]

Is there a way I can make run_cmd accept this?

import Mathlib.Tactic.RunCmd
import Mathlib.Data.Quot
import Mathlib.Data.Nat.Basic

unsafe def magic : ℕ := (Trunc.mk 37).unquot

unsafe def test_magic : Lean.Elab.Command.CommandElabM Unit  :=
unless magic = 37 do throwError "got {magic}"

#eval magic -- ok, prints 37
run_cmd test_magic -- fails!

It currently complains that

(kernel) invalid declaration, it uses unsafe declaration 'test_magic'

[Mario Carneiro]

yes, the declaration needs to be marked unsafe before being passed to addAndCompile

[Eric Wieser]

Are you describing something that needs fixing in core?

[Mario Carneiro]

no

[Eric Wieser]

How do I mark it unsafe, if not via unsafe?

[Mario Carneiro]

In elabRunElab there is a call to evalTerm which has an optional safety argument

[Eric Wieser]

Oh, I hadn't realized docs4#Mathlib.RunCmd.elabRunElab was not in core! (as I didn't know its name)

[Sebastian Ullrich]

Would run_cmd unsafe ... not work?

[Mario Carneiro]

I suppose it would

[Sebastian Ullrich]

To make sure you still have to mention a magic spell to break out of unsafe

[Eric Wieser]

Oh, that works fine

[Eric Wieser]

What's the rule behind when the unsafe keyword is needed? I thought it was only valid on declarations

[Mario Carneiro]

It is, but there is a mathlib (now std) syntax Std.Tactic.TermUnsafe which allows using it in term position

[Mario Carneiro]

it is much simpler than what is done in core which is to make an opaque definition, use implemented_by to point the compiler to an unsafe declaration and then write the rest of the program there

[Mario Carneiro]

in fact elabRunElab and friends contain a use of term-unsafe to call evalTerm, which is an unsafe declaration