feat: run_macro & run_cmd_macro

[tydeu]

This PR adds MacroM support to #eval with the associated run_macro convenience command. It also adds run_cmd_macro, which evaluates a MacroM Command and then immediately elaborates the produced command.

The run_cmd_macro utility circumvents the need to define local command syntax just to expand a single-use macro. For example:

-- # Previously
local macro "gen_stuff%" : command =>
  genStuff -- meta code to generate some commands
gen_stuff% -- perform the generation

-- # With this change
run_cmd_macro genStuff -- perform generation, no new syntax necessary

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-7524 build against this PR was cancelled. (2025-03-17 15:08:45) View Log
• ✅ Mathlib branch lean-pr-testing-7524 has successfully built against this PR. (2025-03-17 15:56:02) View Log
• ✅ Mathlib branch lean-pr-testing-7524 has successfully built against this PR. (2025-03-17 17:21:22) View Log