Zulip Chat Archive

Stream: general

Topic: set_option trace.simplify.rewrite true

Reid Barton (May 01 2020 at 12:35):

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 (May 01 2020 at 12:37):

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

Reid Barton (May 01 2020 at 12:38):

squeeze_simp is not quite as informative, though.

Reid Barton (May 01 2020 at 12:39):

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 (May 01 2020 at 12:40):

(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 (May 01 2020 at 12:44):

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

Reid Barton (May 01 2020 at 12:44):

Oh :question:

Gabriel Ebner (May 01 2020 at 12:47):

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

import tactic.interactive

namespace tactic
namespace interactive

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 :=

Reid Barton (May 01 2020 at 12:49):

Ah, I see :exclamation:

Gabriel Ebner (May 01 2020 at 13:05):

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

Reid Barton (Sep 08 2020 at 18:51):

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 (Sep 09 2020 at 04:18):

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

Reid Barton (Sep 09 2020 at 10:29):

Isn't that called squeeze_simp?

Gabriel Ebner (Sep 09 2020 at 11:10):

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

Reid Barton (Sep 09 2020 at 11:22):

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

Johan Commelin (Sep 09 2020 at 11:28):

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

Johan Commelin (Sep 09 2020 at 11:29):

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 (Sep 09 2020 at 11:33):

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

Johan Commelin (Sep 09 2020 at 11:33):

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

Reid Barton (Sep 09 2020 at 11:33):

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 (Sep 09 2020 at 11:34):

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?

Last updated: Dec 20 2023 at 11:08 UTC