trace simp

Stream: Is there code for X?

[Kenny Lau]

Is there a set_option to trace the steps taken by simp? I tried a few options but none of them does this.

[Johan Commelin]

Not what you asked, but do you know about simp? ?

[Kenny Lau]

yes, but that doesn't show me the intermediate steps

[Matthew Ballard]

Can you share which ones you’ve tried? I “think” set_option trace.Meta.Tactic.simp (off the top of my head) and its descendants have been ok for me.

[Johan Commelin]

And set_option tactic.simp.trace true is also not what you want?

... then I don't know.

[Kenny Lau]

Matthew Ballard said:

Can you share which ones you’ve tried? I “think” set_option trace.Meta.Tactic.simp (off the top of my head) and its descendants have been ok for me.

thanks! this one worked

[Kenny Lau]

Johan Commelin said:

And set_option tactic.simp.trace true is also not what you want?

... then I don't know.

this outputs the same thing as simp?.

[Yaël Dillies]

set_option trace.Meta.Tactic.simp.rewrite true is what you want

[Yaël Dillies]

This is quickly mentioned in the first simproc blogpost

[Matthew Ballard]

Also, there seems to be some redundancy with options for tracing simp right?

[Yaël Dillies]

Definitely! They are also still stuck in their half uppercase, half lowercase phase

[Matthew Ballard]

Is there an existing issue?

[Yaël Dillies]

I do not know, but I know @Cameron Zwarich is aware of the compiler vs Compiler discrepancy, and claims this is distinguishing new and old compiler

[Cameron Zwarich]

The problem with the compiler/Compiler options is known, and will probably be settled in a few releases after the old compiler is completely removed (probably in favor of using the Compiler name for everything?), but if there are similar issues elsewhere you should probably file a separate issue.

[Kenny Lau]

the problem is just that if I write set_option simp and then hit ctrl+space, i get 30 options

[Yaël Dillies]

I don't know. Happy to open one. @Cameron Zwarich is at least aware of trace.compiler vs trace.Compiler (old vs new compiler) and might be able to shed some light?

[Yaël Dillies]

Whoops sorry, I thought my first message went to limbo