A useless option which I can use for another purpose?

Stream: general

[Jason Rute]

Lean has a number of "options", e.g. pp.all, which are used for various things. Since one can't add custom options, I'd like to co-opt one for a proof recording project. In particular, I'd like to make it such that if I run lean -D <some_option>=<some_value> all.lean then Lean will spit out (lots of) trace code, but will not otherwise. Is there an option which is useless which I can use without it effecting the behavior of Lean?

[Jason Rute]

If not, I just realized I might be able to just use that a particular option is set. Most options are never actually set. They have default behavior, but one can distinguish (inside a tactic) if an option is set to anything or nothing, so maybe I can just test that some obscure option like pp.colors is set to something, and I'll just set it to the default value.

[Johan Commelin]

@Jason Rute I guess you can add options in the community fork of Lean? It's a bit more cumbersome, because you have to change core.... not sure whether it's worth it, or if you should just use your hack (-;

[Jason Rute]

I’m doing this proof recording without changing the C++. (Mostly because I’m not comfortable programming in it.) But if the options are built into the lean files, I could change those.

[Johan Commelin]

Well, I'm also not comfortable with changing the C++ for you... so we would have to wait for Gabriel, I guess

[Kevin Lacker]

there is the trace_if_enabled stuff for tracing according to whether a flag is set to on or off. the flag is set from within lean code rather than from the command line, but depending on what environment you're running this in, that might not be too hard to mess around with

[Scott Morrison]

You can add new trace options yourself. Several tactics already do this. (e.g. suggest and solve_by_elim offhand)

[Gabriel Ebner]

Unfortunately none of these options can be set on the command-line, because there's a check that you only use built-in options..

[Gabriel Ebner]

We should disable that check.

[Jason Rute]

Thanks. I think I’ll just go with my hack. This will be very hacky code anyway. I’m trying to record all the tactic proofs in Lean with a combination of carefully placed tracing code added the standard library and mathlib and a crappy homemade Lean parser written in Python.