set_option trace.simplify.rewrite true

Stream: general

[Reid Barton]

Maybe I am just extremely lazy, but I would really like a way to see what simp did without writing the 30+ characters making up the name of this topic somewhere that is often far away from the simp I am interested in. Perhaps we could add some lightweight syntax to simp, like simp? to enable the trace?

[Gabriel Ebner]

There's also another incantation that does something slight different but requires only 8 additional characters: squeeze_simp.

[Reid Barton]

squeeze_simp is not quite as informative, though.

[Reid Barton]

squeeze_simp feels like I have just transformed the puzzle of guessing what simp is doing into the puzzle of understanding the squeeze_simp output. (I know its primary purpose is something else.)

[Reid Barton]

(In particular, I might actually want to replace the simp with a rw or something, and that's hard to judge from squeeze_simp output.)

[Gabriel Ebner]

I also think this would be a great addition. We don't even need to change core for this.

[Reid Barton]

Oh :question:

[Gabriel Ebner]

This "works" except that set_bool_option `trace.simplify.rewrite` tt has no effect. :sad:

import tactic.interactive

namespace tactic
namespace interactive
setup_tactic_parser

reserve notation `simp?`

meta def «simp?» (use_iota_eqn : parse $ (tk "!")?) (no_dflt : parse only_flag)
  (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
  (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit := do
o ← get_options,
set_bool_option `trace.simplify.rewrite tt,
tactic.interactive.simp use_iota_eqn no_dflt hs attr_names locat cfg,
set_options o

end interactive
end tactic

example (x) : 0+x=x :=
begin
  simp?,
end

[Reid Barton]

Ah, I see :exclamation:

[Gabriel Ebner]

Unfortunately there doesn't seem to be any way to enable trace options without changes in the C++ code.

[Reid Barton]

Now that set_bool_option `trace.simplify.rewrite tt has the desired effect, is the above «simp?» method the best way to do this? Or would it be better to just add the flag in core?

[Johan Commelin]

I would love to have simp?, but ideally with the helpful Try this: messages that squeeze_simp gives.

[Reid Barton]

Isn't that called squeeze_simp?

[Gabriel Ebner]

I think the proposal is to rename squeeze_simp to simp? (like rcases?, etc.), and call the name tracing simp simp?!.

[Reid Barton]

this reminds me that ! is already an option to simp, but I have no idea what it does

[Johan Commelin]

Wait, shouldn't simp? use the name tracing, and replace squeeze_simp?

[Johan Commelin]

Maybe I don't understand enough of the details of what has changed. But I thought that with the C++ changes, we could write a better squeeze_simp

[Reid Barton]

The only C++ change is (in effect) that you can turn on trace.simplify.rewrite from inside a tactic block.

[Johan Commelin]

Right. And that should allow a tactic to build better squeeze_simp output, right?

[Reid Barton]

More precisely, when the C++ part of the simplifier is entered, it uses the current options rather than the ones which were in effect when the declaration began.

[Reid Barton]

I have no idea, I just want to see the output of trace.simplify.rewrite! I don't think there is a tactic interface to that, but maybe?