feat: add --help and --all-theorems command line options

[robsimmons]

If we'd like to export and replay the contents of a module, it's desirable to be able to export just the constants in that module and their transitive dependencies.

This PR, in addition adds an --all-theorems MODULE_NAME command line option that adds all the theorems in the specified module to the root set of constants for exporting. It can be used in conjunction with naming individual constants with the -- option.

Additional changes:

• Refactor: consolidates parsing of command line arguments

• Feature: adds usage information, -h argument

• Feature: turns several panics into controlled error (invalid constant, constant not present in environment)

• Backwards incompatible (or bugfix, depending on your perspective): Move the filtering of unsafe constants from the "dump constant" phase to the "figure out what 'everything' is when we export everything".

  Currently, if Foo contains an unsafe definition x, then lean4export Foo -- x just silently drops x. It should either throw an error ("--export-unsafe required") or print out x and its dependencies, and this resolves to do the latter: --export-unsafe only affects the "export everything" behavior.

[nomeata]

Seems unnecessarily restrictive. Why not allow the user to specify any set of module names and/or constants to export? Maybe I need an export of module A and B and additionally foo.

[robsimmons]

@nomeata I think you're right — I've changed the behavior quite a bit so that "export all (theorems) from a module" and "export these constants specifically" are compatible.