expose `#help options` to meta-Lean

[robertylewis]

At https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Dots.20in.20outputs.20.2B.20documentation it was pointed out that we have no manual page listing all the configuration options.

These options are at least slightly dynamic, in that users can create new trace options, so such a page would need to be generated from compiled mathlib the same way as the rest of the docs.

Is it possible to expose the output of #help options? Unfortunately the descriptions for all of the trace options are the same; we'll have to do something there too. As a first pass we could just collect them all together under one description.

Prerequisites

• [ ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[gebner]

Note that for the docs we could just create a file containing import all #help options and parse the output.

If somebody wants to implement this, it would also be nice to have a register_option function in meta code.

[robertylewis]

That's fair, and probably the less disruptive way to do this!