Zulip Chat Archive

Stream: general

Topic: A useless option which I can use for another purpose?

Jason Rute (Oct 22 2020 at 00:37):

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 (Oct 22 2020 at 00:41):

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 (Oct 22 2020 at 03:25):

@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 (Oct 22 2020 at 03:30):

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 (Oct 22 2020 at 03:38):

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

Kevin Lacker (Oct 22 2020 at 04:12):

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 (Oct 22 2020 at 06:15):

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

Gabriel Ebner (Oct 22 2020 at 07:11):

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 (Oct 22 2020 at 07:11):

We should disable that check.

Jason Rute (Oct 22 2020 at 11:28):

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.

Last updated: Dec 20 2023 at 11:08 UTC