Convert to an installable python package

[eric-wieser]

This isn't a full conversion, but should still work after this restructure.

The motivation here is to try and separate out "things specific to mathlib" from "things other lean projects might want". It also means we don't need to worry about any python file names clashing with builtin modules, as they're now namespaced to lean_doc_gen.

Future ideas intended for later PRs:

• Extract the command line parsing from __init__.py into its own file
• Convert some shell scripts to python scripts
• Extract mathlib config to a config file in the mathlib repo.

---

Since bors isn't enabled in this repository, if we do decide to merge this we should either squash merge through github, or I should manually do so locally.