your favourite set_option option

Stream: general

[Kevin Buzzard]

I find set_option stuff hard to remember, and difficult to look up. I just learnt another one today from the conversation Sebastien and Gabriel were having about metavariables. Here's my list of cool set_option stuff which I as a non-tactic-writing intermediate level Lean user have found helpful in the past:

• see the gory details of everything
  set_option pp.all true

• some metavariable thing which I haven't understood properly yet but looks interesting
  set_option pp.instantiate_mvars false

• see how simp did it:
  set_option trace.simplify.rewrite true

• Why are these not defeq / why is rfl failing?
  set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

• why isn't typeclass resolution working?
  set_option trace.class_instances true

Are there any others that people secretly use and which I don't know about? I remember once typing something into Lean and seeing every single option (that's something else I can never remember how to do) but that there were basically too many to comprehend, and I suspect that a user like me never needs to know most of them. The above ones are things which might help me if I'm stuck just writing a regular tactic proof.

[Mario Carneiro]

I remember once typing something into Lean and seeing every single option

That would be #help options

[Mario Carneiro]

I feel like we should do something about #help, either eliminate it or beef it up and hook it to the community web pages or something

[Mario Carneiro]

it's so rarely used it's hard to remember

[Yakov Pechersky]

Is there one for tracing through what refl did?

[Mario Carneiro]

sadly no, except is_def_eq

[Mario Carneiro]

Here's one:

• See what the bytecode for a VM definition is
  set_option trace.compiler.optimize_bytecode true

[Mario Carneiro]

the name is confusing because it's actually a printing option even though it sounds like a configuration

[Mario Carneiro]

• When pp.all is too much information:
  • set_option pp.notation false
  • set_option pp.implicit true
  • set_option pp.numerals false

[Mario Carneiro]

Whoa, what is set_option pp.links true?

[Mario Carneiro]

(pretty printer) add links to constants using control characters

[Gabriel Ebner]

lean#89 It's used in the documentation.

[Mario Carneiro]

aha I was wondering how you pulled that off

[Gabriel Ebner]

Another useful one:
set_option profiler true

[Mario Carneiro]

set_option pp.proofs true when you are facing an unhelpful classical.some _

[Mario Carneiro]

although we should solve this sort of thing with better implicitness conventions

[Kevin Buzzard]

I only didn't mention those last two because I find them easy to remember :-)

[Bryan Gin-ge Chen]

Shall we compile these into a markdown file and put them on our webpage here?

[Kevin Buzzard]

That would be a great idea! I genuinely have to search through Zulip whenever I want to know what some of those options are; looking on the website would be much better for me.

[Floris van Doorn]

set_option old_structure_cmd true
The others are already mentioned here.