Zulip Chat Archive

Is there a way to know all possible set_option parameters one can set, and what is their effect? I am currently looking for an option to "see" the value that Lean assigned to an underscore in the application of a lemma, and some combinations of set_option pp.all true or set_option trace.type_context.is_def_eq_detail true and trace.class_instances true help a bit. Yet, it is completely obscure to me what I am doing, and I wonder how I could get a general picture.

Also, if I try a "stupid thing" like set_option pp.foo true, VSCode tells me unknown option 'pp.foo', type 'help options.' for list of available options and I am stuck with the stupid question : "Where should I type help options?"

Julian Berman (Feb 12 2022 at 17:32):

It's #help options, just as a Lean command -- maybe that should go in the FAQ (I didn't remember what the right invocation was but I recalled Kyle sharing some details which helped find a previous Zulip thread).

Filippo A. E. Nuccio (Feb 12 2022 at 17:33):

Thanks!

Filippo A. E. Nuccio (Feb 12 2022 at 17:34):

I see that there are trillions of them, but at least I can read some of them... :100:

Julian Berman (Feb 12 2022 at 17:34):

Yeah somewhere there's a thread where someone shared a more trimmed down list, but I don't see it yet.

Filippo A. E. Nuccio (Feb 12 2022 at 17:35):

@Alex J. Best Do you think some of these things might land in your tips&trick page?

Alex J. Best (Feb 12 2022 at 17:47):

Yeah that would be good, something about debugging type class problems with trace.class_instances and friends would be nice for sure. Feel free to PR a draft, or I'm happy to try and write something about it this week.

Filippo A. E. Nuccio (Feb 12 2022 at 17:47):

Ok, I will see if I can do something reasonable!

Kevin Buzzard (Feb 12 2022 at 19:41):

Yeah I asked people for their favourites in some thread a couple of years ago. I agree that there are trillions (Filippo and I are number theorists hence we reserve the right not to be able to count); I don't think I've ever used any beyond the ones mentioned in that thread.