doc-gen
doc-gen copied to clipboard
leanprover-community
Convert to an installable python package
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__.pyinto 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.
What is the story for the *.lean files here? Are these installed as well?
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.
Yeah sure, I can squash.
What is the story for the *.lean files here? Are these installed as well?
No, not yet - but the python code doesn't use these at all yet.
No, not yet - but the python code doesn't use these at all yet.
Hmm, but is there anything you can do with the python code alone? Related question: are the CSS/JS files copied as well? I can't find any relevant changes in the PR.