simps?, reassoc?, mk_iff?

Stream: general

[Scott Morrison]

A proposal: all attributes on declarations which generate auxiliary declarations should have a ? mode, which behaves just as normal but prints a trace message, either

1. listing the full names of the new declarations
2. printing the full types of the new declarations

[Scott Morrison]

For me at least, it is a common problem deciphering what exactly has been generated. @[simps] has set_option trace.simps.verbose and set_option trace.simps.debug, but I would like a common interface, ideally extremely quick to add or remove in place: hence the proposal for ?.

[Bhavik Mehta]

Scott Morrison said:

A proposal: all attributes on declarations which generate auxiliary declarations should have a ? mode, which behaves just as normal but prints a trace message, either

1. listing the full names of the new declarations
2. printing the full types of the new declarations

I think both of those!

[Bhavik Mehta]

By the way my temporary work-around for this problem is to use #print prefix afterwards, but I agree a ? would be better

[Kevin Buzzard]

I would like to see instanceoptionally report the name of the def it made too :-) I can never remember the rules and if I'm in mathlib I might not know if I'm in a namespace etc

[Scott Morrison]

Yeah. I wonder if we should just outlaw unnamed instances.

[Johan Commelin]

The problem with instance? is that it causes 85% of mathlib to recompile, if you use it on an instance low in the hierarchy

[Damiano Testa]

As a user who is just becoming aware of these ghosts produced by Lean, I am finding this thread very useful! Besides having a question mark, is there a way to simply know that Lean is producing more stuff than what I am actually typing?

I know that print prefix will sometimes give you more information, but I do not know when it would be useful. On a separate note, I did not know that "unnamed" instances actually were "named by Lean"! Is there a place where I can find a (not necessarily exhaustive) list of situations where I can assume that Lean is producing more in the background?

[Johan Commelin]

I agree that it would be good to have a way to figure out instance names easily

[Scott Morrison]

Johan Commelin said:

The problem with instance? is that it causes 85% of mathlib to recompile, if you use it on an instance low in the hierarchy

I often just restart the server if I temporarily touch a file low down in the hierarchy.

[Kevin Buzzard]

Right -- my use case is that I want to see the name generated by an instance command somewhere in mathlib, and then promptly return things to normal

[Johan Commelin]

still, if VScode could show the name when you hover over instance that would be more ergonomical than appending ? and restarting lean afterwards.

[Kevin Buzzard]

That would be even better!

[Yakov Pechersky]

Would we turn off the noisy linter for the instance decls then?
To find instances, I usually make a scratch file like so:

import data.real.basic

example : ring ℝ := by show_term { apply_instance }

[Kevin Buzzard]

The problem with that approach is that it sometimes says "it was field.to_ring"

[Kevin Buzzard]

I used to do it like that but now I tend to set things up in a tactic block so I can use the infoview to see the actual concrete instance which made it happen rather than just the projections which were applied afterwards.

[Mario Carneiro]

How about a more low level option? set_option trace.new_definitions true and then any time a declaration is added to the environment (via lean internals, user tactics, or directly), the full name of the definition is also printed

[Floris van Doorn]

I implemented this for simps specifically in #6995

[Floris van Doorn]

I am implementing this for to_additive in #7888