Zulip Chat Archive

Stream: general

Topic: simps?, reassoc?, mk_iff?


view this post on Zulip Scott Morrison (Mar 29 2021 at 23:08):

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

view this post on Zulip Scott Morrison (Mar 29 2021 at 23:11):

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 ?.

view this post on Zulip Bhavik Mehta (Mar 30 2021 at 01:28):

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!

view this post on Zulip Bhavik Mehta (Mar 30 2021 at 01:29):

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

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 05:33):

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

view this post on Zulip Scott Morrison (Mar 30 2021 at 05:36):

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

view this post on Zulip Johan Commelin (Mar 30 2021 at 05:47):

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

view this post on Zulip Damiano Testa (Mar 30 2021 at 05:47):

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?

view this post on Zulip Johan Commelin (Mar 30 2021 at 05:47):

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

view this post on Zulip Scott Morrison (Mar 30 2021 at 06:17):

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.

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 06:52):

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

view this post on Zulip Johan Commelin (Mar 30 2021 at 06:55):

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

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 08:43):

That would be even better!

view this post on Zulip Yakov Pechersky (Mar 30 2021 at 08:49):

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 }

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 08:58):

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

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 08:59):

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.

view this post on Zulip Mario Carneiro (Mar 30 2021 at 15:43):

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

view this post on Zulip Floris van Doorn (Apr 01 2021 at 21:39):

I implemented this for simps specifically in #6995


Last updated: May 10 2021 at 18:22 UTC