Add special handling for missing deal_solver

[rpdelaney]

Before this change, the prover attempts to handle the case where
deal_solver cannot be imported by setting deal_solver = None.
However, instantiation of the DealTheorem class a few lines later
depends on deal_solver. This results in an unhandled exception because
None does not have a "Theorem" attribute:

$ python3 -m deal lint
Traceback (most recent call last):
  File "/Users/ryan/.local/share/asdf/installs/python/3.10.2/lib/python3.10/runpy.py", line 196, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "/Users/ryan/.local/share/asdf/installs/python/3.10.2/lib/python3.10/runpy.py", line 86, in _run_code
    exec(code, run_globals)
  File "/Users/ryan/src/me/extinfo/.venv/lib/python3.10/site-packages/deal/__main__.py", line 6, in <module>
    sys.exit(main(sys.argv[1:]))
  File "/Users/ryan/src/me/extinfo/.venv/lib/python3.10/site-packages/deal/_cli/_main.py", line 37, in main
    commands = get_commands()
  File "/Users/ryan/src/me/extinfo/.venv/lib/python3.10/site-packages/deal/_cli/_main.py", line 16, in get_commands
    from ._prove import ProveCommand
  File "/Users/ryan/src/me/extinfo/.venv/lib/python3.10/site-packages/deal/_cli/_prove.py", line 26, in <module>
    class DealTheorem(deal_solver.Theorem):
AttributeError: 'NoneType' object has no attribute 'Theorem'

After this change, a special exception is raised to get_commands() so that
when deal_solver import fails, the ProveCommand can be set to an empty
Command (because the prover cannot run at all without the solver).

[rpdelaney]

I'm working on a test for the lines added to _cli/_main.py. Not sure I understand the other CI errors since I'm not reproducing them locally but I'll look more into that after a test is done to maintain coverage %.

[rpdelaney]

Needs more work.

[orsinium]

Hey, good catch. Try this fix instead:

try:
  from deal_solver import Theorem
except ImportError:
  Theorem = object

class DealTheorem(Theorem):
  ...

[rpdelaney]

Seems to work. I am concerned that that could break the many references to deal_solver elsewhere in the file, but if you're confident that this stuff will never get executed if deal_solver isn't installed, then that's good enough for me. :-)

mypy is unhappy about a few things on my end but let's see what your CI says.

[orsinium]

but if you're confident that this stuff will never get executed if deal_solver isn't installed, then that's good enough for me

From this file, only ProveCommand is supposed to be executed, and it has an explicit check for deal_solver presence. That said, I should have some kind of tests for bare-bones deal installation.

Hmm, what's wrong with CI? Let's see. It might be related to yesterday's GitHub hiccups (githups?).

[orsinium]

Thank you for your help